Proof of Iterated Operations Are Given by a Predicative Formula

Each result cited below is universally quantified over the data in its own statement, and is applied to the data named where it is cited.

Conventions. This proof concerns formulas of class theory: elements of $\mathbb{N}_{0}$ are assigned to set variables and are read as sets only in that sense, and in the formulas below a variable to which a number is assigned occurs only to the left of $\in$ or as a component of an ordered pair, as The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion §numbers-only requires. Let $w$, $n$, $a$, $X$, $F$, $Y$, $R$ and $P$ be as in the predicative clause, and let $z$, $s$, $o$, $t$, $k$, $j$, $u$, $b$ and $v$ be distinct set variables other than $w$, $n$ and $a$. 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 §pair-membership 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 §operation-membership, each formula $(t_{1},t_{2})\in t_{3}$ and $((t_{1},t_{2}),t_{3})\in t_{4}$ written below, with variables $t_{i}$ from those just listed, is predicative and, for sets assigned to the variables inside the pairs, holds if and only if the corresponding ordered pair is an element of the value of the variable to the right of $\in$; the elimination of the pairs introduces only bound variables, so its free variables are among the displayed ones.

The formula. Let $\mathrm{seg}(z,n)$ be a formula given by Induction over Finite Sets, and Predicative Formulas for the Segments [n] and for Finiteness §segment for the set variables $z$, $n$ and the class variables $Y$, $R$; it is predicative with free variables among $z$, $n$, $Y$ and $R$. Let $\mu(s,z,X)$ 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 §map with $s$, $z$ and $X$ in place of its variables $F$, $A$ and $B$, respectively, its bound set variables $p$, $u$, $u'$, $v$, $v'$ being chosen distinct from $w$, $n$, $a$, $z$ and $s$; by that clause it is predicative with free variables $s$, $z$ and $X$. Let $\lambda(o)$ be

$$o\in Y\wedge\forall t\,\bigl(t\in Y\Rightarrow(o,t)\in R\bigr),$$

let $\rho_{1}$ be

$$\exists o\,\exists u\,\bigl(\lambda(o)\wedge(o,u)\in a\wedge(o,u)\in s\bigr),$$

let $\rho_{2}$ be

$$\forall k\,\forall j\,\forall o\,\forall u\,\forall b\,\forall v\,\bigl((k\in z\wedge j\in z\wedge\lambda(o)\wedge((k,o),j)\in P\wedge(k,u)\in s\wedge(j,b)\in a\wedge((u,b),v)\in F)\Rightarrow(j,v)\in s\bigr),$$

and let $\mathrm{it}(w,n,a)$ be

$$\exists z\,\exists s\,\bigl(\mathrm{seg}(z,n)\wedge\mu(s,z,X)\wedge\rho_{1}\wedge\rho_{2}\wedge(n,w)\in s\bigr).$$

The parts $\mathrm{seg}(z,n)$, $\mu(s,z,X)$ and the pair formulas are predicative, so they apply no quantifier to a class variable, and the rest adds only atomic formulas, connectives and quantifiers over set variables; so $\lambda(o)$, $\rho_{1}$, $\rho_{2}$ and $\mathrm{it}(w,n,a)$ are predicative by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols §closure, no quantifier being applied to a class variable. The free variables of $\lambda(o)$ are among $o$, $Y$ and $R$; those of $\rho_{1}$ among $s$, $a$, $Y$ and $R$; those of $\rho_{2}$ among $z$, $s$, $a$, $F$, $P$, $Y$ and $R$; and so those of $\mathrm{it}(w,n,a)$ are among $w$, $n$, $a$, $X$, $F$, $Y$, $R$ and $P$.

