Skip to main content
replaced proof by contradiction with direct proof
Source Link
user44143
user44143

We can explicitly give the requested implicit definition for multiplication: It is the unique function on $(\mathbb{N},S,0)$ satisfying: \begin{align} 0a&=0\\ ab&=ba\\ a(bc)&=(ab)c\\ (Sa)S(ab) &= S(aS(bS(a))) \end{align} The last identity is a distributive law, which would be more familiarly written as: $$(1+a)(1+ab) = 1+a(1+b(1+a))$$

As is usual in these matters, we look at numerals of the form $S^n0$. For each positive integer $n$, that numeral is a term in the language of the model. We quantify over $n$'s outside the model.

We prove by induction that for all $m$ and $n$, the axioms imply that the only possible value for $S^m0\ S^n0$ is $S^{mn}0$, and thus determine the multiplication function on the whole domain of the model. The inductive cases are proved in the lexicographic order on $(m,n)$, so we can use the inductive hypothesis of $(m',n')$ whenever either $m'<m$ or $m'=m \wedge n'<n$.

  • The case $m=0$ follows from the first axiom.

  • The case $m>n$ follows from $m'=n,n'=m$.

  • The case $m=1$, $n=1+k$ follows from \begin{array}{rll} S^m0\ S^n0 &=(SS^k0)S0 & \text{ by commutativity} \\ &=(SS^k0)S((S^k0)0)\ & \text{ by }m'=0, n'=k \\ &=S((S^k0)S(0(SS^k0))) & \text{ by distributing }a=S^k0, b=0 \\ &=S((S^k0)(S0)) & \text{ by }m'=0, n'=1+k\\ &=S(S^k0) & \text{ by }m'=1, n'=k\\ &=S^{mn}0 \end{array}

  • The case $1<m\le n$, where $m-1$ and $n$ have a common factor $h>1$ follows from \begin{array}{rll} S^m0\ S^n0 &= S^m0\ S^h0\ S^{n/h}0 &\text{ by }m'=h, n'=n/h\\ &= S^{h}0\ S^{mn/h}0 &\text{ by }m'=m, n'=n/h\\ &= S^{mn}0 &\text{ by }m'=h, n'=mn/h \end{array} The inductive hypotheses all come before $(m,n)$ in the inductive order because $h\le m-1<m$ and $n/h<n$.

  • In the case $1<m\le n$, where $m-1$ and $n$ are relatively prime, there is some $j$ with $$jn=1+k(m-1)$$ and \begin{align} \text{either }\ m=2,\ \ &1=j=m-1\\ \text{ or }\ \ m>2,\ \ &1\le j<m-1 \end{align} In both cases $0<k<n$. Let $M=m-1$. Then \begin{array}{rll} S^j0\ S^m0\ S^n0 & = S^m0\ S^{jn}0 &\text{ by }m'=j, n'=n\\ &= S(S^M0)S(S^{kM}0) &\text{ by definitions of }j,k,M\\ &= S(S^M0)S(S^M0\ S^k0) &\text{ by }m'=M, n'=k\\ &= S((S^M0)S((S^k0)SS^M0)) &\text{ by distributing }a=S^M0, b=S^k0\\ &= S((S^M0)S(S^{k(1+M)}0)) &\text{ by }m'=1+M=m, n'=k\\ &= S^{1+M(1+k(1+M))}0 &\text{ by }m'=M, n'=1+k(1+M)\\ &= S^{mjn}0 &\text{ by definitions of }j,k,M \\ &= S^j0\ S^{mn}0 &\text{ by }m'=j, n'=mn \end{array}\begin{array}{rll} S^j0\ S^m0\ S^n0 & = S^m0\ S^{jn}0 &\text{ by }m'=j, n'=n\\ &= S(S^M0)S(S^{kM}0) &\text{ by definitions of }j,k,M\\ &= S(S^M0)S(S^M0\ S^k0) &\text{ by }m'=M, n'=k\\ &= S((S^M0)S((S^k0)SS^M0)) &\text{ by distributing }a=S^M0, b=S^k0\\ &= S((S^M0)S(S^{k(1+M)}0)) &\text{ by }m'=1+M=m, n'=k\\ &= S^{1+M(1+k(1+M))}0 &\text{ by }m'=M, n'=1+k(1+M)\\ &= S^{mjn}0 &\text{ by definitions of }j,k,M \end{array} Now sinceSince $S^m0\ S^n=0$ is an element of the standard model, it is of the form $S^p0$. If $mn\neq p$, thenSo also \begin{array}{rll} S^j0\ S^m0\ S^n0 &= S^j0 S^p0 & \text{ by definition of }p\\ &= S^{jp}0 &\text{ by }m'=j, n'=p\\ &\neq S^{jmn}0 &\text{ by }mn\neq p \\ &= S^j0\ S^{mn}0 &\text{ by }m'=j, n'=mn \end{array}\begin{array}{rll} S^j0\ S^m0\ S^n0 &= S^j0 S^p0 & \text{ by definition of }p\\ &= S^{jp}0 &\text{ by }m'=j, n'=p \end{array} which would contradict what was just proved. This rules out all the choices forNow $S^m0\ S^n0$ other than$S^{mjn}0=S^{jp}0$, $S^{mn}0$$mjn=jp$, so it must be the case that$p=mn$, and $S^m0\ S^n0 = S^{mn}0%$ as desired.

