Prove that $(∀m)(∀n)(0 < m \rightarrow (m^− < n^-\leftrightarrow m < n))$

Question

$x < y$ is define as an abbreviation for $(∃u)(x + u^+ = y)$

Given the peano axiom and the 2 theorems about the predecessor $x^-$

These are:

$(∀x)¬(x^+ = 0)$

$(∀x)(∀y)(x+ = y^+ ⇒ x = y)$

Schema: for every expression P and variable symbol x, $P( 0) ⇒ (∀x)(P(x) ⇒ P(x^+)) ⇒ (∀x)P(x)$

$(∀x)(x + 0 = x)$

$(∀x)(∀y)(x + y^+ = (x + y)^+) $

$(∀x)(x.0 = 0)$

$(∀x)(∀y)(x.(y^+) = (x.y) + x)$

And

$\vdash 0^− = 0 $

$\vdash (∀n)((n^+)^− = n)$

Prove that $(∀m)(∀n)(0 < m ⇒ (m^− < n^− ⇐⇒ m < n))$

It seems to be something about induction, but I am not able to prove it now. Could someone please give a proof relaying on the axioms and the 2 theorems I gived above? Thanks!

Answer 1

Yes, the proof is by induction on $m$, with:

$P(m) := \forall n \ (0 < m \to [(p(m) < p(n)) \leftrightarrow (m < n)])$.

Note : for readibility, I'll use $p(n)$ in place of $n-$ and $s(n)$ in place of $n+$.

Basis : $P(0)$.

We have that $0 < 0$ is false, and thus $\mathsf {PA} \vdash \forall n \ (0 < 0 \to [(p(0) < p(n)) \leftrightarrow (0 < n)])$.

Induction step : assume $P(m)$ and prove $P(s(m))$.

We have to prove that: $0 < s(m) \to [(p(s(m)) < p(n)) \leftrightarrow (s(m) < n)]$.

Consider the two cases:

$\to$): if $p(s(m)) < p(n)$, then $s(m) < n$.

But $p(s(m))=m$, and thus: $\exists z \ (m + s(z) = p(n))$, and so: $s(m+z)=m+s(z)=p(n)$.

Thus: $s(s(m+z))=s(p(n))=n$ and finally: $s(m)+s(z)=n$, i.e. $\exists z \ (s(m) + s(z) = n)$, that means: $s(m) < n$.

Note : here we need: $\forall n \ (n \ne 0 \to s(p(n))=n)$. This is easily derived from: $∀n \ ((p(s(n))=n)$.

$\leftarrow$): if $s(m) < n$, then $p(s(m)) < p(n)$.

Thus $\exists z \ (s(m) + s(z) = n)$, and so: $p(s(m)+s(z))=p(n)$.

But, $p(s(m)+s(z))=p(s(m+s(z)))=m+s(z)=p(s(m))+s(z)$, and thus: $\exists z \ (p(s(m))+s(z)=p(n))$, i.e. $p(s(m)) < p(n)$.