How to prove (if it is even needed) if $ac \leq bc$, then $a \leq b$ using Peano axioms

Question

I would like to know about the properties of inequalities in Peano arithmetic. Do they need to be proven or are they true by definition? Especially the following two properties:

1. if $ac \leq bc$, then $a \leq b$,
2. if $a + c \leq b + c$, then $a \leq b$.

Answer 1

Note that for $c =0$ we have $ac \le bc$ for any $a$, and $b$ ... So I assume that what you really want to prove is:

$\forall a \forall b \forall c (c \not = 0 \rightarrow (ac \le bc \rightarrow a \le b))$

Now, to do this, you might think that induction on $c$ would be able to do this fairly quickly, but that is not true. In fact, compared to the method I suggest, induction would only add unnecessary lines to the proof.

Instead, use Trichotomy: $\forall a \forall b ( a < b \lor a = b \lor b<a)$

together with the basic definition of $< $ or $\le$, whichever you have defined.

First prove $\forall a \forall b \forall c (c \not =0 \rightarrow (a < b\rightarrow ac < bc))$, which is easy to do: If $c \not = 0$ and $a < b$, then $a + s(d) = b$ for some $d$, and $c = s(e)$ for some $e$. Thus: $ac = as(e) = ae + a < ae + s(d)e + a + s(d) =(a + s(d))e + a + s(d)=(a+s(d))s(e)=bc$.

Once you have that, you can prove $\forall a \forall b \forall c (c \not = 0 \rightarrow (ac \le bc \rightarrow a \le b))$ by assuming $ac \le bc$, and then ruling out $b < a$ given what you just proved (you'll also need asymmetry and irreflexivity of $<$). So, if $b<a$ is ruled out then $a \le b$ using Trichotomy. If you don't have Trichotomy, you can prove Trichotomy using Induction.

To prove that $\forall a \forall b \forall c (a+c \le b +c \rightarrow a \le b)$, again first prove its 'converse': $\forall a \forall b \forall c ( a <b \rightarrow a +c < b +c)$. This is easy to do: If $a < b$, then $a + s(d) = b$ for some $d$, and hence $(a + s(d)) + c = b + c$, and thus by Association $(a + c) + s(d) = b + c$, and so $a + c < b + c$.

Once you have that, the proof for $\forall a \forall b \forall c (a+c \le b +c \rightarrow a \le b)$ is as follows: assume $a + c \le b + c$. Then if $b < a$ you get $b +c < a + c$ which by asymmetry and irreflexivity of $<$ means that $\neg (a + c \le b + c)$ and hence you get a contradiction. Hence, $\neg b < a$, and so by Trichotomy you are left with $a \le b$.