Renaming and Substituting Variables in Predicative Formulas

In the setting of Routine Facts Used Without Citation: Arithmetic, Maps, Predicativity and Indices, let $x_{0},x_{1},\dots$ be distinct set variables. For a metatheoretic number $m\ge0$, a predicative formula in $x_{0},\dots,x_{m-1}$ is a predicative formula that expresses a condition on $x_{0},\dots,x_{m-1}$, with no displayed variables, as in Conditions Expressed by a Predicative Formula, and Guards (ii). There, and for guards and typed terms below, $x_{0},\dots,x_{m-1}$ take the place of the variables $x_{1},\dots,x_{N}$ of Conditions Expressed by a Predicative Formula, and Guards (i), whose parameters, fixed values and assignments are used throughout. Let $k,n\ge0$ be metatheoretic numbers and let $\varphi$ be a predicative formula in $x_{0},\dots,x_{k-1}$.

(i) Renaming. Let $\sigma$ assign to each $i<k$ an index $\sigma(i)<n$, not necessarily injectively, and let $\varphi(x_{\sigma(0)},\dots,x_{\sigma(k-1)})$ be obtained from $\varphi$ by replacing each free occurrence of $x_{i}$ by $x_{\sigma(i)}$, $i<k$, bound variables being renamed where necessary so that none is captured. It is a predicative formula in $x_{0},\dots,x_{n-1}$, and under every assignment of sets to $x_{0},\dots,x_{n-1}$ it holds if and only if $\varphi$ holds when each $x_{i}$, $i<k$, is assigned the set assigned to $x_{\sigma(i)}$ (this restates Substituting Variables and Set Parameters into Predicative Formulas, Extending Assignments, and Finiteness (ii) for formulas indexed from $x_{0}$).

(ii) Weakening. If $k\le n$, then $\varphi$ itself is a predicative formula in $x_{0},\dots,x_{n-1}$.

(iii) Substitution. For each $i<k$ let $\tau_{i}$ be a variable $x_{j}$ with $j<n$ or a parameter whose value is a set, and let $\varphi(\tau_{0},\dots,\tau_{k-1})$ be obtained from $\varphi$ by replacing each free occurrence of $x_{i}$ by $\tau_{i}$, $i<k$, bound variables being renamed as above. It is a predicative formula in $x_{0},\dots,x_{n-1}$, and under every assignment of sets to $x_{0},\dots,x_{n-1}$ it holds if and only if $\varphi$ holds when each $x_{i}$, $i<k$, is assigned the value of $\tau_{i}$ (this restates Substituting Variables and Set Parameters into Predicative Formulas, Extending Assignments, and Finiteness (i), and with it Substituting Variables and Set Parameters into Predicative Formulas, Extending Assignments, and Finiteness (iii), for formulas indexed from $x_{0}$).

(iv) Substitution of typed terms. Let $\gamma$ be a guard on $x_{0},\dots,x_{n-1}$, and for each $i<k$ let $t_{i}$ be a term of some type $A_{i}$ under $\gamma$. Then the condition

$$\gamma\ \text{holds, and}\ \varphi\ \text{holds when each}\ x_{i},\ i<k,\ \text{is assigned the value of}\ t_{i},$$

on $x_{0},\dots,x_{n-1}$ is expressed by a predicative formula in $x_{0},\dots,x_{n-1}$.

(v) Invariance. Under two assignments that assign the same sets to $x_{0},\dots,x_{k-1}$, whatever they assign to the other variables $x_{k},x_{k+1},\dots$, and under which the parameters keep their values, $\varphi$ holds under the one if and only if it holds under the other (this restates Locality of Predicative Formulas: Truth Depends Only on the Values of the Free Variables (i) and Locality of Predicative Formulas: Truth Depends Only on the Values of the Free Variables (ii) for assignments to $x_{0},x_{1},\dots$).