等式と不等式を定義しましょう。まずは不等式から定義します。
$x\geq y$を判定する関数$\textbf{G}$を下記のように定義します。
$$\textbf{G}\equiv(\lambda xy.\textbf{Z}(x\textbf{P}y))$$
3>2を証明する
$3>2$を判定します。
$\textbf{G32}\equiv
(\lambda xy.\textbf{Z}(x\textbf{P}y))\textbf{32}\rightarrow
\textbf{Z}(\textbf{3P2})\rightarrow
\textbf{Z}((\lambda sz.s(s(s(z))))\textbf{P2})$
$\rightarrow\textbf{Z}(\textbf{P}(\textbf{P}(\textbf{P}(\textbf{2}))))
\rightarrow
\textbf{Z}(\textbf{P}(\textbf{P}(\textbf{P2})))
\rightarrow\textbf{Z}(\textbf{P}(\textbf{P}(\textbf{1})))
\rightarrow\textbf{Z}(\textbf{P}(\textbf{0}))$
ここで算術編の結果$\textbf{P2}\rightarrow\textbf{1}、\textbf{P1}\rightarrow\textbf{0}$を使ったので。
更に$\textbf{P}(\textbf{0})$を求めます。
$\textbf{P0}
\rightarrow(\lambda n.(n\Phi(\textbf{B}))\textbf{F})\textbf{0}
\rightarrow(\textbf{0}\Phi(\textbf{B}))\textbf{F})
\rightarrow((\lambda sz.z)\Phi(\textbf{B}))\textbf{F}$
$\rightarrow(\lambda z.z)\textbf{F}
\rightarrow\textbf{F}$
この結果から、$\textbf{G32}\rightarrow
\textbf{ZF}
\rightarrow(\lambda x.x\textbf{F}\neg\textbf{F})\textbf{F}
\rightarrow\textbf{FF}\neg\textbf{F}$
$\rightarrow(\textbf{FF}\neg)\textbf{F}
\rightarrow(\neg)\textbf{F}
\rightarrow\textbf{T}
$となり、$3>2$であることを証明できました。
2>3を計算する
逆の場合の$2＞3$はどうなるでしょうか。
$\textbf{G23}
\rightarrow(\lambda xy.\textbf{Z}(x\textbf{P}y))\textbf{23}
\rightarrow\textbf{Z}(\textbf{2P3})
\rightarrow\textbf{Z}((\lambda sz.s(s(z)))\textbf{P3})$
$\rightarrow\textbf{Z}(\textbf{P}(\textbf{P}(\textbf{3})))
\rightarrow\textbf{Z}(\textbf{P}(\textbf{2}))
\rightarrow\textbf{Z}(\textbf{1})
\rightarrow(\lambda x.x\textbf{F}\neg\textbf{F})\textbf{1}
\rightarrow\textbf{1}\textbf{F}\neg\textbf{F}$
$\rightarrow(\lambda sz.s(z))\textbf{F}\neg\textbf{F}
\rightarrow\textbf{F}(\neg)\textbf{F}
\rightarrow\textbf{F}$
$2>3$は偽となりました。
2=2を計算する
$\textbf{G22}
\rightarrow(\lambda xy.\textbf{Z}(x\textbf{P}y))\textbf{22}
\rightarrow\textbf{Z}(\textbf{2P2})
\rightarrow\textbf{Z}((\lambda sz.s(s(z)))\textbf{P2})$
$\rightarrow\textbf{Z}(\textbf{P}(\textbf{P}(\textbf{2})))
\rightarrow\textbf{Z}(\textbf{P}(\textbf{1}))
\rightarrow\textbf{Z}(\textbf{0})
\rightarrow\textbf{T}$
Haskellの式は後ほど。