Proving that Order for N is Anti-symmetric

Question

I'm having trouble deriving the following fact from the basic properties of $+_{\mathbb{N}}$ and the definition:

Definition. $\forall n, m \in \mathbb{N}: (n \geq m) \leftrightarrow (\exists a \in \mathbb{N}): n = m + a$.

Fact. $\forall a, b \in \mathbb{N}: (a \geq b ~\land~ b \geq a) \rightarrow a = b$.

I've tried several different strategies, but none works. I think the fact that 0 isn't the successor of any natural number is the key both in the base case and the inductive step, but I keep going in circles trying to make use of that (and other basic facts about addition on $\mathbb{N}$).

I would show you my notes, but there is really nothing of substance in them. I've made almost no progress since yesterday.

Answer 1

I think that we can prove it without Induction, using formal number theory, i.e. first-order Peano Arithmetic [see S.C.Kleene, Introduction to Metamathematics (1952), see pages 181-on].

I will use $>$ (less than) instead of $\ge$, with the definition :

$a > b \leftrightarrow \exists c (a = b +c')$.

In proving the fact , we must use proof by cases [see Kleene, page 98 : if $\Gamma, A \vdash C$ and $\Gamma, B \vdash C$, then $\Gamma, A \lor B \vdash C$].

Assume $a \ge b$ i.e. $a > b \lor a = b$.

Assume $b \ge a$ i.e. $b > a \lor a = b$.

We have four cases, three of which have already $a = b$ in the assumptions.

So, we need only to take care of case : $a > b$ and $b > a$.

From : $a > b$ and $b > a$, we have that $a > a$ [by *134a, Kleene page 187]

But now, unwinding the definition, we have that : $a = a + e'$.

From the last formula [we are using $\exists$-elim, see Kleene page 99] and using : $a + 0 = a$, [Axiom 18], by properties of equality and of sum [*102 and *132, see Kleene pages 183 and 186] we get : $e' = 0$, contradicting Axiom 15: $\lnot a' = 0$.

We can use now *10a [page 113] : $\lnot A \supset (A \supset B)$ with the above contradiction, to derive : $a = b$.

Answer 2

I think this proves it, but I'm not too sure. I'd appreciate any help.

We proceed by induction on $a$ in the Fact above. Let $\varphi(x) \equiv (x \geq b ~\land~ b \geq x) \rightarrow (x=b)$.

The base case $\phi(0)$ is easy to verify. $\checkmark$

Aassume: $$\fbox{1}~\varphi(n) \equiv (n \geq b ~\land~ b \geq n) \rightarrow (n=b).$$

We want: $$\varphi(n')\equiv (n' \geq b ~\land~ b \geq n') \rightarrow (n'=b),$$

so we assume: $$\fbox{2}~(n' \geq b ~\land~ b \geq n')$$

with the hope of deriving $(n' = b)$. From (2) we have: $$\fbox{2a}~n' \geq b; \\ \fbox{2b}~b \geq n'.$$

By Definition above: $$\fbox{2a}~(n' \geq b) \equiv (\exists \alpha)~ n' = b + \alpha; \\ \fbox{2b}~(b \geq n') \equiv (\exists \beta)~ b = n' + \beta.$$

Combining the two we get: $$(\exists \alpha, \beta)~ n' = n' + \beta + \alpha; \\ (\exists \alpha, \beta)~ n + 1 = n + 1 + \beta + \alpha; \\ (\exists \alpha, \beta)~ n + 1 = n + \beta + \alpha + 1; \\ (\exists \alpha, \beta)~ n + 1 = n + (\beta + \alpha)'.$$

We have a cancellation law for addition that says: $\forall a,b,c \in \mathbb{N}: [a + b = a + c] \Longrightarrow b = c$. Using that with the previous result we know that: $$1 = (\beta + \alpha)'.$$

Since $(1 := 0')$ we get: $$\fbox{3}~\alpha + \beta = 0.$$

To show that $n' = b$, it will suffice to show that $\alpha = \beta = 0$. We proceed indirectly, by assuming, for contradiction, that: $$(n' \not = b) \\\equiv \lnot (\alpha = \beta = 0) \\\equiv (\alpha \not= 0 \lor \beta \not= 0).$$

Now we proceed by cases.

$\rhd$ Suppose $(\alpha \not= 0)$. Then we know that $\alpha$ is the successor of some number $\eta$, i.e., $(\exists \eta \in \mathbb{N})~\eta' = \alpha$. With this and (3) we get: $(\exists \eta \in \mathbb{N})~\eta' + \beta = 0$. By a basic property of $+$ this is equivalent to $(\exists \eta \in \mathbb{N})~(\eta + \beta)' = 0$. But we know that $0$ isn't the successor of any natural number and that $(\eta + \beta) \in \mathbb{N}$, so we have a contradiction.

$\rhd$ Suppose $(\beta \not= 0)$. Similar steps here, ending in $\bot$.

Since both cases lead to a contradiction we must have: $$\lnot(\alpha \not= 0 \lor \beta \not= 0) \\ \equiv (\alpha = 0 \land \beta = 0) \\ \equiv (\alpha = \beta = 0).$$

This means by (2) that $n' = b$, which closes the induction. $\checkmark$