Really Simple Equations

Posted on 2017-04-01 by nbloomf

\(\newcommand{\hyp}[2]{\stackrel{\tiny\text{hyp}}{#2}}\) \(\newcommand{\let}[2]{\stackrel{\tiny\text{let}}{#2}}\) \(\newcommand{\a}{a}\) \(\newcommand{\b}{b}\) \(\newcommand{\c}{c}\) \(\newcommand{\p}{p}\) \(\newcommand{\q}{q}\) \(\newcommand{\r}{r}\) \(\newcommand{\s}{s}\) \(\newcommand{\x}{x}\) \(\newcommand{\y}{y}\) \(\newcommand{\z}{z}\) \(\newcommand{\bool}{\mathbb{B}}\) \(\newcommand{\btrue}{\mathsf{true}}\) \(\newcommand{\bfalse}{\mathsf{false}}\) \(\newcommand{\bnot}{\mathsf{not}}\) \(\newcommand{\band}{\mathbin{\mathsf{and}}}\) \(\newcommand{\bor}{\mathbin{\mathsf{or}}}\) \(\newcommand{\bimpl}{\mathbin{\mathsf{impl}}}\) \(\newcommand{\beq}{\mathsf{eq}}\) \(\newcommand{\bif}[3]{\mathsf{if}\left(#1,#2,#3\right)}\) \(\newcommand{\id}{\mathsf{id}}\) \(\newcommand{\compose}{\mathsf{compose}}\) \(\newcommand{\const}{\mathsf{const}}\) \(\newcommand{\apply}{\mathsf{apply}}\) \(\newcommand{\flip}{\mathsf{flip}}\) \(\newcommand{\flipB}{\mathsf{flip2}}\) \(\newcommand{\flipC}{\mathsf{flip3}}\) \(\newcommand{\flipD}{\mathsf{flip4}}\) \(\newcommand{\flipE}{\mathsf{flip5}}\) \(\newcommand{\clone}{\mathsf{clone}}\) \(\newcommand{\cloneC}{\mathsf{clone3}}\) \(\newcommand{\composeAonB}{\mathsf{compose1on2}}\) \(\newcommand{\composeAonC}{\mathsf{compose1on3}}\) \(\newcommand{\composeAonD}{\mathsf{compose1on4}}\) \(\newcommand{\composeBonA}{\mathsf{compose2on1}}\) \(\newcommand{\composeBonB}{\mathsf{compose2on2}}\) \(\newcommand{\composeConA}{\mathsf{compose3on1}}\) \(\newcommand{\ptrue}{\mathsf{ptrue}}\) \(\newcommand{\pfalse}{\mathsf{pfalse}}\) \(\newcommand{\pnot}{\mathsf{pnot}}\) \(\newcommand{\pand}{\mathbin{\mathsf{pand}}}\) \(\newcommand{\por}{\mathbin{\mathsf{por}}}\) \(\newcommand{\pimpl}{\mathbin{\mathsf{pimpl}}}\) \(\newcommand{\fst}{\mathsf{first}}\) \(\newcommand{\snd}{\mathsf{second}}\) \(\newcommand{\dup}{\mathsf{dup}}\) \(\newcommand{\tup}{\mathsf{tup}}\) \(\newcommand{\tSwap}{\mathsf{swap}_{\times}}\) \(\newcommand{\tPair}{\mathsf{pair}_{\times}}\) \(\newcommand{\tAssocL}{\mathsf{assocL}_{\times}}\) \(\newcommand{\tAssocR}{\mathsf{assocR}_{\times}}\) \(\newcommand{\tupL}{\mathsf{tupL}}\) \(\newcommand{\tupR}{\mathsf{tupR}}\) \(\newcommand{\uncurry}{\mathsf{uncurry}}\) \(\newcommand{\curry}{\mathsf{curry}}\) \(\newcommand{\lft}{\mathsf{left}}\) \(\newcommand{\rgt}{\mathsf{right}}\) \(\newcommand{\either}{\mathsf{either}}\) \(\newcommand{\uSwap}{\mathsf{swap}_{+}}\) \(\newcommand{\uPair}{\mathsf{pair}_{+}}\) \(\newcommand{\uAssocL}{\mathsf{assocL}_{+}}\) \(\newcommand{\uAssocR}{\mathsf{assocR}_{+}}\) \(\newcommand{\isLft}{\mathsf{isLeft}}\) \(\newcommand{\isRgt}{\mathsf{isRight}}\) \(\newcommand{\nats}{\mathbb{N}}\) \(\newcommand{\zero}{\mathsf{0}}\) \(\newcommand{\next}{\mathsf{next}}\) \(\newcommand{\unnext}{\mathsf{unnext}}\) \(\newcommand{\iszero}{\mathsf{isZero}}\) \(\newcommand{\prev}{\mathsf{prev}}\) \(\newcommand{\natrec}{\mathsf{natrec}}\) \(\newcommand{\simprec}{\mathsf{simprec}}\) \(\newcommand{\bailrec}{\mathsf{bailrec}}\) \(\newcommand{\mutrec}{\mathsf{mutrec}}\) \(\newcommand{\dnatrec}{\mathsf{dnatrec}}\) \(\newcommand{\normrec}{\mathsf{normrec}}\) \(\newcommand{\findsmallest}{\mathsf{findsmallest}}\) \(\newcommand{\mnormrec}{\mathsf{mnormrec}}\) \(\newcommand{\nequal}{\mathsf{eq}}\) \(\newcommand{\nplus}{\mathsf{plus}}\) \(\newcommand{\ntimes}{\mathsf{times}}\) \(\newcommand{\nleq}{\mathsf{leq}}\) \(\newcommand{\ngeq}{\mathsf{geq}}\) \(\newcommand{\nminus}{\mathsf{minus}}\) \(\newcommand{\nmax}{\mathsf{max}}\) \(\newcommand{\nmin}{\mathsf{min}}\) \(\newcommand{\ndivalg}{\mathsf{divalg}}\) \(\newcommand{\nquo}{\mathsf{quo}}\) \(\newcommand{\nrem}{\mathsf{rem}}\) \(\newcommand{\ndiv}{\mathsf{div}}\) \(\newcommand{\ngcd}{\mathsf{gcd}}\) \(\newcommand{\ncoprime}{\mathsf{coprime}}\) \(\newcommand{\nlcm}{\mathsf{lcm}}\) \(\newcommand{\nmindiv}{\mathsf{mindiv}}\) \(\newcommand{\nisprime}{\mathsf{isPrime}}\) \(\newcommand{\npower}{\mathsf{power}}\) \(\newcommand{\nchoose}{\mathsf{choose}}\) \(\newcommand{\dom}{\mathsf{dom}}\) \(\newcommand{\cod}{\mathsf{cod}}\) \(\newcommand{\lists}[1]{\mathsf{List}(#1)}\) \(\newcommand{\nil}{\mathsf{nil}}\) \(\newcommand{\cons}{\mathsf{cons}}\) \(\newcommand{\uncons}{\mathsf{uncons}}\) \(\newcommand{\isnil}{\mathsf{isNil}}\) \(\newcommand{\tail}{\mathsf{tail}}\) \(\newcommand{\head}{\mathsf{head}}\) \(\newcommand{\foldr}{\mathsf{foldr}}\) \(\newcommand{\foldl}{\mathsf{foldl}}\) \(\newcommand{\tacunfoldN}{\mathsf{tacunfoldN}}\) \(\newcommand{\unfoldN}{\mathsf{unfoldN}}\) \(\newcommand{\dfoldr}{\mathsf{dfoldr}}\) \(\newcommand{\cfoldr}{\mathsf{cfoldr}}\) \(\newcommand{\bfoldr}{\mathsf{bfoldr}}\) \(\newcommand{\dbfoldr}{\mathsf{dbfoldr}}\) \(\newcommand{\lfoldr}{\mathsf{lfoldr}}\) \(\newcommand{\snoc}{\mathsf{snoc}}\) \(\newcommand{\revcat}{\mathsf{revcat}}\) \(\newcommand{\rev}{\mathsf{rev}}\) \(\newcommand{\last}{\mathsf{last}}\) \(\newcommand{\cat}{\mathsf{cat}}\) \(\newcommand{\addlength}{\mathsf{addlength}}\) \(\newcommand{\length}{\mathsf{length}}\) \(\newcommand{\head}{\mathsf{head}}\) \(\newcommand{\at}{\mathsf{at}}\) \(\newcommand{\map}{\mathsf{map}}\) \(\newcommand{\range}{\mathsf{range}}\) \(\newcommand{\zip}{\mathsf{zip}}\) \(\newcommand{\zipPad}{\mathsf{zipPad}}\) \(\newcommand{\unzip}{\mathsf{unzip}}\) \(\newcommand{\prefix}{\mathsf{prefix}}\) \(\newcommand{\suffix}{\mathsf{suffix}}\) \(\newcommand{\lcp}{\mathsf{lcp}}\) \(\newcommand{\lcs}{\mathsf{lcs}}\) \(\newcommand{\all}{\mathsf{all}}\) \(\newcommand{\any}{\mathsf{any}}\) \(\newcommand{\tails}{\mathsf{tails}}\) \(\newcommand{\inits}{\mathsf{inits}}\) \(\newcommand{\filter}{\mathsf{filter}}\) \(\newcommand{\elt}{\mathsf{elt}}\) \(\newcommand{\addcount}{\mathsf{addcount}}\) \(\newcommand{\count}{\mathsf{count}}\) \(\newcommand{\repeat}{\mathsf{repeat}}\) \(\newcommand{\sublist}{\mathsf{sublist}}\) \(\newcommand{\infix}{\mathsf{infix}}\) \(\newcommand{\select}{\mathsf{select}}\) \(\newcommand{\unique}{\mathsf{unique}}\) \(\newcommand{\delete}{\mathsf{delete}}\) \(\newcommand{\dedupeL}{\mathsf{dedupeL}}\) \(\newcommand{\dedupeR}{\mathsf{dedupeR}}\) \(\newcommand{\common}{\mathsf{common}}\) \(\newcommand{\disjoint}{\mathsf{disjoint}}\) \(\newcommand{\sublists}{\mathsf{sublists}}\) \(\newcommand{\take}{\mathsf{take}}\) \(\newcommand{\drop}{\mathsf{drop}}\) \(\newcommand{\takeBut}{\mathsf{takeBut}}\) \(\newcommand{\dropBut}{\mathsf{dropBut}}\) \(\newcommand{\takeWhile}{\mathsf{takeWhile}}\) \(\newcommand{\dropWhile}{\mathsf{dropWhile}}\)

This page is part of a series on Arithmetic Made Difficult.

In this post we will take a break and solve some equations in the natural numbers. These equations will be really simple, but we have to start somewhere! In the more familiar notation we will solve the following equations: \[\begin{array}{rrr} a+b=0 & \quad a+b=1 & \quad a+b=2 \\ ab=0 & \quad ab=1 & \quad ab=2 \end{array}\]

Our strategy is based on two of the Peano axioms. Specifically, (1) \(\zero = \next(m)\) has no solution \(m \in \nats\), and (2) every element of \(\nats\) is either \(\zero\) or of the form \(\next(m)\) for some \(m \in \nats\). Property (2) can be used to perform case analysis on \(\nats\), like so:

Let \(a,b \in \nats\). If \(\nplus(a,b) = \zero\), then \(a = b = \zero\).

Suppose \(\nplus(a,b) = \zero\). Note that either \(a = \zero\) or \(a = \next(m)\) for some \(m \in \nats\). If \(a = \next(m)\), then \[\zero = \nplus(a,b) = \nplus(\next(m),b) = \next(\nplus(m,b)),\] a contradiction. So we have \(a = \zero\). But now \(\zero = \nplus(\zero,b) = b\) as claimed.

The following generalization will be handy.

We have the following.

Every natural number is either \(\zero\), \(\next(\zero)\), or of the form \(\next(\next(m))\) for some \(m \in \nats\).
Every natural number is either \(\zero\), \(\next(\zero)\), \(\next(\next(\zero))\), or of the form \(\next(\next(\next(m)))\) for some \(m \in \nats\).

Let \(n \in \nats\). Either \(n = \zero\) or \(n = \next(k)\) for some \(k \in \nats\); but now either \(k = \zero\) or \(k = \next(m)\) for some \(m \in \nats\). So either \(n = \zero\), \(n = \next(\zero)\), of \(n = \next(\next(m))\) for some \(m \in \nats\).
Similar to (1).

This will allow us to use more detailed case analysis on \(\nats\).

Let \(a,b \in \nats\). If \(\nplus(a,b) = \next(\zero)\), then \((a,b)\) is either \((\zero,\next(\zero))\) or \((\next(\zero),\zero)\).

Note that either \(a = \zero\), \(a = \next(\zero)\), or \(a = \next(\next(m))\) for some \(m \in \nats\).

If \(a = \next(\next(m))\) for some \(m \in \nats\), we have \[\begin{eqnarray*} & & \next(\zero) \\ & \let{\nplus(a,b) = \next(\zero)} = & \nplus(a,b) \\ & \hyp{a = \next(\next(m))} = & \nplus(\next(\next(m)),b) \\ & \href{/posts/arithmetic-made-difficult/Plus.html#cor-plus-up-next} = & \next(\nplus(\next(m),b)) \\ & \href{/posts/arithmetic-made-difficult/Plus.html#cor-plus-up-next} = & \next(\next(\nplus(m,b))) \end{eqnarray*}\] so that \(\zero = \next(\nplus(m,b))\), a contradiction.
If \(a = \next(\zero)\), then we have \(\nplus(\next(\zero),\zero) = \next(\zero) = \nplus(\next(\zero),b)\), so that \(b = \zero\) as claimed.
If \(a = \zero\), then \(\next(\zero) = \nplus(\zero,b) = b\) as claimed.

Ain’t this fun!

Let \(a,b \in \nats\). If \(\nplus(a,b) = \next(\next(\zero))\), then \((a,b)\) is either \((\zero,\next(\next(\zero)))\) or \((\next(\zero),\next(\zero))\) or \((\next(\next(\zero)),\zero)\).

Note that either \(a = \zero\), \(a = \next(\zero)\), \(a = \next(\next(\zero))\), or \(a = \next(\next(\next(m)))\) for some \(m \in \nats\).

If \(a = \next(\next(\next(m)))\) for some \(m \in \nats\), we have \[\begin{eqnarray*} & & \next(\next(\zero)) \\ & \let{\nplus(a,b) = \next(\next(\zero))} = & \nplus(a,b) \\ & \hyp{a = \next(\next(\next(m)))} = & \nplus(\next(\next(\next(m))),b) \\ & \href{/posts/arithmetic-made-difficult/Plus.html#cor-plus-up-next} = & \next(\nplus(\next(\next(m)),b)) \\ & \href{/posts/arithmetic-made-difficult/Plus.html#cor-plus-up-next} = & \next(\next(\nplus(\next(m),b))) \\ & \href{/posts/arithmetic-made-difficult/Plus.html#cor-plus-up-next} = & \next(\next(\next(\nplus(m,b)))) \end{eqnarray*}\] so that \(\zero = \next(\nplus(m,b))\), a contradiction.
If \(a = \next(\next(\zero))\), then we have \[\begin{eqnarray*} & & \nplus(\next(\next(\zero)),\zero) \\ & \href{/posts/arithmetic-made-difficult/Plus.html#thm-plus-zero-right} = & \next(\next(\zero)) \\ & = & \nplus(\next(\next(\zero)),b) \end{eqnarray*}\] so that \(b = \zero\) as claimed.
If \(a = \next(\zero)\), then we have \[\next(\next(\zero)) = \nplus(\next(\zero),b) = \next(\nplus(\zero,b)) = \next(b)\] so that \(b = \next(\zero)\) as claimed.
If \(a = \zero\), then \(\next(\next(\zero)) = \nplus(\zero,b) = b\) as claimed.

And another.

Let \(a,b \in \nats\). If \(\nplus(a,b) = \next(\next(\next(\zero)))\), then \((a,b)\) is either \((\zero,\next(\next(\next(\zero))))\) or \((\next(\zero),\next(\next(\zero)))\) or \((\next(\next(\zero)),\next(\zero))\), or \((\next(\next(\next(\zero))),\zero)\).

If \(a = \zero\), then \(b = \next(\next(\next(\zero)))\) as claimed.

Suppose instead that \(a = \next(m)\) for some \(m\). Now \[\next(\nplus(m,b)) = \next(\next(\next(\zero))),\] so that \(\nplus(m,b) = \next(\next(\zero))\). There are then three possibilities.

If \(m = \zero\), then \(a = \next(\zero)\) and \(b = \next(\next(\zero))\).

If \(m = \next(\zero)\), then \(a = \next(\next(\zero))\) and \(b = \next(\zero)\).

If \(m = \next(\next(\zero))\), then \(a = \next(\next(\next(\zero)))\) and \(b = \zero\).

Okay this is boring. How about some equations with \(\ntimes\)?

Let \(a,b \in \nats\). If \(\ntimes(a,b) = \zero\), then either \(a = \zero\) or \(b = \zero\).

Suppose that neither \(a\) nor \(b\) is \(\zero\); then we have \(a = \next(h)\) and \(b = \next(k)\) for some \(h,k \in \nats\). Now \[\begin{eqnarray*} & & \zero \\ & = & \ntimes(a,b) \\ & = & \ntimes(\next(h),\next(k)) \\ & \href{/posts/arithmetic-made-difficult/Times.html#cor-times-up-next} = & \nplus(\ntimes(h,\next(k)),\next(k)) \\ & \href{/posts/arithmetic-made-difficult/Plus.html#thm-plus-next-right} = & \next(\nplus(\ntimes(h,\next(k)),k)) \end{eqnarray*}\] a contradiction. So we must have either \(a = \zero\) or \(b = \zero\). Note also that in either case we indeed have \(\ntimes(a,b) = \zero\).

woo

Let \(a,b \in \nats\). If \(\ntimes(a,b) = \next(\zero)\), then \((a,b)\) is \((\next(\zero),\next(\zero))\).

Suppose we have \(\ntimes(a,b) = \next(\zero)\). Note that either \(a = \zero\) or \(a = \next(\zero)\) or \(a = \next(\next(m))\) for some \(m \in \nats\).

If \(a = \zero\) we have \(\next(\zero) = \ntimes(a,b) = \zero\), a contradiction.
If \(a = \next(\zero)\), we have \[\next(\zero) = \ntimes(\next(\zero),b) = b\] as claimed.
If \(a = \next(\next(m))\) for some \(m \in \nats\), we have \[\begin{eqnarray*} & & \next(\zero) \\ & = & \ntimes(a,b) \\ & = & \ntimes(\next(\next(m)),b) \\ & = & \nplus(b,\ntimes(\next(m),b)). \end{eqnarray*}\] There are now two possibilties for \(b\). If \(b = \zero\), we have \(\zero = \next(\zero)\), a contradiction. If \(b = \next(k)\) with \(k \in \nats\), we have \[\next(\zero) = \nplus(\next(k),\ntimes(\next(m),\next(k)))\] so that \[\zero = \nplus(k,\ntimes(\next(m),\next(k))).\] But now we have \(k = \zero\) and \[\zero = \ntimes(\next(m),\next(\zero)) = \next(m),\] a contradiction.

One more:

Let \(a,b \in \nats\). If \(\ntimes(a,b) = \next(\next(\zero))\), then \((a,b)\) is either \((\next(\next(\zero)),\next(\zero))\) or \((\next(\zero),\next(\next(\zero)))\).

Suppose we have \(\ntimes(a,b) = \next(\next(\zero))\). Note that either \(a = \zero\) or \(a = \next(\zero)\) or \(a = \next(\next(\zero))\) or \(a = \next(\next(\next(m)))\) for some \(m \in \nats\).

If \(a = \zero\) we have \(\next(\zero) = \ntimes(a,b) = \zero\), a contradiction.
If \(a = \next(\zero)\), we have \[\next(\next(\zero)) = \ntimes(\next(\zero),b) = b\] as claimed.
If \(a = \next(\next(\zero))\), we have \[\ntimes(\next(\next(\zero)),\next(\zero)) = \next(\next(\zero)) = \ntimes(\next(\next(\zero)),b)\] so that \(b = \next(\zero)\) as claimed.
Suppose we have \(a = \next(\next(\next(m)))\) for some \(m \in \nats\). Now \[\begin{eqnarray*} & & \next(\next(\zero)) \\ & = & \ntimes(\next(\next(\next(m))),b) \\ & \href{/posts/arithmetic-made-difficult/Times.html#cor-times-up-next} = & \nplus(\ntimes(\next(\next(m)),b),b) \end{eqnarray*}\] If \(b = \zero\), then we have \(\next(\next(\zero)) = \zero\), a contradiction. Thus \(b = \next(k)\) for some \(k \in \nats\). This leaves two possibilities: \[(\ntimes(\next(\next(m)),\next(k)),\next(k))\] is either \((\next(\zero),\next(\zero))\) or \((\zero,\next(\next(\zero)))\). If \(b = \next(\zero)\), we have \(\next(\next(\zero)) = \next(\next(\next(m)))\) for some \(m\), a contradiction. If \(b = \next(\next(\zero))\) and \(\ntimes(\next(\next(m)),b) = \zero\), we have either \(b = \zero\) (a contradiction) or \(\next(\next(m)) = \zero\) (also a contradiction).

This is kind of ridiculous! But we’re doing number theory from first principles, so ridiculousness is kind of the point.