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.


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?

  • 4
    $\begingroup$ What do you mean by "predicates can be represented as sets"? The statement "for any formula $\varphi$, the collection $S_{\varphi} = \{ x : \varphi(x) \}$ is a set" is obviously not true. $\endgroup$
    – Adayah
    Commented May 19, 2020 at 21:09
  • 4
    $\begingroup$ All your "new axiom" gives is that the intersection of any pair of sets exists, but nothing about it will guarantee that $\{x:\varphi(x)\}$ exists for any $\varphi$. $\endgroup$ Commented May 19, 2020 at 21:12
  • 1
    $\begingroup$ You write "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". How do you know that is true, if you don't have the comprehension schema?? $\endgroup$ Commented May 19, 2020 at 21:51
  • $\begingroup$ @EricWofsey By formalizing ZFC in terms of classes, and showing that every subset of a set is also a set. This is more or less what Andre does in Axioms and Set Theory. $\endgroup$
    – R. Burton
    Commented May 19, 2020 at 21:53
  • $\begingroup$ @R.Burton: A formalization that includes classes is not ZFC. Maybe you are thinking of NBG instead? $\endgroup$ Commented May 19, 2020 at 22:06

3 Answers 3


$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)

  • $\begingroup$ While it is certainly true that a predicate need not form a set, the intersection of the class $S_\varphi$ and a set does. It is this fact that led me to ask the question. Of course, because we're dealing with a single-sorted theory, any term referred to in the axiom will also be a set. The only way I can see this being a problem is if there is a set which can only be expressed as the intersection of a proper class with a set, but is not the intersection of a set with another set. $\endgroup$
    – R. Burton
    Commented May 19, 2020 at 21:21
  • 3
    $\begingroup$ Well how do you get $\{x \in X \mid \varphi(x)\}$ for a general $\varphi$ from your axiom ? If you don't know a priori that $\{x : \varphi(x)\}$ is a set ? Who will be the $P$ “ $\endgroup$ Commented May 19, 2020 at 21:24
  • 3
    $\begingroup$ This has nothing to do with the issue at hand. How can you prove, with your axiom, that $\{x \in X \mid \varphi(x)\}$ exists, for a general $\varphi$ ? If you manage to prove it, you'll prove ZFC inconcistent and will change the face of maths (to a degree) $\endgroup$ Commented May 19, 2020 at 21:32
  • 1
    $\begingroup$ ZFC can prove the existence of what I mentioned. So it is sufficiently strong, and you claim your theory is equivalent but it can't prove that, and we really need a theory of sets to be able to prove that or we can't do much. $\endgroup$ Commented May 19, 2020 at 21:48
  • 1
    $\begingroup$ @Zuhair you're right maybe it wasn't clear enough, I edited $\endgroup$ Commented May 21, 2020 at 21:43

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$.


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.

  • 1
    $\begingroup$ Comprehension is typically Frege's inconsistent "unrestricted comprehension". Separation of Subset, or even Restricted/Bounded Comprehension would be clearer. $\endgroup$
    – Asaf Karagila
    Commented May 22, 2020 at 1:44
  • 1
    $\begingroup$ What you discovered here is simply Scott's trick of making classes into sets. It's used to define cardinals of sets which cannot be well-ordered in ZF, for example, but also to formalise things like ultrapower embeddings in the context of large cardinals. $\endgroup$
    – Asaf Karagila
    Commented May 22, 2020 at 1:47

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .