Why do we even need axiom schema?

Question

It has already been shown that a parameter-free form of ZFC is as strong as ZFC with parameters (hence it is not necessary to have a separate axiom for every list of parameters). Even so, comprehension remains an axiom schema because $\forall\varphi.\forall X.\exists Y.\forall y.y\in Y\iff(y\in X\land \varphi(y))$ cannot be a first-order formula if $\varphi$ is a predicate.

But then, I'm told that ZFC is single-sorted and that the only terms are sets. Furthermore, predicates can be represented as sets by way of $\varphi(x)\iff x\in S_\varphi$, where, naturally $S_\varphi=\{x:\varphi(x)\}$; and this is done specifically to avoid introducing new sorts (or types) to set theory.

That being the case, why bother with the axiom schema at all?

Why not have the single axiom $\forall P.\forall X.\exists Y.\forall y.y\in Y\iff (y\in X\land y\in P)$?

The same thing can be done with replacement.

---

Edit:

To clarify, my thinking goes something like this:

Technically, $\{x:\varphi(x)\}$ is, in general, a class but not a set. That being said, if $X$ is a set and $S_\varphi$ is a class, and $z\in Z\iff z\in X\land z\in S_\varphi$, then $Z$ is also a set. ZFC is single-sorted, so the distinction between set and class is not explicit. In fact, the only way to formally prove the statement "$X$ is/is not a set" is to introduce additional sorts to ZFC.

If you extend ZFC by classes (obtaining a two-sorted theory), then the axiom above can be "translated" to:

$$\forall P^\mathbf{class}.\forall X^\mathbf{set}.\exists Y^\mathbf{set}.\forall y^\mathbf{set}.y\in Y\iff(y\in X\land y\in P)$$

(which is basically the same as the second order axiom of comprehension)

The reason I didn't think this was necessary is that there oughtn't be any set $X$ such that $X$ is the intersection of a set and class (the latter of which cannot be proven to exists in ZFC), but is not the intersection of a set with another set.

Let $\varphi$ be a predicate such that $\{x:\varphi(x)\}$ is a class but not a set. Unless the class $\{x:\varphi(x)\}\cap\mathbf{set}$ is empty, then there must be some set $Y$ such that for any set $X$, $X\cap Y$ is equivalent to $X\cap\{x:\varphi(x)\}$, yes?

Why should it matter if $\{x:\varphi(x)\}$ provably exists?

Answer 1

$S_\varphi$ need not be a set as you defined it : take $\varphi(x) := (x=x)$ for instance. So you need to have some form of thing that tells you that when you restrict it to $X$, then it is in fact a set.

That's what the comprehension axiom scheme tells you. The same type of thing happens with replacement.

In fact it's a theorem that (assuming it's consistent) ZFC cannot be finitely axiomatized : you really do need some axiom schemes, otherwise you're strictly less powerful.

So we can't get rid of axiom schemes if we want to get ZFC, no matter how smart we are in formulating things (as long as we're doing things in the first order, and assuming ZFC is consistent)

Answer 2

We do we need an axiom schema? Well, the short answer is that we want to have first order theories. And quantifying over formulas or classes would be a second order quantifier.

First order theories are great, first order logic has a nice computable proof verification, and everything is neat.

Okay, you might say, move to a second-order theory like von Neumann–Gödel–Bernays, which can be seen as a Henkinization of Zermelo–Fraenkel (and Choice), so you get all the good computable stuff, but you still have a single axiom.

But now we're missing something else. Something deeper. Something useful. $\sf ZFC$, unlike $\sf NBG$, proves the consistency of its finite subtheories. That is to say, if $T$ is a finite set of axioms of $\sf ZFC$, then $\sf ZFC\vdash\operatorname{Con}(T)$.

Why is this good? Well, we want to study independence over $\sf ZFC$, for example of the Continuum Hypothesis. We know, from a meta-theoretic point of view, that it is enough to prove that no finite subtheory of $\sf ZFC$ proves $\sf CH$. Using the above observation, we can work internally to $\sf ZFC$ and prove that no finite fragment proves $\sf CH$. This gives us a lot more power in studying the foundations of mathematics from within mathematics.

This might seems like a quirk. And some people would argue that it is, and if we study the foundations of mathematics, then all the more reason to do that entirely from the meta-theory. But there is elegance to being able to do it from within the theory.

---

It might also be worth noting that taking up the full second order semantics, replacing the Replacement schema with its second order axiom, we have $\sf ZFC_2$, and any model of $\sf ZFC_2$ must be of the form $V_\kappa$ for an inaccessible $\kappa$ (up to isomorphism). And even if you allow Replacement to remain a schema, but replace only Separation by an axiom, we still get a model isomorphic to $V_\kappa$, only that $\kappa$ might not be an inaccessible cardinal.

This is not great, because these models contain all the reals, so they must agree with their meta theory about things like $\sf CH$. And therefore they are terrible for studying any reasonable independence phenomenon. Of course, that being said, we do study independence over $\sf NBG$ or even Morse–Kelley set theory (which is again not finitely axiomatizable), by treating them as first order theories that arise from the natural second order "completions" of $\sf ZFC$.

Answer 3

Summary/takeaway of discussion

The axiom schema of comprehension guarantees that for any set $X$ and predicate $\varphi$, there exists a set $Y$ containing those members of $X$ for which $\varphi(x)$ holds.

In a particular extension of ZFC:

1. Every set is a class (but not every class is a set)

2. For every predicate $\varphi$, there is a class $C_\varphi$ such that $x\in C_\varphi\iff \varphi(x)$

For a given $\varphi$, the axiom of comprehension can be stated as:

$$\forall X.\exists Y.\forall y.y\in Y\iff(y\in X\land \varphi(y))$$

This is equivalent to:

$$\forall X.\exists Y.\forall y.y\in Y\iff (y\in X\land y\in C_\varphi)$$

Since the class of sets exists, if the intersection $C_\varphi$ with the class of sets is nonempty, then there is a least set $S_\varphi$ such that $\varphi(s)$ holds for all $s\in S_\varphi$ (this is not something proven within the scope of the theory, it's just a generic statement).

Since each predicate has a corresponding set, we can rewrite the above as:

$$\forall S.\forall X.\exists Y.\forall y. y\in Y\iff (y\in X\land y\in S)$$

This is equivalent to "the intersection of any two sets exists."

Moving back to ZFC, we can take away classes entirely by assuming $\{x:\varphi(x)\}$ to be the least member of the intersection of $C_\varphi$ with the class of sets (this guarantees at least one set for each predicate). If $S_\varphi$ is the least such set, then the above guarantees that for any set $X$, the set $\{x\in X:\varphi(x)\}=X\cap S_\varphi$ exists.

However, this does not prove that $S_\varphi$ exists.

So while we might be able to prove that "every subset of the integers exists" (provided that we can prove the existence of the integers), we cannot prove that "the set of odd integers exists".

This is where the "axiom of intersection," as it were, fails. While it suffices to prove that a subset of a particular set exists if there is a second set to take the intersection, it does not prove that the second set exists in the first place.

Proving the existence of the second set ultimately requires proving that for any $\varphi$, $S_\varphi$ exists - ultimately ends up being equivalent to the original axiom schema of comprehension.

---

For anyone who's interested, it might be possible to produce interesting "fragments" of ZFC by replacing the axiom schemata as described, and adding a "set construction axiom" (basically, an algorithm for constructing new sets from existing ones, for example $\forall x.\exists y. y=\{x\}$).

I don't know what applications this would have, if any, but it's something to think about.