Proof of Kit for def:iterated-operation-nbg

Throughout, formulas are written with abbreviations as in Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations (vi), and the given $x_{0},\dots,x_{n-1}$ are the first of distinct set variables $x_{0},x_{1},\dots$ as in Renaming and Substituting Variables in Predicative Formulas, so that $x_{0},\dots,x_{4}$ are distinct also when $n<5$. The parameters $\mathbb{N}$, $\le$ and $+$ of the statement are distinct class variables $Y$, $R$ and $P$, at their fixed values as in Conditions Expressed by a Predicative Formula, and Guards (i). Elements of $\mathbb{N}_{0}$ assigned to variables occur in the formulas below only to the left of $\in$ or inside ordered pairs, as The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion (iii) requires.

The formula. The formula is adapted from the published proof of Iterated Operations Are Given by a Predicative Formula. Let $c$, $z$, $w$, $o$, $t$, $r$, $q$, $u$, $b$ and $v$ be distinct set variables other than $x_{0},x_{1},\dots$. 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 (ii), 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) and Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (iv), each formula $w=(u,v)$, $(t_{1},t_{2})\in t_{3}$ and $((t_{1},t_{2}),t_{3})\in t_{4}$ written below is predicative and, when sets are assigned to the variables inside the pairs, holds if and only if the corresponding equation or membership of ordered pairs holds. Let $\mathrm{seg}(z,x_{2})$ be the formula of Induction over Finite Sets, and Predicative Formulas for the Segments [n] and for Finiteness (i) for the set variables $z$, $x_{2}$ and the class variables $Y$, $R$. Let $\mu$ be the formula 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 (vii), written below as $\mu(x_{1},c,x_{0})$, $\mu(x_{3},z,x_{0})$ and $\mu(x_{4},z,x_{0})$ with these variables in place of its three displayed variables, and with distinct set variables $h_{1},\dots,h_{5}$, other than all the variables named so far, in place of its bound variables $p$, $u$, $u'$, $v$ and $v'$, so that the distinctness required there holds. Let

$$\beta=\exists c\,\Bigl(\forall w\,\bigl(w\in c\Leftrightarrow\exists u\,\exists v\,(u\in x_{0}\wedge v\in x_{0}\wedge w=(u,v))\bigr)\wedge\mu(x_{1},c,x_{0})\Bigr),$$ $$\lambda(o)=o\in Y\wedge\forall t\,\bigl(t\in Y\Rightarrow(o,t)\in R\bigr),\qquad\rho_{1}=\exists o\,\exists u\,\bigl(\lambda(o)\wedge(o,u)\in x_{3}\wedge(o,u)\in x_{4}\bigr),$$ $$\rho_{2}=\forall r\,\forall q\,\forall o\,\forall u\,\forall b\,\forall v\,\Bigl(\bigl(r\in z\wedge q\in z\wedge\lambda(o)\wedge((r,o),q)\in P\wedge(r,u)\in x_{4}\wedge(q,b)\in x_{3}\wedge((u,b),v)\in x_{1}\bigr)\Rightarrow(q,v)\in x_{4}\Bigr),$$

and

$$\psi=\beta\wedge x_{2}\in Y\wedge\exists z\,\bigl(\mathrm{seg}(z,x_{2})\wedge\mu(x_{3},z,x_{0})\wedge\mu(x_{4},z,x_{0})\wedge\rho_{1}\wedge\rho_{2}\bigr).$$

Its parts are predicative, and the rest adds only atomic formulas, connectives and quantifiers over set variables; so $\psi$ is predicative by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (i), and its free variables are among $x_{0},\dots,x_{4}$, $Y$, $R$ and $P$.

Reading the parts. Assign sets $X$, $F$, $N$, $a$ and $s$ to $x_{0},\dots,x_{4}$. Five facts are used.

(a) $\beta$ holds if and only if $F$ is a binary operation on $X$. For every set $c$, the first conjunct of $\beta$ holds if and only if $c=X\times X$, by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (viii) applied to the class abstraction $X\times X$ of The Cartesian Product of Two Classes (i); and $X\times X$ is a set by Membership in a Cartesian Product, and the Cartesian Product of Two Sets Is a Set (ii). So $\beta$ holds if and only if $\mu(x_{1},c,x_{0})$ holds with $c$ assigned $X\times X$, that is, 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 (vii), if and only if $F$ is a map $X\times X\to X$, a binary operation on $X$ by Binary Operations on a Set (i). Also, $x_{2}\in Y$ holds if and only if $N\in\mathbb{N}$.

Since $\beta$ and $x_{2}\in Y$ are conjuncts of $\psi$, and the corresponding conditions are conjuncts of the condition of the statement, it remains to show, assuming that $F$ is a binary operation $\ast$ on $X$ and $N\in\mathbb{N}$, that the last conjunct of $\psi$ holds if and only if $a$ and $s$ are maps $[N]\to X$ with $s(1)=a(1)$ and $s(r+1)=s(r)\ast a(r+1)$ for every $r\in[N]$ with $r<N$. Note $1\in[N]$.

