Proof of The Class Comprehension Theorem for Predicative Formulas

The argument follows Mendelson's proof of the class existence theorem (Introduction to Mathematical Logic, Chapter 4, Proposition 4.4 and the propositions before it), reorganised. It is a proof scheme: for each fixed formula, and for each fixed metatheoretic number used below, the inductions below (which are inductions in the metatheory) produce a proof in the theory.

Throughout, letters $a,b,c,p,q,y$ in Step 0 denote sets. We use two facts about tuples that hold by their definition: every tuple and every ordered pair of sets is a set, and $\langle x_{1},\dots,x_{n},x_{n+1}\rangle=(\langle x_{1},\dots,x_{n}\rangle,x_{n+1})$, in particular $\langle a,b,c\rangle=((a,b),c)$ and $\langle x_{1}\rangle=x_{1}$. All equivalences below are obtained by instantiating the universally quantified conditions of the axioms at these sets; no injectivity of pairs is needed. We also use that some set exists, by the axiom of the empty set; call this fact (S). Each clause of the class existence axioms applies to arbitrary classes $X$ and $Y$.

Step 0. Derived class constructions.

Lemma A (reversing pairs). For every class $X$ there is a class $Z$ such that $(a,b)\in Z$ if and only if $(b,a)\in X$, for all sets $a,b$.

By (B5) applied to $X$ there is $X_{1}$ with $(p,c)\in X_{1}$ if and only if $p\in X$, for all sets $p,c$; taking $p=(a,b)$ gives $\langle a,b,c\rangle\in X_{1}$ if and only if $(a,b)\in X$. By (B7) applied to $X_{1}$ there is $X_{2}$ with $\langle a,b,c\rangle\in X_{2}$ if and only if $\langle a,c,b\rangle\in X_{1}$. By (B6) applied to $X_{2}$ there is $X_{3}$ with $\langle a,b,c\rangle\in X_{3}$ if and only if $\langle b,c,a\rangle\in X_{2}$; by the previous condition (instantiated at $b,c,a$) this holds if and only if $\langle b,a,c\rangle\in X_{1}$, that is, if and only if $(b,a)\in X$. So the swap of the first two entries of a triple is the composite of one transposition and one rotation. Finally, by (B4) applied to $X_{3}$ there is $Z$ with $p\in Z$ if and only if there is a set $c$ with $(p,c)\in X_{3}$. For $p=(a,b)$ we have $(p,c)=\langle a,b,c\rangle$, so $(a,b)\in Z$ if and only if there is a set $c$ with $(b,a)\in X$. The condition $(b,a)\in X$ does not involve $c$, and by (S) some set $c$ exists; hence $(a,b)\in Z$ if and only if $(b,a)\in X$.

Lemma R (testing one entry against a passenger). For every metatheoretic $n\ge1$, every $i$ with $1\le i\le n$ and every class $W$ there is a class $Z$ such that, for all sets $x_{1},\dots,x_{n},y$, we have $(\langle x_{1},\dots,x_{n}\rangle,y)\in Z$ if and only if $(x_{i},y)\in W$.

By induction on $n$. For $n=1$ we have $i=1$ and $\langle x_{1}\rangle=x_{1}$, so $Z=W$ works. Suppose the lemma holds for $n$, and let $1\le i\le n+1$. Write $t=\langle x_{1},\dots,x_{n}\rangle$, a set; then $(\langle x_{1},\dots,x_{n+1}\rangle,y)=((t,x_{n+1}),y)=\langle t,x_{n+1},y\rangle$.

Case $i\le n$. The induction hypothesis gives $Z_{0}$ with $(t,y)\in Z_{0}$ if and only if $(x_{i},y)\in W$. By (B5) applied to $Z_{0}$ there is $Z_{1}$ with $\langle a,b,c\rangle=((a,b),c)\in Z_{1}$ if and only if $(a,b)\in Z_{0}$. By (B7) applied to $Z_{1}$ there is $Z$ with $\langle a,b,c\rangle\in Z$ if and only if $\langle a,c,b\rangle\in Z_{1}$. Then $\langle t,x_{n+1},y\rangle\in Z$ if and only if $\langle t,y,x_{n+1}\rangle\in Z_{1}$, if and only if $(t,y)\in Z_{0}$, if and only if $(x_{i},y)\in W$.

Case $i=n+1$. By (B5) applied to $W$ there is $Z_{1}$ with $\langle a,b,c\rangle\in Z_{1}$ if and only if $(a,b)\in W$. By (B6) applied to $Z_{1}$ there is $Z$ with $\langle a,b,c\rangle\in Z$ if and only if $\langle b,c,a\rangle\in Z_{1}$. Then $\langle t,x_{n+1},y\rangle\in Z$ if and only if $\langle x_{n+1},y,t\rangle\in Z_{1}$, if and only if $(x_{n+1},y)\in W$.

