Multiplication on ℕ₀ as a Recursion

In the setting of Routine Facts Used Without Citation: Arithmetic, Maps, Predicativity and Indices, let $\mathbb{N}_{0}$ and $0$ be as in The Class Omega of Natural Numbers with Zero (i) and The Class Omega of Natural Numbers with Zero (ii), $S(x)$ the successor of a set $x$, $(u,v)$ the ordered pair, and $F(u)$ the value of a map $F$ at $u$. Let ${+}$ and ${\cdot}$ be the addition and the multiplication on $\mathbb{N}_{0}$, written $u+v$ and $m\cdot n$, and for $m\in\mathbb{N}_{0}$ let $\tau_{m}$ be the class of that definition,

$$\tau_{m}=\{p:\exists n\,\exists u\,(n\in\mathbb{N}_{0}\wedge u\in\mathbb{N}_{0}\wedge p=((n,u),u+m))\}.$$

In the last two clauses, $x_{0},\dots,x_{5}$ are distinct set variables; a predicative formula in $x_{0},\dots,x_{5}$ is a predicative formula with no class variable free and with free variables among $x_{0},\dots,x_{5}$, and it holds exactly when a condition on $x_{0},\dots,x_{5}$ holds if, for every assignment of sets to $x_{0},\dots,x_{5}$, it holds if and only if the condition does.

(i) The step map. For every $m\in\mathbb{N}_{0}$, $\tau_{m}:\mathbb{N}_{0}\times\mathbb{N}_{0}\to\mathbb{N}_{0}$ is a map, $\mathbb{N}_{0}\times\mathbb{N}_{0}$ being the Cartesian product.

(ii) Values of the step map. For all $m,k,v\in\mathbb{N}_{0}$,

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

(iii) The recursion step. Let $m\in\mathbb{N}_{0}$ and let $f:\mathbb{N}_{0}\to\mathbb{N}_{0}$ be a map. Then $f(S(k))=f(k)+m$ for every set $k\in\mathbb{N}_{0}$ if and only if $f(S(k))=\tau_{m}((k,f(k)))$ for every $k\in\mathbb{N}_{0}$.

(iv) The product as a value. For all $m,n\in\mathbb{N}_{0}$, $m\cdot n$ is a set, and 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 $m\cdot n=f(n)$.

(v) Uniqueness of the value. Let $m,n\in\mathbb{N}_{0}$ and let $z$ and $z'$ be classes. Suppose 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)$; and there is a set $h$ such that $h:\mathbb{N}_{0}\to\mathbb{N}_{0}$ is a map, $h(0)=0$, $h(S(k))=h(k)+m$ for every set $k\in\mathbb{N}_{0}$, and $z'=h(n)$. Then $z=z'$.

(vi) The product through pairs. For all $m,n\in\mathbb{N}_{0}$ and every set $z$: $z=m\cdot n$ if and only if there is a set $f$ such that $f:\mathbb{N}_{0}\to\mathbb{N}_{0}$ is a map, $(0,0)\in f$, for every set $k\in\mathbb{N}_{0}$ and every set $b$ with $(k,b)\in f$ there is a set $c$ with $((b,m),c)\in{+}$ and $(S(k),c)\in f$, and $(n,z)\in f$.

(vii) Membership in the multiplication. For every set $p$: $p\in{\cdot}$ 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)$.

(viii) The step condition is predicative. There is a predicative formula in $x_{0},\dots,x_{5}$ that holds exactly when

$$\text{for every set } k\in\mathbb{N}_{0} \text{ and every set } b \text{ with } (k,b)\in x_{5} \text{ there is a set } c \text{ with } ((b,x_{1}),c)\in{+} \text{ and } (S(k),c)\in x_{5}.$$

(ix) The defining condition is predicative. There is a predicative formula in $x_{0},\dots,x_{5}$ that holds exactly when $x_{5}:\mathbb{N}_{0}\to\mathbb{N}_{0}$ is a map, $(0,0)\in x_{5}$, the condition displayed in (viii) holds, and $(x_{2},x_{4})\in x_{5}$.