Curry–Howard对应

(证明变为程序。)对 $\vdash \varphi$ 的自然演绎推导做归纳。若最后一条规则是 $\to$-引入,由假设 $\psi$ 下 $\chi$ 的子证明推出 $\varphi=\psi\to\chi$:由归纳假设,该子证明被翻译为项 $t$,满足 $x{:}A_\psi \vdash t : A_\chi$(假设变为自由变量 $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$ 与两个投影。证明系统的每条规则都有对应的项构造规则,因此对推导做归纳就能产生类型为 $A_\varphi$ 的良类型闭项。

(程序变为证明。)反过来,对类型推导 $\vdash t : A$ 做归纳。每条类型规则——变量、抽象、应用、配对、投影——与某条自然演绎规则——假设、$\to$-引入、$\to$-消去、$\wedge$-引入、$\wedge$-消去——具有完全相同的树形结构。于是取同一棵推导树,擦除所有项,并把每个类型读作它所翻译自的公式:这恰好就是 $\varphi$ 的一个合法的直觉主义证明(其中 $A=A_\varphi$)。

由于这两个翻译(证明 $\to$ 项,以及项 $\to$ 证明)在推导树上互为结构逆——一个逐规则地精确撤销另一个所做的——$\varphi$ 可证恰好当 $A_\varphi$ 被居留时成立。$\blacksquare$