Reading the parts. Now assign a set $X$, a binary operation $\ast$ on $X$, $\mathbb{N}$, $\le$ and $+$ to $X$, $F$, $Y$, $R$ and $P$, let $n\in\mathbb{N}$, let $a$ be a map from a set $E$ containing $[n]$ to $X$, so that $\operatorname{dom}a=E$ by Functions, Values of a Function, and Functions from One Class to Another §map and every element of $[n]$ lies in $E$ by Subclasses and Subsets §subclass, with $a_{k}$ denoting $a(k)$ for $k\in E$, and let $w$ be a set. By Intervals of Natural Numbers: Initial Segments, Adding One Element, Splitting and Shifting §segment, $[n]=\{k\in\mathbb{N}:k\le n\}$, a set by Sets and Maps: Ordinary Notation §set-builder, and by Class Abstraction: the Class of All Sets Satisfying a Predicative Formula §restricted and Class Abstraction: the Class of All Sets Satisfying a Predicative Formula §abstraction a set lies in $[n]$ if and only if it lies in $\mathbb{N}$ and is $\le n$. Here $1\in\mathbb{N}$ by The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion §sets, so $1\in[n]$ by Arithmetic and Order of the Natural Numbers §least, and $n\in[n]$ by Arithmetic and Order of the Natural Numbers §partial-order. Six facts are used.

(i) For every set $o$, $\lambda(o)$ holds if and only if $o=1$. By the conventions and The Order on Omega §order, $\lambda(o)$ says that $o\in\mathbb{N}$ and $o\le t$ for every $t\in\mathbb{N}$. The number $1$ satisfies this by Arithmetic and Order of the Natural Numbers §least; and if $o$ does, then $o\le1$ and $1\le o$, so $o=1$ by Arithmetic and Order of the Natural Numbers §partial-order.

(ii) 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 §segment, as $n\in\mathbb{N}\subseteq\mathbb{N}_{0}$; and for all sets $s$ and $z$, $\mu(s,z,X)$ holds if and only if $s$ is a map $s: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 §map.

(iii) For $k\in\mathbb{N}_{0}$ and every set $j$, $((k,1),j)\in{+}$ if and only if $j=k+1$: $+$ is a binary operation on $\mathbb{N}_{0}$ by The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion §operations, and $k,1\in\mathbb{N}_{0}$; so this is Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols §operation with $\mathbb{N}_{0}$, $+$, $k$, $1$ and $j$ in place of $a$, $\ast$, $u$, $v$ and $z$. Likewise, for $u,b\in X$ and every set $v$, $((u,b),v)\in{\ast}$ if and only if $v=u\ast b$, by the same clause with $X$ and $\ast$.

(iv) For a map $g$ with domain $D$, $k\in D$ and every set $u$, $(k,u)\in g$ if and only if $u=g(k)$, by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols §value; and then, when $g$ is a map to $X$, $u=g(k)\in\operatorname{ran}g\subseteq X$ by Relations, Domain, Range, Inverse and Composition §range, Class Abstraction: the Class of All Sets Satisfying a Predicative Formula §abstraction and Functions, Values of a Function, and Functions from One Class to Another §map.

(v) For $k\in[n]$: $k+1\in[n]$ if and only if $k<n$. Indeed $k+1\in\mathbb{N}$ by The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion §operations, and $k<k+1$ with no $d\in\mathbb{N}$ satisfying $k<d<k+1$, by Arithmetic and Order of the Natural Numbers §successor. If $k+1\le n$, then $k<n$ by Arithmetic and Order of the Natural Numbers §partial-order. If $k<n$, then $n<k+1$ is impossible, so $k+1<n$ or $k+1=n$ by Arithmetic and Order of the Natural Numbers §trichotomy, that is, $k+1\le n$ by Arithmetic and Order of the Natural Numbers §partial-order, so $k+1\in[n]$ by the description of $[n]$ above.

(vi) The restriction $a|_{[n]}$ is a map $a|_{[n]}:[n]\to X$ with $(a|_{[n]})(k)=a_{k}$ for every $k\in[n]$, and $\mathop{\ast}\limits_{k=1}^{n}a_{k}$ is the iterated operation of $a|_{[n]}$ by Iterated Operations: Finite Sums and Finite Products §restriction. Indeed, by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §restriction, $a|_{[n]}$ is a function with domain $[n]\cap E$ and $(a|_{[n]})(k)=a_{k}$ for every $k\in[n]\cap E$; by The Boolean Operations on Classes, Disjointness, and the Universal Class §operations and Class Abstraction: the Class of All Sets Satisfying a Predicative Formula §abstraction a set lies in $[n]\cap E$ if and only if it lies in $[n]$ and in $E$, that is, if and only if it lies in $[n]$, so $[n]\cap E=[n]$ by Class Theory NBG: the Axioms, Standing Conventions and Basic Notation §extensionality. If a set $v$ lies in the range of $a|_{[n]}$, then $(k,v)\in a|_{[n]}$ for some set $k$ by Relations, Domain, Range, Inverse and Composition §range and Class Abstraction: the Class of All Sets Satisfying a Predicative Formula §abstraction, so $k\in[n]$ and $v=(a|_{[n]})(k)=a_{k}$ by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols §value, and $a_{k}\in X$ by (iv); so the range of $a|_{[n]}$ is included in $X$ by Subclasses and Subsets §subclass, and $a|_{[n]}:[n]\to X$ by Functions, Values of a Function, and Functions from One Class to Another §map.

