User:Dfeuer/Double Induction Principle/Naturals

Theorem

Let $\RR$ be a relation such that:

For each natural number $n$, $n \mathrel \RR 0$

For any natural numbers $m$ and $n$:

$\paren {n \mathrel \RR m} \land \paren {m \mathrel \RR n} \implies m \mathrel \RR \paren {n^+}$

Then $n \mathrel \RR m $ for any naturals $m$ and $n$.

Proof

Let $P$ be the class of all rationals $n$ such that $0 \mathrel \RR n$.

$0 \in P$.

Suppose $n \in P$.

Then $0 \mathrel \RR n$ and $n \mathrel \RR 0$, so $0 \mathrel \RR n^+$.

Thus for each natural $n$: $n \in P \implies n^+ \in P$.

Thus $P$ contains all the naturals. That is, for each natural $n$, $0 \mathrel \RR n$.

Let $A$ be the class of all naturals $n$ such that for all naturals $m$, $m \mathrel \RR n$ and $n \mathrel \RR m$.

$0 \in A$.

Suppose that $n \in A$.

Let $B$ be the class of all naturals $m$ such that $m \mathrel \RR n^+$ and $n^+ \mathrel \RR m$.

We have shown that $0 \in B$.

Suppose that $m \in B$.

Then by the definition of $B$: $m \mathrel \RR n^+$ and $n^+ \mathrel \RR m$.

Thus $n^+ \mathrel \RR m^+$ because $\RR$ is double inductive.

By the definition of $A$, $m^+ \mathrel \RR n$ and $n \mathrel \RR m^+$.

Because $\RR$ is doubly inductive, $m^+ \mathrel \RR n^+$.

As we already have $n^+ \mathrel \RR m^+$, we see that $m^+ \in B$.

Thus $B$ is inductive, so it contains every natural.

Thus $A$ is inductive, so it contains every natural.