Proof of Values of Variables and Set Parameters Are Sets; a Predicative Monotonicity Condition

Throughout, formulas written with the abbreviations $\forall$ and $\Rightarrow$ stand for the formulas they abbreviate 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.

Values of variables and set parameters. We prove (i). Fix an assignment of sets to $x_{0},\dots,x_{n-1}$; by Conditions Expressed by a Predicative Formula, and Guards (i), the value of a variable $x_{j}$ is the set assigned to it, and the value of a parameter is its fixed value, given before the assignment and unaffected by it. If $\tau$ is a variable $x_{j}$ with $j<n$, then $x_{j}$ is among $x_{0},\dots,x_{n-1}$, so its value is the set assigned to it. If $\tau$ is a parameter whose value is a set, its value is that set, whatever is assigned to $x_{0},x_{1},\dots$. In both cases the value of $\tau$ is a set.

The monotonicity condition. We prove (ii). Let $m$, $a$ and $b$ be distinct set variables other than $x_{0}$; they differ from the class variables $F$, $\mathbb{N}$, $\le_{\omega}$ and $\overline{\le}$. 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 $\le_{\omega}$ for $s$, $m$ for $t_{1}$ and $x_{0}$ for $t_{2}$, and with $F$, $F$, $\overline{\le}$ for $s$ and the pairs $m,a$, then $x_{0},b$, then $a,b$ for $t_{1},t_{2}$, the four formulas

$$(m,x_{0})\in{\le_{\omega}},\qquad (m,a)\in F,\qquad (x_{0},b)\in F,\qquad (a,b)\in{\overline{\le}}$$

are predicative, and when sets are assigned to the two components each holds if and only if the ordered pair of the assigned sets is an element of the value of the class variable on the right. Each is the renaming $\pi_{2}[t/t']$ 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 (iii), so, by the construction 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 (i), its free variables are among its two components and the class variable on the right. The formula $m\in\mathbb{N}$ is atomic, hence predicative, with free variables $m$ and $\mathbb{N}$. Let $\psi$ be the formula

$$\forall m\,\Bigl(\bigl(m\in\mathbb{N}\wedge(m,x_{0})\in{\le_{\omega}}\bigr)\Rightarrow\exists a\,\exists b\,\bigl((m,a)\in F\wedge(x_{0},b)\in F\wedge(a,b)\in{\overline{\le}}\bigr)\Bigr).$$

It is built from the formula $m\in\mathbb{N}$ and the four displayed formulas by $\neg$, $\wedge$ and quantifiers over the set variables $m$, $a$ and $b$, so it is predicative; and since $m$, $a$ and $b$ are bound in it, its free variables are among $x_{0}$ and the parameters $F$, $\mathbb{N}$, $\le_{\omega}$ and $\overline{\le}$ of the condition.

Let a set $c$ be assigned to $x_{0}$, the parameters having their values. Read as in Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations (iv), the quantifiers over $m$, $a$ and $b$ range over sets, so $\psi$ holds if and only if for every set $d$ with $d\in\mathbb{N}$ and $(d,c)\in{\le_{\omega}}$ there are sets $e$ and $f$ with $(d,e)\in F$, $(c,f)\in F$ and $(e,f)\in{\overline{\le}}$, by what was said of the four pair-membership formulas; that is, if and only if the condition holds at $c$. By Conditions Expressed by a Predicative Formula, and Guards (ii), $\psi$ is a predicative formula in $x_{0}$ expressing the condition.