Lemma Q (one entry in a class). For every metatheoretic $n\ge1$, every $i$ with $1\le i\le n$ and every class $W$ there is a class $Z$ such that $\langle x_{1},\dots,x_{n}\rangle\in Z$ if and only if $x_{i}\in W$, for all sets $x_{1},\dots,x_{n}$.

By (B5) applied to $W$ there is $W_{1}$ with $(a,b)\in W_{1}$ if and only if $a\in W$. Lemma R applied to $n$, $i$ and $W_{1}$ gives $Z_{0}$ with $(\langle x_{1},\dots,x_{n}\rangle,y)\in Z_{0}$ if and only if $(x_{i},y)\in W_{1}$, that is, if and only if $x_{i}\in W$. By (B4) applied to $Z_{0}$ there is $Z$ with $p\in Z$ if and only if there is a set $y$ with $(p,y)\in Z_{0}$. Taking $p=\langle x_{1},\dots,x_{n}\rangle$: $p\in Z$ if and only if there is a set $y$ with $x_{i}\in W$, which by (S) holds if and only if $x_{i}\in W$.

Lemma P (two distinct entries as a pair in a class). For every metatheoretic $n\ge1$, all distinct $i,j$ with $1\le i,j\le n$ and every class $W$ there is a class $Z$ such that $\langle x_{1},\dots,x_{n}\rangle\in Z$ if and only if $(x_{i},x_{j})\in W$, for all sets $x_{1},\dots,x_{n}$.

By induction on $n$. For $n=1$ there are no distinct $i,j$ and there is nothing to prove. Suppose the lemma holds for $n$, let $i\ne j$ be in $1,\dots,n+1$, and write $\langle x_{1},\dots,x_{n+1}\rangle=(\langle x_{1},\dots,x_{n}\rangle,x_{n+1})$.

Case $i,j\le n$. The induction hypothesis gives $Z_{0}$ with $\langle x_{1},\dots,x_{n}\rangle\in Z_{0}$ if and only if $(x_{i},x_{j})\in W$. By (B5) applied to $Z_{0}$ there is $Z$ with $(p,q)\in Z$ if and only if $p\in Z_{0}$; with $p=\langle x_{1},\dots,x_{n}\rangle$ and $q=x_{n+1}$ this is the claim.

Case $j=n+1$, so $i\le n$. Lemma R applied to $n$, $i$ and $W$ gives $Z$ with $(\langle x_{1},\dots,x_{n}\rangle,y)\in Z$ if and only if $(x_{i},y)\in W$; take $y=x_{n+1}$.

Case $i=n+1$, so $j\le n$. Lemma A applied to $W$ gives $W'$ with $(a,b)\in W'$ if and only if $(b,a)\in W$. Lemma R applied to $n$, $j$ and $W'$ gives $Z$ with $(\langle x_{1},\dots,x_{n}\rangle,y)\in Z$ if and only if $(x_{j},y)\in W'$, that is, if and only if $(y,x_{j})\in W$; take $y=x_{n+1}$.

Reduction to class parameters. Let $\varphi$ be as in the clause comprehension of the statement, and suppose some parameter is a set variable $u$, assigned a set $a$. By renaming bound variables (as in Stage (1a) below, with fresh set variables; equivalent under every assignment by elementary logic) we may assume that no quantifier of $\varphi$ binds $u$, so every occurrence of $u$ in $\varphi$ is free. Choose a class variable $U$ occurring nowhere in $\varphi$ and different from all parameters (the list of class variables is infinite by Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations §symbols), and let $\varphi'$ result from $\varphi$ by replacing every occurrence of $u$ by $U$. An atomic part containing $u$, such as $u\in t$, $t\in u$, $u=t$ or $t=u$, becomes the same part with $U$ in place of $u$, which is again an atomic formula by Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations §formula, and no quantifier is added or changed. Hence $\varphi'$ is predicative, its free variables are those of $\varphi$ with $u$ replaced by $U$, and in particular its free set variables other than set-variable parameters are among $x_{1},\dots,x_{n}$. The set $a$ is a class, by Classes, Membership, Sets and Proper Classes §set; assign it to $U$. Read as in Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations §reading, each atomic part of $\varphi'$ then says about $a$ exactly what the corresponding part of $\varphi$ says, and the quantifiers of both formulas range over sets through the same set variables, none of which is $u$ or $U$; so $\varphi'$ and $\varphi$ express the same statement about $x_{1},\dots,x_{n}$, $a$ and the remaining parameters. Doing this for each set-variable parameter in turn yields a predicative formula whose parameters are all class variables, distinct from $x_{1},\dots,x_{n}$, and which, with each new class variable assigned the set assigned to the parameter it replaced, expresses the same statement as $\varphi$; a class $Z$ obtained for it at these classes therefore satisfies the conclusion of the clause comprehension of the statement for $\varphi$. So for the proof of the clause comprehension of the statement we may, and through the end of Step 2 do, assume that $Y_{1},\dots,Y_{m}$ are all class variables, and we keep writing $\varphi$ for the formula.