This establishes the claim that the above axioms implicitly define multiplication in $(\mathbb{N}, 0, S)$.

We can explicitly give the requested implicit definition for multiplication: It is the unique function on $(\mathbb{N},S,0)$ satisfying: \begin{align} 0a&=0\\ ab&=ba\\ a(bc)&=(ab)c\\ (Sa)S(ab) &= S(aS(bS(a))) \end{align} The last identity is a distributive law, which would be more familiarly written as: $$(1+a)(1+ab) = 1+a(1+b(1+a))$$

As is usual in these matters, we look at numerals of the form $S^n0$. For each positive integer $n$, that numeral is a term in the language of the model. We quantify over $n$'s outside the model.

We prove by induction that for all $m$ and $n$, the axioms imply that the only possible value for $S^m0\ S^n0$ is $S^{mn}0$, and thus determine the multiplication function on the whole domain of the model. The inductive cases are proved in the lexicographic order on $(m,n)$, so we can use the inductive hypothesis of $(m',n')$ whenever either $m'<m$ or $m'=m \wedge n'<n$.

  • The case $m=0$ follows from the first axiom.

  • The case $m>n$ follows from $m'=n,n'=m$.

  • The case $m=1$, $n=1+k$ follows from \begin{array}{rll} S^m0\ S^n0 &=(SS^k0)S0 & \text{ by commutativity} \\ &=(SS^k0)S((S^k0)0)\ & \text{ by }m'=0, n'=k \\ &=S((S^k0)S(0(SS^k0))) & \text{ by distributing }a=S^k0, b=0 \\ &=S((S^k0)(S0)) & \text{ by }m'=0, n'=1+k\\ &=S(S^k0) & \text{ by }m'=1, n'=k\\ &=S^{mn}0 \end{array}

  • The case $1<m\le n$, where $m-1$ and $n$ have a common factor $h>1$ follows from \begin{array}{rll} S^m0\ S^n0 &= S^m0\ S^h0\ S^{n/h}0 &\text{ by }m'=h, n'=n/h\\ &= S^{h}0\ S^{mn/h}0 &\text{ by }m'=m, n'=n/h\\ &= S^{mn}0 &\text{ by }m'=h, n'=mn/h \end{array} The inductive hypotheses all come before $(m,n)$ in the inductive order because $h\le m-1<m$ and $n/h<n$.

  • In the case $1<m\le n$, where $m-1$ and $n$ are relatively prime, there is some $j$ with $$jn=1+k(m-1)$$ and \begin{align} \text{either }\ m=2,\ \ &1=j=m-1\\ \text{ or }\ \ m>2,\ \ &1\le j<m-1 \end{align} In both cases $0<k<n$. Let $M=m-1$. Then \begin{array}{rll} S^j0\ S^m0\ S^n0 & = S^m0\ S^{jn}0 &\text{ by }m'=j, n'=n\\ &= S(S^M0)S(S^{kM}0) &\text{ by definitions of }j,k,M\\ &= S(S^M0)S(S^M0\ S^k0) &\text{ by }m'=M, n'=k\\ &= S((S^M0)S((S^k0)SS^M0)) &\text{ by distributing }a=S^M0, b=S^k0\\ &= S((S^M0)S(S^{k(1+M)}0)) &\text{ by }m'=1+M=m, n'=k\\ &= S^{1+M(1+k(1+M))}0 &\text{ by }m'=M, n'=1+k(1+M)\\ &= S^{mjn}0 &\text{ by definitions of }j,k,M \\ &= S^j0\ S^{mn}0 &\text{ by }m'=j, n'=mn \end{array} Now since $S^m0\ S^n=0$ is an element of the standard model, it is of the form $S^p0$. If $mn\neq p$, then \begin{array}{rll} S^j0\ S^m0\ S^n0 &= S^j0 S^p0 & \text{ by definition of }p\\ &= S^{jp}0 &\text{ by }m'=j, n'=p\\ &\neq S^{jmn}0 &\text{ by }mn\neq p \\ &= S^j0\ S^{mn}0 &\text{ by }m'=j, n'=mn \end{array} which would contradict what was just proved. This rules out all the choices for $S^m0\ S^n0$ other than $S^{mn}0$, so it must be the case that $S^m0\ S^n0 = S^{mn}0%$ as desired.

