Proof of The True Condition and Agreement of Two Classes at a Pair Are Predicative

Throughout, formulas written with the abbreviation $\forall$ stand for the formulas it abbreviates in Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations (ii), and are read as in Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations (iv). By Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations (v), a formula is predicative exactly when none of its quantifiers is applied to a class variable; hence a formula built from predicative formulas by $\neg$, $\wedge$ and quantifiers over set variables is again predicative.

The true condition. We prove (i). Let $n\ge0$, let $u$ be a set variable, and let $\tau$ be the formula

$$\forall u\,(u=u),$$

that is, $\neg\exists u\,\neg(u=u)$. It is built from the atomic formula $u=u$ by negations and a quantifier over the set variable $u$, so it is predicative. Its only variable $u$ is bound, so by Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations (iii) it has no free variables; in particular its free variables are among $x_{0},\dots,x_{n-1}$, and $\tau$ has no parameters. Read as in Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations (iv), $\tau$ says that every set $u$ satisfies $u=u$, which is true. So under every assignment of sets to $x_{0},\dots,x_{n-1}$ (for $n=0$, the empty assignment) both $\tau$ and the condition hold, and $\tau$ holds if and only if the condition does. By Conditions Expressed by a Predicative Formula, and Guards (ii), $\tau$ is a predicative formula in $x_{0},\dots,x_{n-1}$ expressing the condition that holds under every assignment.

Agreement at a pair. We prove (ii). Let $v$ be a set variable other than $x_{0}$; it differs from the class variables $S$ and $M$, the two lists of variables being disjoint by Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations (i). By Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (iii), applied with $S$ and with $M$ for $s$, $x_{0}$ for $t_{1}$ and $v$ for $t_{2}$, the formulas $(x_{0},v)\in S$ and $(x_{0},v)\in M$ are predicative, and when sets $a$ and $b$ are assigned to $x_{0}$ and $v$, they hold if and only if $(a,b)\in S$ and $(a,b)\in M$ respectively. Their free variables are among $x_{0}$, $v$ and $S$, respectively $M$. Indeed, in Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity the formula $(x_{0},v)\in S$ is $\pi_{2}[t/t']$, the renaming of the formula $\pi_{2}$ obtained by eliminating the ordered pair from $(t'_{1},t'_{2})\in S$, where $t'_{1}$ and $t'_{2}$ are distinct set variables other than $S$. Each formula $\theta$ inserted by Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations (viii) has its free variables among $z$ and the arguments of the symbol, and $z$ is bound in the inserted part $\exists z\,(\theta\wedge\alpha(z))$; so the free variables of $\pi_{2}$ are among $t'_{1}$, $t'_{2}$ and $S$. The renaming of Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (i) changes bound variables only and replaces the free occurrences of $t'_{1}$ and $t'_{2}$ by $t_{1}$ and $t_{2}$, here $x_{0}$ and $v$. Hence the free variables of $(x_{0},v)\in S$ are among $x_{0}$, $v$ and $S$, and likewise those of $(x_{0},v)\in M$ are among $x_{0}$, $v$ and $M$. Let $\psi$ be the formula

$$\exists v\,\bigl((x_{0},v)\in S\wedge(x_{0},v)\in M\bigr).$$

It is built from these two predicative formulas by $\wedge$ and a quantifier over the set variable $v$, so it is predicative, and since $v$ is bound in it, its free variables are among $x_{0}$ and the parameters $S$ and $M$ of the condition.

Let a set $a$ be assigned to $x_{0}$, the parameters $S$ and $M$ having their values. Read as in Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations (iv), the quantifier $\exists v$ over the set variable $v$ ranges over sets, so $\psi$ holds if and only if there is a set $b$ such that both conjuncts hold with $a$ assigned to $x_{0}$ and $b$ to $v$; by what was said above, this is the case if and only if there is a set $b$ with $(a,b)\in S$ and $(a,b)\in M$, that is, if and only if the condition holds at $a$. By Conditions Expressed by a Predicative Formula, and Guards (ii), $\psi$ is a predicative formula in $x_{0}$ expressing the condition.