Proof of Multiplication on ℕ₀ as a Recursion

Throughout, $m+u\in\mathbb{N}_{0}$ for $m,u\in\mathbb{N}_{0}$ by Addition on Omega (i), so sums of elements of $\mathbb{N}_{0}$ are sets, as are $0=\emptyset$ and all elements of classes.

The step map. Let $m\in\mathbb{N}_{0}$. No quantifier of the formula defining $\tau_{m}$ in Multiplication on Omega (i), nor of the class abstractions defining $\mathbb{N}_{0}$ and ${+}$ in The Class Omega of Natural Numbers with Zero (i) and Addition on Omega (i), binds a class variable, so that formula is predicative by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (i), and by Class Abstraction: the Class of All Sets Satisfying a Predicative Formula (i) a set $p$ lies in $\tau_{m}$ if and only if $p=((n,u),u+m)$ for some $n,u\in\mathbb{N}_{0}$. Hence every element of $\tau_{m}$ is an ordered pair, and $\tau_{m}$ is a relation. Let $(a,v)$ and $(a,v')$ be elements of $\tau_{m}$, say $(a,v)=((n,u),u+m)$ and $(a,v')=((n',u'),u'+m)$ with $n,u,n',u'\in\mathbb{N}_{0}$. By The Characteristic Property of Ordered Pairs and Nested Tuples of Sets (i), $a=(n,u)$, $v=u+m$, $a=(n',u')$ and $v'=u'+m$; then $(n,u)=(n',u')$ gives $u=u'$ by the same lemma, and $v=v'$. So $\tau_{m}$ is a function. By Relations, Domain, Range, Inverse and Composition (ii), a set $a$ lies in the domain of $\tau_{m}$ if and only if $(a,v)\in\tau_{m}$ for some set $v$, that is, by the characteristic property again, if and only if $a=(n,u)$ for some $n,u\in\mathbb{N}_{0}$ (the companion being $v=u+m$); by The Cartesian Product of Two Classes (i) this says $a\in\mathbb{N}_{0}\times\mathbb{N}_{0}$, so $\operatorname{dom}\tau_{m}=\mathbb{N}_{0}\times\mathbb{N}_{0}$. Every second coordinate $u+m$ lies in $\mathbb{N}_{0}$, so the range of $\tau_{m}$ (Relations, Domain, Range, Inverse and Composition (iii)) is included in $\mathbb{N}_{0}$. By Functions, Values of a Function, and Functions from One Class to Another (iii), $\tau_{m}:\mathbb{N}_{0}\times\mathbb{N}_{0}\to\mathbb{N}_{0}$ is a map.

Values of the step map. Let $m,k,v\in\mathbb{N}_{0}$. Taking $n=k$ and $u=v$ in the description of the elements of $\tau_{m}$ just obtained, $((k,v),v+m)\in\tau_{m}$; and $(k,v)\in\mathbb{N}_{0}\times\mathbb{N}_{0}$ by Maps between Classes: Values, Pairs, Extensionality, Restrictions, Constant Maps and Preimages (viii). Since $\tau_{m}:\mathbb{N}_{0}\times\mathbb{N}_{0}\to\mathbb{N}_{0}$ is a map by (i) and $v+m$ is a set, Maps between Classes: Values, Pairs, Extensionality, Restrictions, Constant Maps and Preimages (ii) gives $\tau_{m}((k,v))=v+m$.

The recursion step. Let $m\in\mathbb{N}_{0}$ and let $f:\mathbb{N}_{0}\to\mathbb{N}_{0}$ be a map. For $k\in\mathbb{N}_{0}$ we have $f(k)\in\mathbb{N}_{0}$ by Maps between Classes: Values, Pairs, Extensionality, Restrictions, Constant Maps and Preimages (i), so (ii), with $f(k)$ in place of $v$, gives

$$\tau_{m}((k,f(k)))=f(k)+m.$$

Hence, for each $k\in\mathbb{N}_{0}$, the equations $f(S(k))=f(k)+m$ and $f(S(k))=\tau_{m}((k,f(k)))$ have the same right-hand side. As the elements of $\mathbb{N}_{0}$ are sets, both conditions range over the same $k$, and they are equivalent.

The product as a value. Let $m,n\in\mathbb{N}_{0}$. By Multiplication on Omega (i), $m\cdot n$ is the unique set $z$ such that

$$\exists f\,\bigl(f:\mathbb{N}_{0}\to\mathbb{N}_{0}\wedge f(0)=0\wedge\forall k\,(k\in\mathbb{N}_{0}\Rightarrow f(S(k))=f(k)+m)\wedge z=f(n)\bigr),$$

where $f$ and $k$ are set variables, so that the quantifiers read "there is a set $f$" and "for every set $k$" (Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations (iv)). So $m\cdot n$ is a set, and this formula with $z=m\cdot n$ provides a set $f$ with the four properties asserted.

Uniqueness of the value. Let $m$, $n$, $z$, $z'$, $f$ and $h$ be as in the hypotheses. By (iii), $f(S(k))=\tau_{m}((k,f(k)))$ and $h(S(k))=\tau_{m}((k,h(k)))$ for every $k\in\mathbb{N}_{0}$. Now $\mathbb{N}_{0}$ is a set by Omega Is the Least Inductive Class: It Is a Set, Induction from Zero, the Peano Properties, and Transitivity (i), $0\in\mathbb{N}_{0}$ by Omega Is the Least Inductive Class: It Is a Set, Induction from Zero, the Peano Properties, and Transitivity (ii), and $\tau_{m}:\mathbb{N}_{0}\times\mathbb{N}_{0}\to\mathbb{N}_{0}$ is a map by (i). So The Recursion Theorem on Omega (i), applied with $a=\mathbb{N}_{0}$, $c=0$ and $\tau_{m}$ as the map $g$ there, gives exactly one map $F:\mathbb{N}_{0}\to\mathbb{N}_{0}$ with $F(0)=0$ and $F(S(k))=\tau_{m}((k,F(k)))$ for every $k\in\mathbb{N}_{0}$. Both $f$ and $h$ are such maps, so $f=h$, which gives $f(n)=h(n)$ for $n\in\mathbb{N}_{0}$, and therefore

$$z=f(n)=h(n)=z'.$$

The product through pairs. Let $m,n\in\mathbb{N}_{0}$, let $z$ be a set, and let $f:\mathbb{N}_{0}\to\mathbb{N}_{0}$ be a map. We first show that the condition

$$(\ast)\qquad\text{for every set } k\in\mathbb{N}_{0} \text{ and every set } b \text{ with } (k,b)\in f \text{ there is a set } c \text{ with } ((b,m),c)\in{+} \text{ and } (S(k),c)\in f$$

holds if and only if $f(S(k))=f(k)+m$ for every $k\in\mathbb{N}_{0}$. Two facts are used: for sets $b$ and $c$ with $b\in\mathbb{N}_{0}$, $((b,m),c)\in{+}$ if and only if $c=b+m$, by The Number n Lies in the Segment [n], and Membership in the Addition Class on ω (ii); and $S(k)\in\mathbb{N}_{0}$ for $k\in\mathbb{N}_{0}$, by Omega Is the Least Inductive Class: It Is a Set, Induction from Zero, the Peano Properties, and Transitivity (ii). Suppose $(\ast)$, and let $k\in\mathbb{N}_{0}$. By Maps between Classes: Values, Pairs, Extensionality, Restrictions, Constant Maps and Preimages (i), $f(k)\in\mathbb{N}_{0}$ and $(k,f(k))\in f$, so $(\ast)$ with $b=f(k)$ gives a set $c$ with $((f(k),m),c)\in{+}$, whence $c=f(k)+m$, and with $(S(k),c)\in f$, whence $c=f(S(k))$ by Maps between Classes: Values, Pairs, Extensionality, Restrictions, Constant Maps and Preimages (ii). Thus $f(S(k))=f(k)+m$. Conversely, suppose these equations hold, and let $k\in\mathbb{N}_{0}$ and $b$ be a set with $(k,b)\in f$. Then $b=f(k)$ by Maps between Classes: Values, Pairs, Extensionality, Restrictions, Constant Maps and Preimages (ii), so $b\in\mathbb{N}_{0}$ by Maps between Classes: Values, Pairs, Extensionality, Restrictions, Constant Maps and Preimages (i). The set $c=f(S(k))=b+m$ satisfies $((b,m),c)\in{+}$ and, by Maps between Classes: Values, Pairs, Extensionality, Restrictions, Constant Maps and Preimages (i), $(S(k),c)\in f$, as $(\ast)$ requires.

Moreover $(0,0)\in f$ if and only if $f(0)=0$, and $(n,z)\in f$ if and only if $z=f(n)$, by Maps between Classes: Values, Pairs, Extensionality, Restrictions, Constant Maps and Preimages (ii), since $0,n\in\mathbb{N}_{0}$. So the right-hand side of (vi) says exactly that there is a set $f$ such that $f:\mathbb{N}_{0}\to\mathbb{N}_{0}$ is a map, $f(0)=0$, $f(S(k))=f(k)+m$ for every set $k\in\mathbb{N}_{0}$, and $z=f(n)$. If $z=m\cdot n$, the set $f$ given by (iv) is such a set. Conversely, given such a set $f$, (iv) gives a set $f'$ with the same first three properties and $m\cdot n=f'(n)$, and (v), applied with these $m,n\in\mathbb{N}_{0}$ to $f$ with $z$ and to $f'$ with $m\cdot n$, gives $z=m\cdot n$.

Membership in the multiplication. By Multiplication on Omega (i), ${\cdot}$ is the class abstraction

$${\cdot}=\{p:\exists m\,\exists n\,(m\in\mathbb{N}_{0}\wedge n\in\mathbb{N}_{0}\wedge p=((m,n),m\cdot n))\},$$

and no quantifier of its formula, nor of the class abstractions defining $\mathbb{N}_{0}$ and ${+}$ in The Class Omega of Natural Numbers with Zero (i) and Addition on Omega (i), binds a class variable, so the formula is predicative by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (i). By Class Abstraction: the Class of All Sets Satisfying a Predicative Formula (i), a set $p$ lies in ${\cdot}$ if and only if this formula holds for $p$, that is, reading the quantifiers over the set variables $m$ and $n$ as in Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations (iv), if and only if there are sets $m$ and $n$ with $m\in\mathbb{N}_{0}$, $n\in\mathbb{N}_{0}$ and $p=((m,n),m\cdot n)$.

The step condition is predicative. Let $k$, $b$, $c$ and $s$ be set variables, distinct from one another and from $x_{0},\dots,x_{5}$, and let $Y$ be a class variable. The formulas

$$s=S(k),\qquad (s,c)\in x_{5},\qquad (k,b)\in x_{5},\qquad ((b,x_{1}),c)\in Y$$

are predicative by Atomic Predicative Formulas: Equality with Unordered Pairs, Singletons and Successors (iii), 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) (twice) 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); when sets are assigned to their set variables, they hold exactly when $s$ is the successor of $k$, $(s,c)$ is an element of $x_{5}$, $(k,b)$ is an element of $x_{5}$, and $((b,x_{1}),c)$ is an element of $Y$. In the last formula, the ordered pairs having been eliminated, $Y$ occurs only in atomic parts $w\in Y$ with $w$ a set variable. Replacing each of them by the membership formula of the class ${+}$ at $w$ is the elimination of the class term from $((b,x_{1}),c)\in{+}$ prescribed by Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations (ix), and by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (viii) the result holds exactly when $((b,x_{1}),c)\in{+}$. The membership formula of ${+}$ has no free class variable, since ${+}$ is defined in Addition on Omega (i) by a class abstraction without parameters; so the replacement puts the class term ${+}$ in place of $Y$ and introduces no free class variable, and $\psi$ below has none. Likewise $k\in\mathbb{N}_{0}$ stands for the membership formula of the class $\mathbb{N}_{0}$ at $k$, which has no free class variable, $\mathbb{N}_{0}$ being defined in The Class Omega of Natural Numbers with Zero (i) by a class abstraction without parameters, and which holds exactly when $k\in\mathbb{N}_{0}$. Let $\psi$ be the formula