This establishes the claim that the above axioms implicitly define multiplication in $(\mathbb{N}, 0, S)$.

We can explicitly give the requested implicit definition for multiplication: It is the unique function on $(\mathbb{N},S,0)$ satisfying: \begin{align} 0a&=0\\ ab&=ba\\ a(bc)&=(ab)c\\ (Sa)S(ab) &= S(aS(bS(a))) \end{align} The last identity is a distributive law, which would be more familiarly written as: $$(1+a)(1+ab) = 1+a(1+b(1+a))$$

As is usual in these matters, we look at numerals of the form $S^n0$. For each positive integer $n$, that numeral is a term in the language of the model. We quantify over $n$'s outside the model.

We prove by induction that for all $m$ and $n$, the axioms imply that the only possible value for $S^m0\ S^n0$ is $S^{mn}0$, and thus determine the multiplication function on the whole domain of the model. The inductive cases are proved in the lexicographic order on $(m,n)$, so we can use the inductive hypothesis of $(m',n')$ whenever either $m'<m$ or $m'=m \wedge n'<n$.

  • The case $m=0$ follows from the first axiom.

  • The case $m>n$ follows from $m'=n,n'=m$.

  • The case $m=1$, $n=1+k$ follows from \begin{array}{rll} S^m0\ S^n0 &=(SS^k0)S0 & \text{ by commutativity} \\ &=(SS^k0)S((S^k0)0)\ & \text{ by }m'=0, n'=k \\ &=S((S^k0)S(0(SS^k0))) & \text{ by distributing }a=S^k0, b=0 \\ &=S((S^k0)(S0)) & \text{ by }m'=0, n'=1+k\\ &=S(S^k0) & \text{ by }m'=1, n'=k\\ &=S^{mn}0 \end{array}

  • The case $1<m\le n$, where $m-1$ and $n$ have a common factor $h>1$ follows from \begin{array}{rll} S^m0\ S^n0 &= S^m0\ S^h0\ S^{n/h}0 &\text{ by }m'=h, n'=n/h\\ &= S^{h}0\ S^{mn/h}0 &\text{ by }m'=m, n'=n/h\\ &= S^{mn}0 &\text{ by }m'=h, n'=mn/h \end{array} The inductive hypotheses all come before $(m,n)$ in the inductive order because $h\le m-1<m$ and $n/h<n$.

  • In the case $1<m\le n$, where $m-1$ and $n$ are relatively prime, there is some $j$ with $$jn=1+k(m-1)$$ and \begin{align} \text{either }\ m=2,\ \ &1=j=m-1\\ \text{ or }\ \ m>2,\ \ &1\le j<m-1 \end{align} In both cases $0<k<n$. Let $M=m-1$. Then \begin{array}{rll} S^j0\ S^m0\ S^n0 & = S^m0\ S^{jn}0 &\text{ by }m'=j, n'=n\\ &= S(S^M0)S(S^{kM}0) &\text{ by definitions of }j,k,M\\ &= S(S^M0)S(S^M0\ S^k0) &\text{ by }m'=M, n'=k\\ &= S((S^M0)S((S^k0)SS^M0)) &\text{ by distributing }a=S^M0, b=S^k0\\ &= S((S^M0)S(S^{k(1+M)}0)) &\text{ by }m'=1+M=m, n'=k\\ &= S^{1+M(1+k(1+M))}0 &\text{ by }m'=M, n'=1+k(1+M)\\ &= S^{mjn}0 &\text{ by definitions of }j,k,M \end{array} Since $S^m0\ S^n=0$ is an element of the standard model, it is of the form $S^p0$. So also \begin{array}{rll} S^j0\ S^m0\ S^n0 &= S^j0 S^p0 & \text{ by definition of }p\\ &= S^{jp}0 &\text{ by }m'=j, n'=p \end{array} Now $S^{mjn}0=S^{jp}0$, $mjn=jp$, $p=mn$, and $S^m0\ S^n0 = S^{mn}0%$ as desired.

This establishes the claim that the above axioms implicitly define multiplication in $(\mathbb{N}, 0, S)$.

removed axiom of cancellation
Source Link
user44143
user44143

We can explicitly give the requested implicit definition for multiplication: It is the unique function on $(\mathbb{N},S,0)$ satisfying: \begin{align} 0a&=0\\ ab&=ba\\ a(bc)&=(ab)c\\ (Sa)b=(Sa)c &\to b=c\\ (Sa)S(ab) &= S(aS(bS(a))) \end{align}\begin{align} 0a&=0\\ ab&=ba\\ a(bc)&=(ab)c\\ (Sa)S(ab) &= S(aS(bS(a))) \end{align} The last identity is a distributive law, which would be more familiarly written as: $$(1+a)(1+ab) = 1+a(1+b(1+a))$$