Step 1. Normal form.

Call a formula normal if it is predicative, is built by the rules of Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations §formula using only $\neg$, $\wedge$ and $\exists$ over set variables, every atomic part has the form $s\in t$ with $s$ a set variable and $t$ either a set variable different from $s$ or a class variable, and no two occurrences of $\exists$ in it bind the same variable. Its degree is the number of occurrences of $\neg$, $\wedge$ and $\exists$ in it. Abbreviations ($\forall$, $\Rightarrow$, $\Leftrightarrow$) are understood unfolded as in Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations §formula.

Let $\varphi$ be as in the clause comprehension of the statement, with the parameters $Y_{1},\dots,Y_{m}$ all class variables as arranged above. Since $\varphi$ is predicative, no class variable is quantified in it, so every class variable occurring in $\varphi$ is free and hence among $Y_{1},\dots,Y_{m}$. We transform $\varphi$ in three stages; in each, a fresh variable means a set variable occurring nowhere in the current formula, different from $x_{1},\dots,x_{n}$ and from every variable introduced before (the list of set variables is infinite by Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations §symbols).

Stage (1a). Replace each part $\exists v\,\psi$, one at a time, by $\exists v'\,\psi'$, where $v'$ is fresh and $\psi'$ results from $\psi$ by replacing the free occurrences of $v$ by $v'$. By elementary logic (renaming of bound variables, with no capture since $v'$ is fresh) the result is equivalent to the original under every assignment. Afterwards no two quantifiers bind the same variable and none binds any of $x_{1},\dots,x_{n}$.

Stage (1b). Replace each atomic part $s\in t$ in which $s$ is a class variable, or $s$ and $t$ are the same set variable, by $\exists z\,(z=s\wedge z\in t)$ with $z$ fresh. This is equivalent for every assignment of classes $S$ to $s$ and $T$ to $t$ (with $S=T$ if $s,t$ are the same variable), read as in Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations §reading: if $S\in T$, then $S$ is a set by Elements Are Sets, and the Empty Set and the Pair of Two Sets Exist and Are Unique §elements, so the set $z=S$ witnesses $z=S$ and $z\in T$; conversely, if some set $z$ satisfies $z=S$ and $z\in T$, then $S\in T$ by substitutivity of equality (Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations §symbols). The new part $z\in t$ has a set variable $z$ on the left, different from $t$.

Stage (1c). Replace each atomic part $s=t$ (with $s,t$ variables of any kind, including those created in (1b)) by $\forall z\,(z\in s\Leftrightarrow z\in t)$ with $z$ fresh. For classes $S,T$ assigned to $s,t$: if $S=T$ then for every set $z$, $z\in S$ if and only if $z\in T$, by substitutivity of equality (Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations §symbols); conversely, if this holds for every set $z$ then $S=T$ by the axiom of extensionality. The new atomic parts $z\in s$ and $z\in t$ have the set variable $z$ on the left, different from $s$ and $t$. This stage creates no equality and no membership with a class variable on the left.

Each replacement substitutes for an atomic part a formula with the same free variables and with new quantifiers over fresh set variables only, so by the replacement property of elementary logic the whole formula stays equivalent to $\varphi$ under every assignment, stays predicative, and keeps its free variables. The result $\varphi^{*}$ is therefore a normal formula, equivalent to $\varphi$ for all sets $x_{1},\dots,x_{n}$ and classes $Y_{1},\dots,Y_{m}$, whose free set variables are among $x_{1},\dots,x_{n}$, whose free class variables are among $Y_{1},\dots,Y_{m}$, and none of whose quantifiers binds any of $x_{1},\dots,x_{n}$.

Step 2. Induction on the degree.

Fix classes $Y_{1},\dots,Y_{m}$. We prove, by strong induction on the metatheoretic number $k$, the claim $C(k)$: for every normal formula $\psi$ of degree $k$ whose class variables are among $Y_{1},\dots,Y_{m}$, every $n\ge1$ and every list $x_{1},\dots,x_{n}$ of distinct set variables that contains every free set variable of $\psi$ and no variable bound by a quantifier of $\psi$, there is a class $Z$ with $\langle x_{1},\dots,x_{n}\rangle\in Z$ if and only if $\psi$, for all sets $x_{1},\dots,x_{n}$. The induction hypothesis is used for all such $n$ and lists, not only the given one.