If $\mathrm{it}(w,n,a)$ holds. There are sets $z$ and $s$ satisfying its five conjuncts. By (ii), $z=[n]$ and $s$ is a map $s:[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 (i), and $u=a_{1}$ and $u=s(1)$ by (iv), whence $s(1)=a_{1}$. Let $k\in[n]$ with $k<n$, so $k+1\in[n]$ by (v); put $u=s(k)$, $b=a_{k+1}$, both in $X$ by (iv), and $v=u\ast b$. Then $k\in z$, $k+1\in z$, $\lambda(1)$ by (i), $((k,1),k+1)\in{+}$ by (iii), $(k,u)\in s$ and $(k+1,b)\in a$ by (iv), and $((u,b),v)\in{\ast}$ by (iii); so $\rho_{2}$, applied to $k$, $k+1$, $1$, $u$, $b$ and $v$, gives $(k+1,v)\in s$, that is, $s(k+1)=s(k)\ast a_{k+1}$ by (iv). Hence $s$ is the map of Iterating a Binary Operation along a Finite List §existence for $\ast$ and $a|_{[n]}$, which is a map $[n]\to X$ with $(a|_{[n]})(k)=a_{k}$ for $k\in[n]$ by (vi), by the uniqueness there. As $(n,w)\in s$ and $n\in[n]$, $w=s(n)$ by (iv), which is the iterated operation of $a|_{[n]}$ by Iterated Operations: Finite Sums and Finite Products §iterated, that is, $\mathop{\ast}\limits_{k=1}^{n}a_{k}$ by (vi).

If $w=\mathop{\ast}\limits_{k=1}^{n}a_{k}$. Let $s$ be the map of Iterating a Binary Operation along a Finite List §existence for $\ast$ and $a|_{[n]}$, a map $[n]\to X$ by (vi); its domain is the set $[n]$ by Functions, Values of a Function, and Functions from One Class to Another §map, so $s$ is a set by Images of Sets under Functions Are Sets, and a Function with a Set Domain Is a Set §function-set, and $w=s(n)$ by (vi) and Iterated Operations: Finite Sums and Finite Products §iterated; moreover $s(1)=a_{1}$ and $s(k+1)=s(k)\ast a_{k+1}$ for $k\in[n]$ with $k<n$, as $(a|_{[n]})(k)=a_{k}$ for $k\in[n]$ by (vi). Take $[n]$ and $s$ for $z$ and $s$. Then $\mathrm{seg}([n],n)$ and $\mu(s,[n],X)$ hold by (ii). For $\rho_{1}$, take $1$ and $a_{1}$ for $o$ and $u$: $\lambda(1)$ holds by (i), and $(1,a_{1})\in a$ and $(1,a_{1})\in s$ by (iv), as $1\in[n]$ and $s(1)=a_{1}$. For $\rho_{2}$, let $k$, $j$, $o$, $u$, $b$ and $v$ be sets satisfying its hypotheses. Then $k,j\in[n]$, so $k\in\mathbb{N}\subseteq\mathbb{N}_{0}$; $o=1$ by (i), so $j=k+1$ by (iii); $u=s(k)$ and $b=a_{k+1}$, both in $X$, by (iv); and $v=u\ast b$ by (iii). As $k+1\in[n]$, $k<n$ by (v), so $v=s(k)\ast a_{k+1}=s(k+1)$, and $(k+1,v)\in s$ by (iv), that is, $(j,v)\in s$. Finally $(n,w)\in s$ by (iv), as $n\in[n]$ and $w=s(n)$. So $\mathrm{it}(w,n,a)$ holds.

This proves the clause predicative.