Curry–Howard対応

(証明はプログラムになる。)$\vdash \varphi$ の自然演繹導出に関する帰納法による。最後の規則が $\to$導入であり、仮定 $\psi$ のもとでの $\chi$ の部分証明から $\varphi=\psi\to\chi$ を導く場合:帰納法の仮定により、その部分証明は $x{:}A_\psi \vdash t : A_\chi$ である項 $t$ へ翻訳される(仮定は自由変数 $x$ になる);すると $\lambda x{:}A_\psi.\,t$ は閉じており型 $A_\psi\to A_\chi=A_\varphi$ を持つ。最後の規則が $\psi\to\chi$ と $\psi$ からの $\to$除去(モーダスポネンス)の場合:帰納法の仮定により項 $t_1 : A_\psi\to A_\chi$ と $t_2 : A_\psi$ が得られる;すると $t_1\,t_2 : A_\chi$。$\wedge$導入と $\wedge$除去の規則は、対 $\langle t_1,t_2\rangle$ と2つの射影へ対称的に翻訳される。証明体系のすべての規則に対応する項構成規則があるので、導出に関する帰納法は型 $A_\varphi$ の型付けされた閉じた項を生成する。

(プログラムは証明になる。)逆に、型付け導出 $\vdash t : A$ に関する帰納法による。各型付け規則——変数、抽象、適用、対、射影——は自然演繹の規則——仮定、$\to$導入、$\to$除去、$\wedge$導入、$\wedge$除去——とまったく同じ木の形を持つ。したがって同じ導出木を取り、すべての項を消去し、各型をそれが翻訳された論理式として読めば、これはまさに $\varphi$ の妥当な直観主義的証明である(ここで $A=A_\varphi$)。

2つの翻訳(証明 $\to$ 項、および項 $\to$ 証明)は導出木上で互いに構造的な逆写像である——一方は他方が行うことを規則ごとに正確に取り消す——ので、$\varphi$ が証明可能であることと $A_\varphi$ が住人を持つことはちょうど同値である。$\blacksquare$