As is usual in these matters, we look at numerals of the form $S^n0$. For each positive integer $n$, that numeral is a term in the language of the model. We quantify over $n$'s outside the model.

We prove by induction that for all $m$ and $n$, the axioms imply that the only possible value for $S^m0\ S^n0=S^{mn}0$$S^m0\ S^n0$ is $S^{mn}0$, willand thus determine the values of the multiplication function foron the whole domain of the model. The inductive cases are proved in the lexicographic order on $(m,n)$, so we can use the inductive hypothesis of $(m',n')$ whenever either $m'<m$ or $m'=m \wedge n'<n$.

  • The case $m=0$ follows from the first axiom.

  • The case $m>n$ follows from $m'=n,n'=m$.

  • The case $m=1$, $n=1+k$ follows from \begin{array}{rll} S^m0\ S^n0 &=(SS^k0)S0 & \text{ by commutativity} \\ &=(SS^k0)S((S^k0)0)\ & \text{ by }m'=0, n'=k \\ &=S((S^k0)S(0(SS^k0))) & \text{ by distributing }a=S^k0, b=0 \\ &=S((S^k0)(S0)) & \text{ by }m'=0, n'=1+k\\ &=S(S^k0) & \text{ by }m'=1, n'=k\\ &=S^{mn}0 \end{array}

  • The case $1<m\le n$, where $m-1$ and $n$ have a common factor $h>1$ follows from \begin{array}{rll} S^m0\ S^n0 &= S^m0\ S^h0\ S^{n/h}0 &\text{ by }m'=h, n'=n/h\\ &= S^{h}0\ S^{mn/h}0 &\text{ by }m'=m, n'=n/h\\ &= S^{mn}0 &\text{ by }m'=h, n'=mn/h \end{array} The inductive hypotheses all come before $(m,n)$ in the inductive order because $h\le m-1<m$ and $n/h<n$.

  • In the case $1<m\le n$, where $m-1$ and $n$ are relatively prime, there is some $j$ with $$jn=1+k(m-1)$$ and \begin{align} \text{either }\ m=2,\ \ &1=j=m-1\\ \text{ or }\ \ m>2,\ \ &1\le j<m-1 \end{align} In both cases $0<k<n$. Let $M=m-1$. Then \begin{array}{rll} S^j0\ S^m0\ S^n0 & = S^m0\ S^{jn}0 &\text{ by }m'=j, n'=n\\ &= S(S^M0)S(S^{kM}0) &\text{ by definitions of }j,k,M\\ &= S(S^M0)S(S^M0\ S^k0) &\text{ by }m'=M, n'=k\\ &= S((S^M0)S((S^k0)SS^M0)) &\text{ by distributing }a=S^M0, b=S^k0\\ &= S((S^M0)S(S^{k(1+M)}0)) &\text{ by }m'=1+M=m, n'=k\\ &= S^{1+M(1+k(1+M))}0 &\text{ by }m'=M, n'=1+k(1+M)\\ &= S^{mjn}0 &\text{ by definitions of }j,k,M \\ &= S^j0\ S^{mn}0 &\text{ by }m'=j, n'=mn \end{array} So either immediately or by cancellingNow since $S^j0$ from both sides$S^m0\ S^n=0$ is an element of the standard model, it is of the form $S^m0\ S^n0 = S^{mn}0$$S^p0$. If $mn\neq p$, then \begin{array}{rll} S^j0\ S^m0\ S^n0 &= S^j0 S^p0 & \text{ by definition of }p\\ &= S^{jp}0 &\text{ by }m'=j, n'=p\\ &\neq S^{jmn}0 &\text{ by }mn\neq p \\ &= S^j0\ S^{mn}0 &\text{ by }m'=j, n'=mn \end{array} which would contradict what was just proved. This rules out all the choices for $S^m0\ S^n0$ other than $S^{mn}0$, so it must be the case that $S^m0\ S^n0 = S^{mn}0%$ as desired.

This establishes the claim that the above axioms implicitly define multiplication in $(\mathbb{N}, 0, S)$.

We can explicitly give the requested implicit definition for multiplication: It is the unique function on $(\mathbb{N},S,0)$ satisfying: \begin{align} 0a&=0\\ ab&=ba\\ a(bc)&=(ab)c\\ (Sa)b=(Sa)c &\to b=c\\ (Sa)S(ab) &= S(aS(bS(a))) \end{align} The last identity is a distributive law, which would be more familiarly written as: $$(1+a)(1+ab) = 1+a(1+b(1+a))$$

As is usual in these matters, we look at numerals of the form $S^n0$. For each positive integer $n$, that numeral is a term in the language of the model. We quantify over $n$'s outside the model.

