\(t, f\) はそれぞれ真偽を示すシンボルとする. \(\top, \bot\) などとも書かれる.
if 式とは \(\mathrm{if}~a~b~c\) と書かれる式のこと. 第一引数 \(a\) を条件部という. \(b\) が Then 部、\(c\) が Else 部という. 式全体の値は、\(a=t\) なら \(b\) 、\(a=f\) なら \(c\). \(a\) がそれ以外の値を取ることはないようにする.
任意の \(a,b\) について \[b \equiv \mathrm{if}~a ~ b ~ b\] が成立する. これはつまり、条件部がなんであろうが Then 部も Else 部も同じ値なら if 全体もその値であると言っている.
if 文の第二引数 (Then部) では第一引数 (条件部) が \(t\) であることを用いて良い. 例えば次が成立する. \[\mathrm{if}~a~b~c \equiv \mathrm{if}~a~(\mathrm{if}~a~b~d)~c\]
同様に、if文の第三引数 (Else部) は第一引数 (条件部) が \(f\) であることを用いて良い. \[\mathrm{if}~a~b~c \equiv \mathrm{if}~a~b~(\mathrm{if}~a~d~c)\]
ところで式 \(X\) を次のようなものとして定義する: \[X \equiv \mathrm{if}~X ~ f ~ t\]
\(X\) は if の第一引数 (条件部) にあるので \(t\) または \(f\) である.
\(t=f\) を示す.
公理1により \[f \equiv \mathrm{if}~X ~ f ~ f\]
公理2, 2' を順に用いて、 \[\begin{align*} f & \equiv \mathrm{if}~X ~ f ~ f \\ & \equiv \mathrm{if}~X ~ (\mathrm{if}~X~f~t) ~ f \\ & \equiv \mathrm{if}~X ~ (\mathrm{if}~X~f~t) ~ (\mathrm{if}~X~t~f) \end{align*}\]
次に、中の深いところの2つの \(X\) を定義 \(\mathrm{if}~X~f~t\) で置き換える.
\[\begin{align*} f & \equiv \mathrm{if}~X ~ (\mathrm{if}~ \color{red}{(\mathrm{if}~X~f~t)} ~f~t) ~ (\mathrm{if}~ \color{blue}{(\mathrm{if}~X~f~t)} ~t~f) \end{align*}\]
1つめの \(\color{red}{(\mathrm{if}~X~f~t)}\) に公理2 を適用する. つまりこの \(X\) は最も外側の if の Then 部にあるから \(X=t\) である. 従って \(\color{red}{\mathrm{if}~X~f~t} \equiv \color{red}{\mathrm{if}~t~f~t} \equiv \color{red}{f}\) だとしてよい. 同様に公理2'から、 \(\color{blue}{(\mathrm{if}~X~f~t)}\) は \(\color{blue}{t}\) だとしてよい.
\[\begin{align*} f & \equiv \mathrm{if}~X ~ (\mathrm{if}~ \color{red}{(\mathrm{if}~X~f~t)} ~f~t) ~ (\mathrm{if}~ \color{blue}{(\mathrm{if}~X~f~t)} ~t~f) \\ & \equiv \mathrm{if}~X ~ (\mathrm{if}~\color{red}{f}~f~t) ~ (\mathrm{if}~\color{blue}{(\mathrm{if}~X~f~t)} ~t~f)\\ & \equiv \mathrm{if}~X ~ (\mathrm{if}~\color{red}{f}~f~t) ~ (\mathrm{if}~\color{blue}{t}~t~f) \end{align*}\]
2つある if 文は条件部が明らかなので評価する. \[f \equiv \mathrm{if}~X ~ t ~ t\]
最後に公理1を再び適用すると、 \[f \equiv t\] を得る.