Proof of Renaming and Substituting Variables in Predicative Formulas

Throughout, a formula is built by the rules of Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations (ii), an expression with abbreviations standing for the formula obtained by eliminating them as in Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations (vi), and formulas are read as in Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations (iv). Bound variables are renamed so that, in a predicative formula in $x_{0},\dots,x_{m-1}$, a quantifier is $\exists x_{m}$ applied to a predicative formula in $x_{0},\dots,x_{m}$. The inductions below run over this construction of $\varphi$, for all $k$ at once.

Invariance. We prove (v). If $\varphi$ is atomic, $s\in t$ or $s=t$, then each of $s$ and $t$ is a variable $x_{i}$ with $i<k$ or a parameter, and has the same value under both assignments, so $\varphi$ holds under both or under neither. Negation and conjunction preserve this. If $\varphi$ is $\exists x_{k}\,\psi$ with $\psi$ a predicative formula in $x_{0},\dots,x_{k}$, then for every set $z$ the two assignments, changed to assign $z$ to $x_{k}$, assign the same sets to $x_{0},\dots,x_{k}$; by induction $\psi$ holds under the one if and only if under the other, and so the same holds for $\varphi$.

Substitution of variables and parameters. We prove (iii), by induction on $\varphi$ for all $n$ and all $\tau_{0},\dots,\tau_{k-1}$ at once. The value of each $\tau_{i}$ under an assignment of sets to $x_{0},\dots,x_{n-1}$ is a set, so "$\varphi$ holds when each $x_{i}$ is assigned the value of $\tau_{i}$" is meaningful. If $\varphi$ is atomic, replacing its variables gives an atomic formula in the $\tau_{i}$ and the parameters, which holds exactly when $\varphi$ holds at the values of the $\tau_{i}$. Negation and conjunction commute with the replacement. Let $\varphi$ be $\exists x_{k}\,\psi$, with $\psi$ a predicative formula in $x_{0},\dots,x_{k}$, and put $\tau_{k}=x_{n}$. By induction, $\psi(\tau_{0},\dots,\tau_{k-1},x_{n})$ is a predicative formula in $x_{0},\dots,x_{n}$, and under an assignment that gives $x_{n}$ the set $z$ it holds if and only if $\psi$ holds when $x_{i}$ is assigned the value of $\tau_{i}$, $i<k$, and $x_{k}$ is assigned $z$; by (v), applied to $\psi$, it does not matter what this assignment gives the variables beyond $x_{k}$. Then $\varphi(\tau_{0},\dots,\tau_{k-1})$ is $\exists x_{n}\,\psi(\tau_{0},\dots,\tau_{k-1},x_{n})$, a predicative formula in $x_{0},\dots,x_{n-1}$, and quantifying over the sets $z$ gives its reading.

Renaming and weakening. (i) is the case $\tau_{i}=x_{\sigma(i)}$ of (iii), and (ii) is the case $\sigma(i)=i$ of (i).

Substitution of typed terms. For (iv), use the variables $x_{n},\dots,x_{n+k-1}$, which are none of $x_{0},\dots,x_{n-1}$; they are not free in $\gamma$ and occur in no $t_{i}$, as $\gamma$ and the $t_{i}$ are written with $x_{0},\dots,x_{n-1}$ and parameters. Let $i<k$. By Terms and Typed Terms under a Guard (iv), the condition $\gamma\wedge x_{n}=t_{i}$ on $x_{0},\dots,x_{n}$ is expressed by a predicative formula in $x_{0},\dots,x_{n}$; renaming $x_{n}$ to $x_{n+i}$ by (i) gives a predicative formula $\psi_{i}$ in $x_{0},\dots,x_{n+k-1}$ expressing $\gamma\wedge x_{n+i}=t_{i}$, since $\gamma$ and the value of $t_{i}$ depend only on the sets assigned to $x_{0},\dots,x_{n-1}$ (by (v) and Terms and Typed Terms under a Guard (i)). By (i) again, $\varphi(x_{n},\dots,x_{n+k-1})$ is a predicative formula in $x_{0},\dots,x_{n+k-1}$, and so is $\gamma$, by (ii). Let

$$\theta=\exists x_{n}\cdots\exists x_{n+k-1}\,\bigl(\gamma\wedge\psi_{0}\wedge\dots\wedge\psi_{k-1}\wedge\varphi(x_{n},\dots,x_{n+k-1})\bigr),$$

a predicative formula in $x_{0},\dots,x_{n-1}$. Fix an assignment of sets to $x_{0},\dots,x_{n-1}$. If $\theta$ holds, its witnesses $w_{0},\dots,w_{k-1}$ satisfy $\gamma$ and $w_{i}=t_{i}$, so $\varphi$ holds when each $x_{i}$ is assigned the value of $t_{i}$. Conversely, if $\gamma$ holds, each $t_{i}$ is a set by Terms and Typed Terms under a Guard (iii), and if moreover $\varphi$ holds at the values of the $t_{i}$, these values are witnesses for $\theta$. So $\theta$ expresses the condition.