$$\forall k\,\Bigl(k\in\mathbb{N}_{0}\Rightarrow\forall b\,\bigl((k,b)\in x_{5}\Rightarrow\exists c\,\bigl(((b,x_{1}),c)\in{+}\wedge\exists s\,(s=S(k)\wedge(s,c)\in x_{5})\bigr)\bigr)\Bigr).$$

No quantifier in $\psi$ binds a class variable, those inside the class abstractions defining $\mathbb{N}_{0}$ and ${+}$ in The Class Omega of Natural Numbers with Zero (i) and Addition on Omega (i) included, so $\psi$ is predicative by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (i). Its free variables are among $x_{1}$ and $x_{5}$, hence among $x_{0},\dots,x_{5}$, and no class variable occurs free in it, the class terms having been eliminated. Reading its quantifiers over sets (Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations (iv)) and its parts as just described, and noting that $\exists s\,(s=S(k)\wedge(s,c)\in x_{5})$ holds exactly when $(S(k),c)\in x_{5}$, under every assignment of sets to $x_{0},\dots,x_{5}$ the formula $\psi$ holds if and only if for every set $k\in\mathbb{N}_{0}$ and every set $b$ with $(k,b)\in x_{5}$ there is a set $c$ with $((b,x_{1}),c)\in{+}$ and $(S(k),c)\in x_{5}$. So $\psi$ is a predicative formula in $x_{0},\dots,x_{5}$, in the sense of Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations (v), that holds exactly when the condition of (viii) holds.

