How do I prove formally that for all natural numbers $a\cdot S(c)=b\cdot S(c)\implies a\cdot c=b\cdot c$

Question

Natural numbers, addition, multiplication, and the successor function S, are defined in the wikipedia article regarding Peano axioms.

https://en.m.wikipedia.org/wiki/Peano_axioms

Originally I was trying to prove that for all natural numbers $\neg c=0 \implies (a\cdot c=b\cdot c \implies a=b)$

But I was struggling to prove the induction step regarding induction on c, hence my question. I assumed this was the most straightforward way to prove the statement, but if there is another method that does not include proving the statement in the title, that is also fine.

Answer 1

Let's prove some preliminar properties. I'm assuming commutativity, associativity and the distributive property (which are true by the way).

I need some other useful properties (you can read only the statement and skip if you are not interested or you already know them).

Integrity $$ab=0\implies a=0\mbox{ or }b=0$$

Proof. Suppose $a,b\neq 0$, then $a=S(a')$ and $b=S(b')$. Hence $$0=ab=S(a')b=a'b+b=a'b+S(b')=S(a'b+b')$$ You get a contradiction because $0$ is not in the image of $S$.

Simplification law for the sum: $$a+c=b+c\implies a=b$$ Proof. You prove it by an easy induction.

Existence of a unicque solution of exactly one of the following equations: $$a+x=b\mbox{ or }a=b+x$$

Proof. Consider the case $a\neq b$ for the rest of the proof.

At most one of the equation has solution: Assume $a+x_1=b$ and $b+x_2=a$ then substituting you get $b+x_2+x_1=b$.Since $x_1$ and $x_2$ cannot be both zero (otherwise you would get $a=b$ which is not the case) exactly one must be non zero, whitout loss of generality suppose $x_1\neq 0$, then $x_1=S(x_1')$ hence $$b=b+S(x_1')+x_2\implies b=b+S(x_1'+x_2)$$ You can simplify to $S(x_1'+x_2)=0$ and get a contraddiction. Hence at most one equation could have a solution.

Uniqueness of the solution: Assume $a+x_1=b=a+x_2$, by simplifying you get $x_1=x_2$.

Existence of a solution for one of the equations: By induction on $a$.

For $a=0$ the equation $a+x=b$ has solution $x=b$. Assume the existence for $a$ and consider the two equations $$ S(a)+x=b \mbox{ and } S(a)=b+x$$ If $b=0$ then the second one has solution $x=S(a)$, otherwise $b=S(b')$ and rewriting the first and second one you get $$S(a)+x=S(b')\mbox{ and }S(a)=S(b')+x$$ since for $a$ the statement holds,one of the equations $$a+x=b'\mbox{ or }a=b'+x$$ has solution $x_1$, assume the first. Then taking successor of both left and right side of the equation you get $S(a+x)=S(b')$. Hence $$S(a)+x=b$$ You prove the second case (where the second equation for $a$ holds) in the same way.

This third property in the case $a=b$ is easier to prove, and in this case there is only one equation.

Your Statement Now we have all the machinery to prove that $$c\neq 0 \mbox{ then } ac=bc\implies a=b$$

Proof. Assume $a\neq b$ then it must be $a=b+x$ or $a+x=b$ for some $x$. Without loss of generality assume the first, then distributing you get $$(b+x)c=bc \implies bc+xc=bc$$ and simplifying you get $$xc=0$$ Since $c\neq0$ it must be $x=0$. Hence $a=b$.

Answer 2

Mathematical induction is given as follows:

$1.\,\,P(0)\\2.\,\,(\forall n \in \mathbb{N})[P(n) \implies P(S(n))]\\3.\therefore (\forall n \in \mathbb{N})[P(n)]$

For this proof we will have to define P(x) to be $(\forall b,c \in \mathbb{N})\big[\neg c=0[x \cdot c=b\cdot c\implies b=x]\big]$. Thus the outline of the proof will be

$1. (\forall b,c \in \mathbb{N})\big[\neg c=0\implies[0 \cdot c=b\cdot c\implies b=0]\big]\\ 2.(\forall x \in \mathbb{N})\bigg[\big[\neg c=0\implies(\forall b,c \in \mathbb{N})[x \cdot c=b\cdot c\implies b=x]\big]\implies\big[\neg c=0\implies(\forall b,c \in \mathbb{N})[S(x) \cdot c=b\cdot c\implies b=S(x)\big]\bigg]\\3.(\forall a,b,c \in \mathbb{N})\big[\neg c=0\implies[a \cdot c=b\cdot c\implies a=b]\big]$

Currently I am unaware of how to prove the consequent of statement 2. given its antecedent.I am able to answer your second question. There is indeed an alternative method to prove the statement $(\forall a,b,c \in \mathbb{N})[\neg c=0\implies[a\cdot c=b\cdot c \implies a=b]\big]$ involving a proof by contradiction.

The proof goes as follows

$1.(\forall a,b \in \mathbb{N})[a<b\lor a=b\lor a>b]\\2.(\forall a,b,c \in \mathbb{N})\big[\neg c=0\implies [a<b\implies ac<bc]\big]\\3.(\forall a,b,c \in \mathbb{N})\big[\neg c=0\implies [a>b\implies ac>bc]\big]\\4.(\forall a,b,c \in \mathbb{N})\big[\neg c=0\implies [a<b\lor a>b\implies ac\neq bc]\big]\\5. \therefore (\forall a,b,c \in \mathbb{N})\big[\neg c=0\implies [ac=bc \implies \neg(a<b\lor a>b)]\big]\\6. \therefore (\forall a,b,c \in \mathbb{N})\big[\neg c=0\implies [ac=bc \implies a=b]\big]\\$

Hope this helps.