加算の公理は\(x+0=x,x+S(y)=S(x+y)\)。\(x\leq y\)の定義は\(\exists z\in\mathbb{N}[x+z=y]\)。
【補題1】任意の\(a\in\mathbb{N}\)に対し\(0+a=a\)が成り立つ。
（証明）帰納法による。\(0+0=0\)。また\(0+a=a\)のもと\(0+S(a)=S(0+a)=S(a)\)。■
【補題2】任意の\(a,b\in\mathbb{N}\)に対し\(a+S(b)=S(a)+b\)が成り立つ。
（証明）\(a\)を任意に固定し、\(b\)に関する帰納法を用いる。\(a+S(0)=S(a+0)=S(a)=S(a)+0\)。また\(a+S(b)=S(a)+b\)のもと、\(a+S(S(b))=S(a+S(b))=S(S(a)+b)=S(a)+S(b)\)。■
【定理】任意の\(x,y\in\mathbb{N}\)に対し、\(y\leq x\vee x\leq y\)が成り立つ。
（証明）\(y\in\mathbb{N}\)を任意に固定し、\(\varphi_y(x):y\leq x\vee x\leq y\)とおく。\(x\)についての帰納法により、\(\forall x[\varphi_y(x)]\)を導く。
[I]補題1により、\(0+y=y\)から\(0\leq y\)、したがって\(\varphi_y(0)\)が成立する。
[II]\(\varphi_y(x)\)を仮定し、\(\varphi_y(S(x))\)を導く。
(ア)\(y\leq x\)のとき：\(y+z=x\)（\(z\in\mathbb{N}\)）とおける。\(y+S(z)=S(y+z)=S(x)\)により\(y\leq S(x)\)。
(イ)\(x\leq y\)のとき：\(x+w=y\)（\(w\in\mathbb{N}\)）とおける。
(イの1)\(w=0\)のとき：\(x+0=y\)から、\(y+S(0)=S(y+0)=S(y)=S(x+0)=S(x)\)、したがって\(y\leq S(x)\)。
(イの2)\(w\neq0\)のとき：\(w=S(v)\)なる\(v\in\mathbb{N}\)がとれる。補題2を用いて\(S(x)+v=x+S(v)=x+w=y\)、したがって\(S(x)\leq y\)。
以上により、いずれの場合も\(y\leq S(x)\)か\(S(x)\leq y\)の少なくとも一方が成り立つから、\(\varphi_y(S(x))\)が成立する。 ■