We prove by induction that for all $m$ and $n$, the axioms imply $S^m0\ S^n0=S^{mn}0$, will determine the values of the multiplication function for the whole domain of the model. The inductive cases are proved in the lexicographic order on $(m,n)$, so we can use the inductive hypothesis of $(m',n')$ whenever either $m'<m$ or $m'=m \wedge n'<n$.

  • The case $m=0$ follows from the first axiom.

  • The case $m>n$ follows from $m'=n,n'=m$.

  • The case $m=1$, $n=1+k$ follows from \begin{array}{rll} S^m0\ S^n0 &=(SS^k0)S0 & \text{ by commutativity} \\ &=(SS^k0)S((S^k0)0)\ & \text{ by }m'=0, n'=k \\ &=S((S^k0)S(0(SS^k0))) & \text{ by distributing }a=S^k0, b=0 \\ &=S((S^k0)(S0)) & \text{ by }m'=0, n'=1+k\\ &=S(S^k0) & \text{ by }m'=1, n'=k\\ &=S^{mn}0 \end{array}

  • The case $1<m\le n$, where $m-1$ and $n$ have a common factor $h>1$ follows from \begin{array}{rll} S^m0\ S^n0 &= S^m0\ S^h0\ S^{n/h}0 &\text{ by }m'=h, n'=n/h\\ &= S^{h}0\ S^{mn/h}0 &\text{ by }m'=m, n'=n/h\\ &= S^{mn}0 &\text{ by }m'=h, n'=mn/h \end{array} The inductive hypotheses all come before $(m,n)$ in the inductive order because $h\le m-1<m$ and $n/h<n$.

  • In the case $1<m\le n$, where $m-1$ and $n$ are relatively prime, there is some $j$ with $$jn=1+k(m-1)$$ and \begin{align} \text{either }\ m=2,\ \ &1=j=m-1\\ \text{ or }\ \ m>2,\ \ &1\le j<m-1 \end{align} In both cases $0<k<n$. Let $M=m-1$. Then \begin{array}{rll} S^j0\ S^m0\ S^n0 & = S^m0\ S^{jn}0 &\text{ by }m'=j, n'=n\\ &= S(S^M0)S(S^{kM}0) &\text{ by definitions of }j,k,M\\ &= S(S^M0)S(S^M0\ S^k0) &\text{ by }m'=M, n'=k\\ &= S((S^M0)S((S^k0)SS^M0)) &\text{ by distributing }a=S^M0, b=S^k0\\ &= S((S^M0)S(S^{k(1+M)}0)) &\text{ by }m'=1+M=m, n'=k\\ &= S^{1+M(1+k(1+M))}0 &\text{ by }m'=M, n'=1+k(1+M)\\ &= S^{mjn}0 &\text{ by definitions of }j,k,M \\ &= S^j0\ S^{mn}0 &\text{ by }m'=j, n'=mn \end{array} So either immediately or by cancelling $S^j0$ from both sides, $S^m0\ S^n0 = S^{mn}0$.

We can explicitly give the requested implicit definition for multiplication: It is the unique function on $(\mathbb{N},S,0)$ satisfying: \begin{align} 0a&=0\\ ab&=ba\\ a(bc)&=(ab)c\\ (Sa)S(ab) &= S(aS(bS(a))) \end{align} The last identity is a distributive law, which would be more familiarly written as: $$(1+a)(1+ab) = 1+a(1+b(1+a))$$

As is usual in these matters, we look at numerals of the form $S^n0$. For each positive integer $n$, that numeral is a term in the language of the model. We quantify over $n$'s outside the model.