(b) For every set $o$, $\lambda(o)$ holds if and only if $o=1$: by The Order on Omega (i), $\lambda(o)$ says that $o\in\mathbb{N}$ and $o\le t$ for every $t\in\mathbb{N}$, and $1$ is the least natural number; a least element is unique, since $o\le1$ and $1\le o$ give $o=1$ by Order and Arithmetic of ℕ₀ in Flat Form (i), so $\lambda(o)$ implies $o=1$.

(c) For every set $z$, $\mathrm{seg}(z,N)$ holds if and only if $z=[N]$, by Induction over Finite Sets, and Predicative Formulas for the Segments [n] and for Finiteness (i), as $N\in\mathbb{N}\subseteq\mathbb{N}_{0}$; and $\mu(x_{3},z,x_{0})$, respectively $\mu(x_{4},z,x_{0})$, holds if and only if $a$, respectively $s$, is a map $z\to X$, 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 (vii).

(d) For $r\in\mathbb{N}_{0}$ and every set $q$, $((r,1),q)\in{+}$ if and only if $q=r+1$; and for $u,b\in X$ and every set $v$, $((u,b),v)\in{\ast}$ if and only if $v=u\ast b$. Both are Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (xi), for the binary operation $+$ on $\mathbb{N}_{0}$ (The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion (iv)) and for $\ast$ on $X$.

(e) For a map $g:[N]\to X$, every $r\in[N]$ and every set $u$, $(r,u)\in g$ if and only if $u=g(r)$, by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (x), and then $u\in X$. Moreover, for $r\in[N]$, $r+1\in[N]$ if and only if $r<N$.

If the last conjunct of $\psi$ holds. There is a set $z$ satisfying its five conjuncts. By (c), $z=[N]$ and $a$ and $s$ are maps $[N]\to X$. By $\rho_{1}$ there are sets $o$ and $u$ with $\lambda(o)$, $(o,u)\in a$ and $(o,u)\in s$; so $o=1$ by (b), and $u=a(1)$ and $u=s(1)$ by (e), whence $s(1)=a(1)$. Let $r\in[N]$ with $r<N$, so $r+1\in[N]$ by (e); put $u=s(r)$ and $b=a(r+1)$, both in $X$ by (e), and $v=u\ast b$. Then $r\in z$, $r+1\in z$, $\lambda(1)$ by (b), $((r,1),r+1)\in{+}$ and $((u,b),v)\in{\ast}$ by (d), and $(r,u)\in s$ and $(r+1,b)\in a$ by (e); so $\rho_{2}$, applied to $r$, $r+1$, $1$, $u$, $b$ and $v$, gives $(r+1,v)\in s$, that is, $s(r+1)=s(r)\ast a(r+1)$ by (e).

If the recursion holds. Let $a$ and $s$ be maps $[N]\to X$ with $s(1)=a(1)$ and $s(r+1)=s(r)\ast a(r+1)$ for every $r\in[N]$ with $r<N$, and take the set $[N]$ for $z$. Then $\mathrm{seg}([N],N)$, $\mu(x_{3},[N],x_{0})$ and $\mu(x_{4},[N],x_{0})$ hold by (c). For $\rho_{1}$, take $1$ and $a(1)$ for $o$ and $u$: $\lambda(1)$ holds by (b), and $(1,a(1))\in a$ and $(1,a(1))\in s$ by (e), as $s(1)=a(1)$. For $\rho_{2}$, let $r$, $q$, $o$, $u$, $b$ and $v$ be sets satisfying its hypotheses. Then $r,q\in[N]$, so $r\in\mathbb{N}_{0}$; $o=1$ by (b), so $q=r+1$ by (d); $u=s(r)$ and $b=a(r+1)$, both in $X$, by (e); and $v=u\ast b$ by (d). As $r+1\in[N]$, $r<N$ by (e), so $v=s(r)\ast a(r+1)=s(r+1)$, and $(q,v)\in s$ by (e). So the last conjunct of $\psi$ holds.

Hence, under every assignment of sets to $x_{0},\dots,x_{4}$, $\psi$ holds if and only if $x_{1}$ is a binary operation on $x_{0}$, $x_{2}\in\mathbb{N}$, $x_{3}$ and $x_{4}$ are maps $[x_{2}]\to x_{0}$, $x_{4}(1)=x_{3}(1)$, and $x_{4}(r+1)=x_{4}(r)\ast x_{3}(r+1)$ for every $r\in[x_{2}]$ with $r<x_{2}$, with $\ast$ the operation $x_{1}$; so $\psi$ is a predicative formula in $x_{0},\dots,x_{4}$ in the sense of Renaming and Substituting Variables in Predicative Formulas.

Any positions. By Renaming and Substituting Variables in Predicative Formulas (i), applied to $\psi$ with five variables and $\sigma(0)=i$, $\sigma(1)=j$, $\sigma(2)=k$, $\sigma(3)=l$ and $\sigma(4)=m$, the formula $\psi(x_{i},x_{j},x_{k},x_{l},x_{m})$ is a predicative formula in $x_{0},\dots,x_{n-1}$ that holds, under every assignment of sets to $x_{0},\dots,x_{n-1}$, exactly when the condition of the statement holds. This proves (i).