The defining condition is predicative. Let $A$ and $B$ be distinct class variables. The bound variables of $\mu$ below and of $\psi$ are renamed apart, where necessary, from each other and from $x_{0},\dots,x_{5}$, and the remaining bound variables below are set variables distinct from all of these. 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), with $x_{5}$ as $F$, the formula $\mu(x_{5},A,B)$ is predicative, and for classes $A$ and $B$ it holds exactly when $x_{5}:A\to B$ is a map. In it, $A$ and $B$ occur only in atomic parts $u\in A$ and $v\in B$ with $u$ and $v$ set variables; replacing these by the membership formula of $\mathbb{N}_{0}$ at $u$ and at $v$ is the elimination of the class term from $\mu(x_{5},\mathbb{N}_{0},\mathbb{N}_{0})$ (Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations (ix)), and by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (viii) the result holds exactly when $x_{5}:\mathbb{N}_{0}\to\mathbb{N}_{0}$ is a map. Next, $0=\emptyset$ by The Class Omega of Natural Numbers with Zero (ii), and a set $e$ is $\emptyset$ exactly when $\forall w\,(w\notin e)$, by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (iii); so the formula $\exists e\,(\forall w\,(w\notin e)\wedge(e,e)\in x_{5})$, predicative 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 (iii), holds exactly when $(0,0)\in x_{5}$. By the same clause, the formula $(x_{2},x_{4})\in x_{5}$ is predicative and holds exactly when $(x_{2},x_{4})$ is an element of $x_{5}$. Let $\chi$ be the formula

$$\mu(x_{5},\mathbb{N}_{0},\mathbb{N}_{0})\wedge\exists e\,(\forall w\,(w\notin e)\wedge(e,e)\in x_{5})\wedge\psi\wedge(x_{2},x_{4})\in x_{5}.$$

No quantifier in it binds a class variable, so it is predicative by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (i); its free variables are among $x_{1},x_{2},x_{4},x_{5}$, hence among $x_{0},\dots,x_{5}$, and no class variable occurs free in it, the class terms having been eliminated. By the readings of its four conjuncts, the third being (viii) as just proved, under every assignment of sets to $x_{0},\dots,x_{5}$ the formula $\chi$ holds if and only if $x_{5}:\mathbb{N}_{0}\to\mathbb{N}_{0}$ is a map, $(0,0)\in x_{5}$, the condition of (viii) holds, and $(x_{2},x_{4})\in x_{5}$. So $\chi$ is a predicative formula in $x_{0},\dots,x_{5}$, in the sense of Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations (v), that holds exactly when the condition of (ix) holds.