We prove by induction that for all $m$ and $n$, the axioms imply that the only possible value for $S^m0\ S^n0$ is $S^{mn}0$, and thus determine the multiplication function on the whole domain of the model. The inductive cases are proved in the lexicographic order on $(m,n)$, so we can use the inductive hypothesis of $(m',n')$ whenever either $m'<m$ or $m'=m \wedge n'<n$.

  • The case $m=0$ follows from the first axiom.

  • The case $m>n$ follows from $m'=n,n'=m$.

  • The case $m=1$, $n=1+k$ follows from \begin{array}{rll} S^m0\ S^n0 &=(SS^k0)S0 & \text{ by commutativity} \\ &=(SS^k0)S((S^k0)0)\ & \text{ by }m'=0, n'=k \\ &=S((S^k0)S(0(SS^k0))) & \text{ by distributing }a=S^k0, b=0 \\ &=S((S^k0)(S0)) & \text{ by }m'=0, n'=1+k\\ &=S(S^k0) & \text{ by }m'=1, n'=k\\ &=S^{mn}0 \end{array}

  • The case $1<m\le n$, where $m-1$ and $n$ have a common factor $h>1$ follows from \begin{array}{rll} S^m0\ S^n0 &= S^m0\ S^h0\ S^{n/h}0 &\text{ by }m'=h, n'=n/h\\ &= S^{h}0\ S^{mn/h}0 &\text{ by }m'=m, n'=n/h\\ &= S^{mn}0 &\text{ by }m'=h, n'=mn/h \end{array} The inductive hypotheses all come before $(m,n)$ in the inductive order because $h\le m-1<m$ and $n/h<n$.

  • In the case $1<m\le n$, where $m-1$ and $n$ are relatively prime, there is some $j$ with $$jn=1+k(m-1)$$ and \begin{align} \text{either }\ m=2,\ \ &1=j=m-1\\ \text{ or }\ \ m>2,\ \ &1\le j<m-1 \end{align} In both cases $0<k<n$. Let $M=m-1$. Then \begin{array}{rll} S^j0\ S^m0\ S^n0 & = S^m0\ S^{jn}0 &\text{ by }m'=j, n'=n\\ &= S(S^M0)S(S^{kM}0) &\text{ by definitions of }j,k,M\\ &= S(S^M0)S(S^M0\ S^k0) &\text{ by }m'=M, n'=k\\ &= S((S^M0)S((S^k0)SS^M0)) &\text{ by distributing }a=S^M0, b=S^k0\\ &= S((S^M0)S(S^{k(1+M)}0)) &\text{ by }m'=1+M=m, n'=k\\ &= S^{1+M(1+k(1+M))}0 &\text{ by }m'=M, n'=1+k(1+M)\\ &= S^{mjn}0 &\text{ by definitions of }j,k,M \\ &= S^j0\ S^{mn}0 &\text{ by }m'=j, n'=mn \end{array} Now since $S^m0\ S^n=0$ is an element of the standard model, it is of the form $S^p0$. If $mn\neq p$, then \begin{array}{rll} S^j0\ S^m0\ S^n0 &= S^j0 S^p0 & \text{ by definition of }p\\ &= S^{jp}0 &\text{ by }m'=j, n'=p\\ &\neq S^{jmn}0 &\text{ by }mn\neq p \\ &= S^j0\ S^{mn}0 &\text{ by }m'=j, n'=mn \end{array} which would contradict what was just proved. This rules out all the choices for $S^m0\ S^n0$ other than $S^{mn}0$, so it must be the case that $S^m0\ S^n0 = S^{mn}0%$ as desired.

This establishes the claim that the above axioms implicitly define multiplication in $(\mathbb{N}, 0, S)$.

straightened out induction, simplifying cases and removing one axiom
Source Link
user44143
user44143

We can explicitly give the requested implicit definition for multiplication: It is the unique function on $(\mathbb{N},S,0)$ satisfying: \begin{align} 0a&=0\\ ab&=ba\\ a(bc)&=(ab)c\\ (Sa)b=(Sa)c &\to b=c\\ (Sa)S(ab) &= S(aS(bS(a))) \end{align} The last identity is a distributive law, which would be more familiarly written as: $$(1+a)(1+ab) = 1+a(1+b(1+a))$$

As is usual in these matters, we look at numerals of the form $S^n0$. For each positive integer $n$, that numeral is a term in the language of the model. We quantify over $n$'s outside the model.

