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

This helper adopts the setting of The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion, which is used for (v); it is a statement of the metatheory about formulas and conditions. Let $x_{1},x_{2},\dots$ be distinct set variables. For a metatheoretic number $k\ge0$, conditions on $x_{1},\dots,x_{k}$, their parameters with their fixed values, and assignments of sets to $x_{1},\dots,x_{k}$ are as in Conditions Expressed by a Predicative Formula, and Guards (i), and a condition is expressed by a predicative formula as in Conditions Expressed by a Predicative Formula, and Guards (ii) with no displayed variables, predicative being meant for formulas written with abbreviations as in Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations (vi). Every parameter is a variable that is none of $x_{1},x_{2},\dots$. Throughout, the parameters have fixed values, as in Conditions Expressed by a Predicative Formula, and Guards (i). For a condition $\varphi$ on $x_{1},\dots,x_{k}$ and sets $a_{1},\dots,a_{k}$, $\varphi(a_{1},\dots,a_{k})$ means that $\varphi$ holds under the assignment of $a_{j}$ to $x_{j}$ for $1\le j\le k$. Let $n\ge0$ and $m\ge0$ be metatheoretic numbers.

(i) Let $\varphi$ be a condition on $x_{1},\dots,x_{n}$ expressed by a predicative formula. For $1\le j\le n$ let $\sigma_{j}$ be either one of the variables $x_{1},\dots,x_{m}$ or a parameter whose fixed value is a set; under an assignment of sets to $x_{1},\dots,x_{m}$, the value of $\sigma_{j}$ is the set assigned to it if it is one of $x_{1},\dots,x_{m}$, and its fixed value if it is a parameter. Then the condition $\varphi(\sigma_{1},\dots,\sigma_{n})$ on $x_{1},\dots,x_{m}$, that is, "$\varphi$ holds with each $x_{j}$ given the value of $\sigma_{j}$", is expressed by a predicative formula.

(ii) Let $\varphi$ be a condition on $x_{1},\dots,x_{n}$ expressed by a predicative formula, and let $\rho$ be a map from $\{1,\dots,n\}$ to $\{1,\dots,m\}$. Then the condition $\varphi(x_{\rho(1)},\dots,x_{\rho(n)})$ on $x_{1},\dots,x_{m}$, that is, "$\varphi$ holds with each $x_{j}$ given the set assigned to $x_{\rho(j)}$", is expressed by a predicative formula.

(iii) Let $\varphi$ be a condition on $x_{1},\dots,x_{n+1}$ expressed by a predicative formula, and let $c$ be a parameter whose fixed value is a set. Then the condition $\varphi(x_{1},\dots,x_{n},c)$ on $x_{1},\dots,x_{n}$, that is, "$\varphi$ holds with each $x_{j}$, $j\le n$, keeping its set and with $x_{n+1}$ given the value $c$", is expressed by a predicative formula.

(iv) Let $a_{1},\dots,a_{n}$ and $c$ be sets. Then giving $x_{i}$ the set $a_{i}$ for $1\le i\le n$ and $x_{n+1}$ the set $c$ is an assignment of sets to $x_{1},\dots,x_{n+1}$: for every $i$ with $1\le i\le n+1$, the value it gives $x_{i}$ is a set.

(v) Let $X$, $Y$ and $R$ be distinct class variables, parameters with the fixed values $\mathbb{N}_{0}$, $\mathbb{N}$ and the order $\le$ of $\mathbb{N}_{0}$, as in The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion (ii) and The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion (v). For every $i$ with $1\le i\le n$, the condition "$x_{i}$ is finite" on $x_{1},\dots,x_{n}$ is expressed by a predicative formula whose parameters are among $X$, $Y$ and $R$.