Degree $0$, $\psi$ is $s\in t$ with $s,t$ distinct set variables. Both are free, so $s=x_{i}$ and $t=x_{j}$ with $i\ne j$. By (B1) there is $E$ with $(a,b)\in E$ if and only if $a\in b$. Lemma P applied to $n$, $i$, $j$ and $E$ gives $Z$ with $\langle x_{1},\dots,x_{n}\rangle\in Z$ if and only if $(x_{i},x_{j})\in E$, that is, if and only if $x_{i}\in x_{j}$.

Degree $0$, $\psi$ is $s\in Y_{l}$ with $s$ a set variable. Then $s=x_{i}$ for some $i$, and Lemma Q applied to $n$, $i$ and $Y_{l}$ gives the class.

Degree $k\ge1$, $\psi$ is $\neg\chi$. The formula $\chi$ is normal of degree $k-1$ with the same free and bound variables, so the induction hypothesis gives $Z_{0}$ for $\chi$ and the same list. By (B3) applied to $Z_{0}$ there is $Z$ with $p\in Z$ if and only if $p\notin Z_{0}$ for every set $p$; taking the set $p=\langle x_{1},\dots,x_{n}\rangle$, this holds if and only if $\chi$ fails, that is, if and only if $\psi$.

Degree $k\ge1$, $\psi$ is $(\chi\wedge\theta)$. Both $\chi$ and $\theta$ are normal of degree less than $k$, their free set variables are free in $\psi$ and their bound variables are bound in $\psi$, so the same list serves for both; the induction hypothesis gives $Z_{1}$ for $\chi$ and $Z_{2}$ for $\theta$. By (B2) applied to $Z_{1}$ and $Z_{2}$ there is $Z$ with $p\in Z$ if and only if $p\in Z_{1}$ and $p\in Z_{2}$; at $p=\langle x_{1},\dots,x_{n}\rangle$ this holds if and only if $\chi$ and $\theta$.

Degree $k\ge1$, $\psi$ is $\exists y\,\chi$ with $y$ a set variable. Since $y$ is bound in $\psi$, it is not in the list, so $x_{1},\dots,x_{n},y$ are $n+1$ distinct set variables. Every free set variable of $\chi$ is free in $\psi$ or equals $y$, so it lies in the extended list. Since $\psi$ is normal, $y$ is not bound again inside $\chi$, and the other bound variables of $\chi$ are bound in $\psi$, so the extended list contains no bound variable of $\chi$; and $\chi$ is normal of degree $k-1$. (If $y$ does not occur free in $\chi$ nothing changes.) The induction hypothesis, applied to $\chi$ with the list $x_{1},\dots,x_{n},y$, gives $W$ with $\langle x_{1},\dots,x_{n},y\rangle\in W$ if and only if $\chi$, for all sets $x_{1},\dots,x_{n},y$. By (B4) applied to $W$ there is $Z$ with $p\in Z$ if and only if there is a set $y$ with $(p,y)\in W$. Since $(\langle x_{1},\dots,x_{n}\rangle,y)=\langle x_{1},\dots,x_{n},y\rangle$, we get $\langle x_{1},\dots,x_{n}\rangle\in Z$ if and only if there is a set $y$ with $\chi$, which by Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations §reading is the reading of $\psi$.

Conclusion of the clause comprehension of the statement. Given $\varphi$, the list $x_{1},\dots,x_{n}$ and classes $Y_{1},\dots,Y_{m}$, Step 1 yields the normal formula $\varphi^{*}$ for which the list satisfies the hypotheses of $C(k)$, with $k$ the degree of $\varphi^{*}$. Step 2 gives $Z$ with $\langle x_{1},\dots,x_{n}\rangle\in Z$ if and only if $\varphi^{*}$, hence, by the equivalence of Step 1, if and only if $\varphi(x_{1},\dots,x_{n},Y_{1},\dots,Y_{m})$, for all sets $x_{1},\dots,x_{n}$.

Step 3. Uniqueness, the clause unique of the statement. Let $n=1$ and let $Z$ and $Z'$ both satisfy the condition. For every set $x_{1}$, $x_{1}\in Z$ holds if and only if $\varphi(x_{1},Y_{1},\dots,Y_{m})$, if and only if $x_{1}\in Z'$. By the axiom of extensionality, which requires agreement on sets only, $Z=Z'$.