Proof of Substituting Variables and Set Parameters into Predicative Formulas, Extending Assignments, and Finiteness

(i). Let $\psi$ be a predicative formula expressing $\varphi$, as in Conditions Expressed by a Predicative Formula, and Guards (ii): its free variables are among $x_{1},\dots,x_{n}$ and the parameters of $\varphi$. By Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations (vi) we may take $\psi$ to be the formula obtained by eliminating its abbreviations, built by the rules of Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations (ii). Apply 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) to $\psi$ with $k=n$, the distinct set variables $x_{1},\dots,x_{n}$ in place of $v_{1},\dots,v_{n}$, and $\sigma_{1},\dots,\sigma_{n}$ in place of $y_{1},\dots,y_{n}$; this gives the predicative formula $\psi'=\psi[\sigma/x]$. The free variables of $\psi$ other than $x_{1},\dots,x_{n}$ are parameters, none of $x_{1},x_{2},\dots$, and stay unchanged; so the free variables of $\psi'$ are among $x_{1},\dots,x_{m}$, the parameters among $\sigma_{1},\dots,\sigma_{n}$ and the parameters of $\varphi$, which are the variables and parameters of the condition $\varphi(\sigma_{1},\dots,\sigma_{n})$ on $x_{1},\dots,x_{m}$.

Let sets be assigned to $x_{1},\dots,x_{m}$, the parameters having their fixed values, and let $b_{j}$ be the value of $\sigma_{j}$; each $b_{j}$ is a set, by hypothesis when $\sigma_{j}$ is a parameter. Apply Locality of Predicative Formulas: Truth Depends Only on the Values of the Free Variables (ii) to $\psi'$: its free set variables, namely the parameters among $\sigma_{1},\dots,\sigma_{n}$ and of $\varphi$ that are set variables, with their fixed values, and those of $x_{1},\dots,x_{m}$ that occur in it, play the role of the clause's $x_{i}$; the $x_{j}$, $j\le m$, that do not occur in $\psi'$ are its extra variables $y_{j}$; and the parameters that are class variables, with their fixed values, are its class variables $Z$. By that clause, the truth of $\psi'$ under this assignment is its truth under the assignment restricted to its free variables. A set is assigned to each class variable among $\sigma_{1},\dots,\sigma_{n}$, since such a $\sigma_{j}$ is a parameter with a set as its value; so 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 (i), $\psi'$ holds if and only if $\psi$ holds when each $x_{j}$, $j\le n$, is assigned $b_{j}$ and the parameters of $\varphi$ keep their values. Since $\psi$ expresses $\varphi$ and $b_{1},\dots,b_{n}$ are sets, this holds if and only if $\varphi(b_{1},\dots,b_{n})$. Thus $\psi'$ expresses $\varphi(\sigma_{1},\dots,\sigma_{n})$.

(ii). For $1\le j\le n$ the variable $\sigma_{j}=x_{\rho(j)}$ is one of $x_{1},\dots,x_{m}$, since $1\le\rho(j)\le m$, and its value under an assignment of sets to $x_{1},\dots,x_{m}$ is the set assigned to $x_{\rho(j)}$. So this is the case of (i) in which every $\sigma_{j}$ is a variable.

(iii). Apply (i) with $n+1$ in place of $n$, $n$ in place of $m$, $\sigma_{j}=x_{j}$ for $1\le j\le n$ and $\sigma_{n+1}=c$, a parameter whose value is a set. Under an assignment of sets to $x_{1},\dots,x_{n}$ the value of $\sigma_{j}$ is the set assigned to $x_{j}$ for $j\le n$, and that of $\sigma_{n+1}$ is $c$; so the condition $\varphi(\sigma_{1},\dots,\sigma_{n+1})$ is $\varphi(x_{1},\dots,x_{n},c)$, which is therefore expressed by a predicative formula.

(iv). The assignment gives $x_{i}$ the set $a_{i}$ for $1\le i\le n$ and $x_{n+1}$ the set $c$; so for $1\le i\le n+1$ the value of $x_{i}$ is one of the sets $a_{1},\dots,a_{n},c$, and the assignment is one of sets to $x_{1},\dots,x_{n+1}$ in the sense of Conditions Expressed by a Predicative Formula, and Guards (i).

(v). Let $1\le i\le n$. By Induction over Finite Sets, and Predicative Formulas for the Segments [n] and for Finiteness (ii), applied with the set variable $x_{i}$ in place of $A$ and with $X$, $Y$ and $R$ assigned $\mathbb{N}_{0}$, $\mathbb{N}$ and $\le$, there is a predicative formula $\mathrm{fin}(x_{i})$, whose free variables are among $x_{i}$, $X$, $Y$ and $R$, such that for every set $C$, $\mathrm{fin}(x_{i})$ holds when $C$ is assigned to $x_{i}$ if and only if $C$ is finite. Replacing $A$ by $x_{i}$ is a renaming of a set variable, which introduces no parameters; so the parameters of $\mathrm{fin}(x_{i})$, as a formula on $x_{1},\dots,x_{n}$, are among $X$, $Y$ and $R$, which are class variables and so none of $x_{1},x_{2},\dots$. Let sets $a_{1},\dots,a_{n}$ be assigned to $x_{1},\dots,x_{n}$. By Locality of Predicative Formulas: Truth Depends Only on the Values of the Free Variables (ii), applied with $x_{i}$ as the only free set variable of $\mathrm{fin}(x_{i})$ and the other variables among $x_{1},\dots,x_{n}$ as the further set variables, $\mathrm{fin}(x_{i})$ holds under this assignment if and only if it holds when $a_{i}$ is assigned to $x_{i}$, that is, if and only if $a_{i}$ is finite. So $\mathrm{fin}(x_{i})$ expresses the condition "$x_{i}$ is finite" on $x_{1},\dots,x_{n}$.