defining inequality of natural numbers by case-analysis

Question

If I add to Peano Arithmetic a relation (predicate?) symbol $\leq$ and an axiom $\forall n\forall m(n\leq m \leftrightarrow n=m \lor S(n)\leq m)$, can I prove $\forall n\forall m(n\leq m \to n\leq S(m))$?

Related question: How to compare Peano numbers?

Answer 1

You can see this post for reference to the logical theory of definition.

In oder to add to a first-order language a new predicate symbol $P$, we have to introduce an axiom defining it.

The defining axiom must be : $P(x_1, \ldots, x_n) \leftrightarrow \varphi(x_1, \ldots, x_n)$, where $\varphi$ is a formula of the "original" language, and thus must not contain the predicate $P$.

In first-order arithmetic with Peano's axiom we can introduce the binary predicate (or relation) $<$ through the axiom :

$n < m \leftrightarrow \exists z (m=n+S(z))$

and then :

$n \le m \leftrightarrow n < m \lor n = m$.

With these abbreviations, we can prove :

$n \le m \leftrightarrow n < S(m)$.

See Stephen Cole Kleene, Introduction to Metamathematics (1952) : $ ✳138a$, page 188.

---

---

Proof

For lemmas, I'll use the original Kleene's numeration; for Peano's axioms I'll call them $P1-P7$, following the order in Wiki's page.

Some preliminary lemmas:

$✳135b : 0 < S(n)$; proof from axioms $P3-P4$ : recursive axioms for sum.

$ ✳136 : 0 \le n$; proof by Induction on $n$, using $✳135b$.

$ ✳137 : n = 0 \lor (\exists m)(n = S(m))$; proof by cases from $✳136 : 0 < n \lor 0 = n$.

---

The following is an expanded version of the three-lines proof in Kleene's book of :

$ ✳138a : n \le m \leftrightarrow n < S(m)$.

Proof :

step 1

$n < S(m) \leftrightarrow (\exists z)(S(m)=n + S(z))$ --- abbreviation

[1] assume for $\exists$E : $S(m)=n+S(z)$;

$z = 0 \lor (\exists w)(z=S(w))$ --- from $✳137$

[1a] assume $z=0$

from [1] : $S(m)=n+S(0)$

$S(m)=n+S(0) \lor (\exists w)(S(m)=n+S(S(w)))$ --- by $\lor$I

Thus : $c=0, S(m)=n+S(z) \vdash S(m)=n+S(0) \lor (\exists w)(S(m)=n+S(S(w)))$ --- by $\exists$E.

[1b] assume $(\exists w)(z=S(w))$

In the same way, by $\exists$E, we prove : $(\exists w)(z=S(w)), S(m)=n+S(z) \vdash S(m)=n+S(0) \lor (\exists w)(S(m)=n+S(S(w)))$.

From [1a] and [1b] follows (proof by cases and $\rightarrow$I) :

$n < S(m) \rightarrow S(m)=n+S(0) \lor (\exists w)(S(m)=n+S(S(w)))$.

=\=\=\=

[2] assume $S(m)=n+S(0)$; by $\exists$I : $(\exists z)(S(m)=n+S(z))$;

also : $(\exists w)(S(m)=n + S(S(w))) \vdash (\exists z)(S(m)=n+S(z))$.

Then $S(m)=n+S(0) \lor (\exists w)(S(m)=n + S(S(w))) \rightarrow (\exists z)(S(m)=n+S(z))$ --- proof by cases and $\rightarrow$I.

Thus:

$S(m)=n+S(0) \lor (\exists w)(S(m)=n + S(S(w))) \rightarrow (n < S(m))$ --- abbreviation.

=\=\=\=

From [1] and [2] and $\leftrightarrow$I :

$n < S(m) \leftrightarrow S(m)=n+S(0) \lor (\exists w)(S(m)=n + S(S(w)))$

=\=\=\=

=\=\=\=

step 2

[1] Assume : $S(m)=n+S(0)$;

it follows that : $S(m)=S(n+0)$, by axiom $P4$, and : $m=n+0$, by axiom $P2$, and $m=n$.

Thus : $S(m)=n+S(0) \rightarrow m=n$.

In the same way : $m=n \rightarrow S(m)=n+S(0)$.

Thus, by $\leftrightarrow$I : $m=m \leftrightarrow S(m)=n+S(0)$.

=\=\=\=

[2] Assume $(\exists w)(S(m)=n+S(S(w)))$;

assume for $\exists$E : $S(m)=n+S(S(w))$; then $S(m)=S(n+S(w))$, and so : $m=n+S(w)$ and finally : $(\exists w)(m=n+S(w))$, by $\exists$I.

Thus :

$(\exists w)(S(m)=n+S(S(w))) \rightarrow (\exists w)(m=n+S(w))$.

In the same way : $(\exists w)(m=n+S(w)) \rightarrow (\exists w)(S(m)=n+S(S(w)))$

Finally :

$(\exists w)(m=n+S(w)) \leftrightarrow (\exists w)(S(m)=n+S(S(w)))$ --- by $\leftrightarrow$I.

=\=\=\=

=\=\=\=

step 3

From step 1 we have : $n < S(m) \leftrightarrow S(m)=n+S(0) \lor (\exists w)(S(m)=n + S(S(w)))$.

From step 2 we have : $(\exists w)(m=n+S(w)) \leftrightarrow (\exists w)(S(m)=n+S(S(w)))$.

We need also the fact that : $S(m)=n+S(0)=S(n+0)=S(n) \leftrightarrow m=n$.

Using tautologies [see $✳29a/b$, page 116] : $A \leftrightarrow B \vdash (A \lor C) \leftrightarrow (B \lor C)$ and $A \leftrightarrow B \vdash (C \lor A) \leftrightarrow (C \lor B)$, we have :

$n < S(m) \leftrightarrow m=n \lor (\exists w)(m=n+S(w))$

and finally, with the abbreviation for $n < m$ :

$n < S(m) \leftrightarrow m=n \lor n < m$

which is :

$n < S(m) \leftrightarrow n \le m$.

---

---

Notes

(A) Equivalently, we can start with :

$n \le m \leftrightarrow \exists z (m=n+z)$

and then define :

$n < m \leftrightarrow n \le m \land n \ne m$.

---

(B) We can instead use $<$ as a primitive symbols, adding to the usual (firts-oder) Peano's axioms the following recursive definition of $<$ :

$\forall x \lnot (x < 0)$

$\forall x \forall y (x < S(y) \leftrightarrow (x < y \lor x = y))$.