In logic, quantifiers $\forall$ and $\exists$ give mathematical objects. Is there any equivalent "quantifier" giving a logical proposition or predicate?
For example, if I denote the "for all predicate P" by $\square P$, I could write:
$$\forall x,\forall y,[x = y \Leftrightarrow (\square P,P(x)\Leftrightarrow P(y))]$$
My question is then: is there any standard notation for $\square$? Is this concept even useful? Can we consider propositions and predicates as a specific type of object?
Thanks in advance.
Logical propositions and predicates “quantifiers”
logicquantifiers
Best Answer
Yes. The ability to quantify over predicates is the defining feature of second order logic. You can then ask if you can quantify over predicates that expect predicates and so forth, and these give rise to other higher order logics in an analogous way.
As an example in second order logic, you can say:
$$\forall P . \forall x . P(x) \lor \lnot P(x)$$
Here we are quantifying first over all predicates $P$, then over all elements $x$, then asserting the law of the excluded middle holds in every case.
These logics are fairly well studied, but they're substantially less well behaved than first order logic. In particular things like the compactness theorem fail because there's no good notion of proof theory for higher order logics.
A big part of the reason we use set theory as our foundations is because we can imitate higher order logic inside first order logic. Since everything is a set in ZFC, we can "quantify over propositions" by looking at the set of propositions (which is itself an element of our theory). This is a big part of where set theory gets its power, and I seem to recall a prominent set theorist saying "any higher order logic is set theory in sheep's clothing", but I'm forgetting where I saw it. I'm sure a quick google will bring it up if you're interested.
I hope this helps ^_^