カリー＝ハワード対応（含意の断片）

型の基本型 $o_i$ を命題変数 $p_i$ と同一視する。

1. $x_1{:}A_1,\ldots,x_n{:}A_n\vdash M:B$ ならば $\{A_1,\ldots,A_n\}\vdash B$。
2. $\{A_1,\ldots,A_n\}\vdash B$ ならば、ある項 $M$ について $x_1{:}A_1,\ldots,x_n{:}A_n\vdash M:B$（$A_i$ には重複がないとする）。
3. さらに、仮定に名前を付けた自然演繹の導出と、型付けの導出（したがって、補題 2.2 により型付き項）とは一対一に対応する。この対応のもとで、β 基 $(\lambda x{:}A.M)N$ は「$({\to}\mathrm{I})$ で $A\to B$ を導いた直後に $({\to}\mathrm{E})$ で使う」という回り道に対応し、その縮約 $M[x:=N]$ は「$A$ の仮定を使っていた箇所に $A$ の証明 $N$ を直接差し込む」ことに対応する。