Quantification over the set(?) of predicates

Question

When learning set theory and logic, one fact that popped up a handful of times was that we did not quantify over predicates. To quote the notes I took in class on the axiom of unrestricted comprehension:

Given any predicate $\varphi$ in the language of set theory with one free variable $x$ (and perhaps some parameters $a_1,\ldots,a_n$), there exists a necessariy unique set $\{x\;\colon\;\varphi(x)\}$.

Note that $\varphi$ is not part of the logical language: it is not an object that has members and so we cannot say $\forall\varphi$. Formally we would write $$\exists A\forall x(x\in A\leftrightarrow\varphi(x)).$$

Is there a reason why we cannot (or do not want to?) quantify over predicates?

I have also studied the arithmetization of syntax, whereby we code functions, relations, sentences, predicates, etc. by natural numbers, in an effort to state and prove the First Incompleteness Theorem. I am wondering if there is any way you could take a similar approach to translate predicates into sets, thereby creating a "set of predicates"? Indeed, we could arithmetize these predicates by the Godel function $\#$, and then form a set of predicates via the axiom schema of restricted comprehension (separation), by having some predicate $\psi$ such that $\psi(y)$ if and only if $y=\#(\varphi(x))$ for some predicate $\varphi(x)$ with one free variable. This would remove the restriction on quantifying over predicates.

Realizing that this does not circumvent the need for a schema, this doesn't achieve much. However my question is whether it is possible to quantify over predicates: if so, is my argument valid, and if not, why not?

Answer 1

Not sure if this is an answer, but it's too long for a comment:

Sure it's possible to quantify over subsets of the domain$^*$, in the sense that (with a background set theory in place) we can define semantics for a logic which does so; but do we want to?

To build on Asaf's comment, let me give a classic example of a terrible second-order sentence $\varphi$. We work in the language consisting of two unary predicates, $U$ and $V$, and one binary relation $E$. Now $\varphi$ says:

• $U$ and $V$ partition the domain.

• $U$ is infinite and countable.

• $E\subseteq U\times V$.

• For every subset $X$ of $U$, there is a unique $v\in V$ such that $X=\{u: uEv\}$.

• Every uncountable subset of $V$ has the same cardinality as $V$ itself.

It's not hard to write the above in second-order logic. But now $\varphi$ has a model if and only if the continuum hypothesis is true! So even deciding whether sentences of second-order logic are consistent requires us to make strong set-theoretic commitments. By contrast, the consistency problem for first-order logic, while undecidable, has no real set-theoretic content. (An important side effect of this is that, while first-order logic has a "purely syntactic" side captured by the Completeness Theorem, second-order logic really doesn't, so if you want to use second-order logic while avoiding making ontological commitments, you're in a bit of a jam. Quine famously called second-order logic "set theory in sheeps' clothing" for this reason, although others have pushed back against this.)

So it all boils down to: what do we want out of our logic? Expressive power and nice behavior are fundamentally at odds with one another (a similar theme is behind Godel's incompleteness theorem). Ultimately, one might argue that we should look for theorems of the following form:

[Such-and-such] logic is the strongest logic with [so-and-so] nice property.

This has actually been done for first-order logic - Lindstrom's theorem states that first-order logic is the strongest logic with the compactness and Lowenheim-Skolem properties. Now, how strong an argument Lindstrom's theorem is for first-order logic being the "right" logic depends on how important you view these specific nice properties, and reasonable people can disagree here - personally I find it extremely compelling, but others do not.

The point is that when we ask, "What logic should we use for (this piece of) mathematics?", we implicitly have a lot of preferences for how a logic should/should not behave (in this context); and these preferences are going to be in tension with one another.

---

Your question is actually about quantifying over definable subsets of the domain, e.g. predicates, not arbitrary subsets; but there's a strong similarity here. For any given logic $L$, we can devise a new logic $L'$ which is $L$ together with the ability to quantify over $L$-formulas; these logics get progressively worse and worse, and looking at the full second-order picture is a good first step to understanding this level-by-level, definable picture. You may also be interested in the hyperarithmetic hierarchy.