We prove by induction that for all $m$ and $n$, the axioms imply $S^m0\ S^n0=S^{mn}0$, will determine the values of the multiplication function for the whole domain of the model. The inductive cases are proved in the lexicographic order on $(m,n)$, so we can use the inductive hypothesis of $(m',n')$ whenever either $m'<m$ or $m'=m \wedge n'<n$.

  • The case $m=0$ follows from the first axiom.

  • The case $m>n$ follows from $m'=n,n'=m$.

  • The case $m=1$, $n=1+k$ follows from \begin{array}{rll} S^m0\ S^n0 &=(SS^k0)S0 & \text{ by commutativity} \\ &=(SS^k0)S((S^k0)0)\ & \text{ by }m'=0, n'=k \\ &=S((S^k0)S(0(SS^k0))) & \text{ by distributing }a=S^k0, b=0 \\ &=S((S^k0)(S0)) & \text{ by }m'=0, n'=1+k\\ &=S(S^k0) & \text{ by }m'=1, n'=k\\ &=S^{mn}0 \end{array}

  • The case $1<m\le n$, where $m-1$ and $n$ have a common factor $h>1$ follows from \begin{array}{rll} S^m0\ S^n0 &= S^m0\ S^h0\ S^{n/h}0 &\text{ by }m'=h, n'=n/h\\ &= S^{h}0\ S^{mn/h}0 &\text{ by }m'=m, n'=n/h\\ &= S^{mn}0 &\text{ by }m'=h, n'=mn/h \end{array} The inductive hypotheses all come before $(m,n)$ in the inductive order because $h\le m-1<m$ and $n/h<n$.

  • In the case $1<m\le n$, where $m-1$ and $n$ are relatively prime, there is some $j$ with $$jn=1+k(m-1)$$ and \begin{align} \text{either }\ m=2,\ \ &1=j=m-1\\ \text{ or }\ \ m>2,\ \ &1\le j<m-1 \end{align} In both cases $0<k<n$. Let $M=m-1$. Then \begin{array}{rll} S^j0\ S^m0\ S^n0 & = S^m0\ S^{jn}0 &\text{ by }m'=j, n'=n\\ &= S(S^M0)S(S^{kM}0) &\text{ by definitions of }j,k,M\\ &= S(S^M0)S(S^M0\ S^k0) &\text{ by }m'=M, n'=k\\ &= S((S^M0)S((S^k0)SS^M0)) &\text{ by distributing }a=S^M0, b=S^k0\\ &= S((S^M0)S(S^{k(1+M)}0)) &\text{ by }m'=1+M=m, n'=k\\ &= S(S^{M(1+k(1+M)}0) &\text{ by }m'=M, n'=1+k(1+M)\\ &= S^{mjn}0 &\text{ by definitions of }j,k,M \\ &= S^j0\ S^{mn}0 &\text{ by }m'=j, n'=mn \end{array}\begin{array}{rll} S^j0\ S^m0\ S^n0 & = S^m0\ S^{jn}0 &\text{ by }m'=j, n'=n\\ &= S(S^M0)S(S^{kM}0) &\text{ by definitions of }j,k,M\\ &= S(S^M0)S(S^M0\ S^k0) &\text{ by }m'=M, n'=k\\ &= S((S^M0)S((S^k0)SS^M0)) &\text{ by distributing }a=S^M0, b=S^k0\\ &= S((S^M0)S(S^{k(1+M)}0)) &\text{ by }m'=1+M=m, n'=k\\ &= S^{1+M(1+k(1+M))}0 &\text{ by }m'=M, n'=1+k(1+M)\\ &= S^{mjn}0 &\text{ by definitions of }j,k,M \\ &= S^j0\ S^{mn}0 &\text{ by }m'=j, n'=mn \end{array} So either immediately or by cancelling $S^j0$ from both sides, $S^m0\ S^n0 = S^{mn}0$.

We can explicitly give the requested implicit definition for multiplication: It is the unique function on $(\mathbb{N},S,0)$ satisfying: \begin{align} 0a&=0\\ ab&=ba\\ a(bc)&=(ab)c\\ (Sa)b=(Sa)c &\to b=c\\ (Sa)S(ab) &= S(aS(bS(a))) \end{align} The last identity is a distributive law, which would be more familiarly written as: $$(1+a)(1+ab) = 1+a(1+b(1+a))$$

As is usual in these matters, we look at numerals of the form $S^n0$. For each positive integer $n$, that numeral is a term in the language of the model. We quantify over $n$'s outside the model.

We prove by induction that for all $m$ and $n$, the axioms imply $S^m0\ S^n0=S^{mn}0$, will determine the values of the multiplication function for the whole domain of the model. The inductive cases are proved in the lexicographic order on $(m,n)$, so we can use the inductive hypothesis of $(m',n')$ whenever either $m'<m$ or $m'=m \wedge n'<n$.

  • The case $m=0$ follows from the first axiom.

  • The case $m>n$ follows from $m'=n,n'=m$.

  • The case $m=1$, $n=1+k$ follows from \begin{array}{rll} S^m0\ S^n0 &=(SS^k0)S0 & \text{ by commutativity} \\ &=(SS^k0)S((S^k0)0)\ & \text{ by }m'=0, n'=k \\ &=S((S^k0)S(0(SS^k0))) & \text{ by distributing }a=S^k0, b=0 \\ &=S((S^k0)(S0)) & \text{ by }m'=0, n'=1+k\\ &=S(S^k0) & \text{ by }m'=1, n'=k\\ &=S^{mn}0 \end{array}

  • The case $1<m\le n$, where $m-1$ and $n$ have a common factor $h>1$ follows from \begin{array}{rll} S^m0\ S^n0 &= S^m0\ S^h0\ S^{n/h}0 &\text{ by }m'=h, n'=n/h\\ &= S^{h}0\ S^{mn/h}0 &\text{ by }m'=m, n'=n/h\\ &= S^{mn}0 &\text{ by }m'=h, n'=mn/h \end{array} The inductive hypotheses all come before $(m,n)$ in the inductive order because $h\le m-1<m$ and $n/h<n$.

  • In the case $1<m\le n$, where $m-1$ and $n$ are relatively prime, there is some $j$ with $$jn=1+k(m-1)$$ and \begin{align} \text{either }\ m=2,\ \ &1=j=m-1\\ \text{ or }\ \ m>2,\ \ &1\le j<m-1 \end{align} In both cases $0<k<n$. Let $M=m-1$. Then \begin{array}{rll} S^j0\ S^m0\ S^n0 & = S^m0\ S^{jn}0 &\text{ by }m'=j, n'=n\\ &= S(S^M0)S(S^{kM}0) &\text{ by definitions of }j,k,M\\ &= S(S^M0)S(S^M0\ S^k0) &\text{ by }m'=M, n'=k\\ &= S((S^M0)S((S^k0)SS^M0)) &\text{ by distributing }a=S^M0, b=S^k0\\ &= S((S^M0)S(S^{k(1+M)}0)) &\text{ by }m'=1+M=m, n'=k\\ &= S(S^{M(1+k(1+M)}0) &\text{ by }m'=M, n'=1+k(1+M)\\ &= S^{mjn}0 &\text{ by definitions of }j,k,M \\ &= S^j0\ S^{mn}0 &\text{ by }m'=j, n'=mn \end{array} So either immediately or by cancelling $S^j0$ from both sides, $S^m0\ S^n0 = S^{mn}0$.

We can explicitly give the requested implicit definition for multiplication: It is the unique function on $(\mathbb{N},S,0)$ satisfying: \begin{align} 0a&=0\\ ab&=ba\\ a(bc)&=(ab)c\\ (Sa)b=(Sa)c &\to b=c\\ (Sa)S(ab) &= S(aS(bS(a))) \end{align} The last identity is a distributive law, which would be more familiarly written as: $$(1+a)(1+ab) = 1+a(1+b(1+a))$$

As is usual in these matters, we look at numerals of the form $S^n0$. For each positive integer $n$, that numeral is a term in the language of the model. We quantify over $n$'s outside the model.

We prove by induction that for all $m$ and $n$, the axioms imply $S^m0\ S^n0=S^{mn}0$, will determine the values of the multiplication function for the whole domain of the model. The inductive cases are proved in the lexicographic order on $(m,n)$, so we can use the inductive hypothesis of $(m',n')$ whenever either $m'<m$ or $m'=m \wedge n'<n$.

  • The case $m=0$ follows from the first axiom.

  • The case $m>n$ follows from $m'=n,n'=m$.

  • The case $m=1$, $n=1+k$ follows from \begin{array}{rll} S^m0\ S^n0 &=(SS^k0)S0 & \text{ by commutativity} \\ &=(SS^k0)S((S^k0)0)\ & \text{ by }m'=0, n'=k \\ &=S((S^k0)S(0(SS^k0))) & \text{ by distributing }a=S^k0, b=0 \\ &=S((S^k0)(S0)) & \text{ by }m'=0, n'=1+k\\ &=S(S^k0) & \text{ by }m'=1, n'=k\\ &=S^{mn}0 \end{array}

  • The case $1<m\le n$, where $m-1$ and $n$ have a common factor $h>1$ follows from \begin{array}{rll} S^m0\ S^n0 &= S^m0\ S^h0\ S^{n/h}0 &\text{ by }m'=h, n'=n/h\\ &= S^{h}0\ S^{mn/h}0 &\text{ by }m'=m, n'=n/h\\ &= S^{mn}0 &\text{ by }m'=h, n'=mn/h \end{array} The inductive hypotheses all come before $(m,n)$ in the inductive order because $h\le m-1<m$ and $n/h<n$.

  • In the case $1<m\le n$, where $m-1$ and $n$ are relatively prime, there is some $j$ with $$jn=1+k(m-1)$$ and \begin{align} \text{either }\ m=2,\ \ &1=j=m-1\\ \text{ or }\ \ m>2,\ \ &1\le j<m-1 \end{align} In both cases $0<k<n$. Let $M=m-1$. Then \begin{array}{rll} S^j0\ S^m0\ S^n0 & = S^m0\ S^{jn}0 &\text{ by }m'=j, n'=n\\ &= S(S^M0)S(S^{kM}0) &\text{ by definitions of }j,k,M\\ &= S(S^M0)S(S^M0\ S^k0) &\text{ by }m'=M, n'=k\\ &= S((S^M0)S((S^k0)SS^M0)) &\text{ by distributing }a=S^M0, b=S^k0\\ &= S((S^M0)S(S^{k(1+M)}0)) &\text{ by }m'=1+M=m, n'=k\\ &= S^{1+M(1+k(1+M))}0 &\text{ by }m'=M, n'=1+k(1+M)\\ &= S^{mjn}0 &\text{ by definitions of }j,k,M \\ &= S^j0\ S^{mn}0 &\text{ by }m'=j, n'=mn \end{array} So either immediately or by cancelling $S^j0$ from both sides, $S^m0\ S^n0 = S^{mn}0$.

straightened out induction, simplifying cases and removing one axiom
Source Link
user44143
user44143
Loading
simplified axioms, removed double bullets
Source Link
user44143
user44143
Loading
added explanation for odd identity
Source Link
user44143
user44143
Loading
Source Link
user44143
user44143
Loading