次のように述べることができるだろう。 前もって、命題変数と型名（型記号、型変数）の対応があるとする。 命題論理式と型表現（type expression）の翻訳をτで示す。 命題論理式Pの（仮定なし）証明と、τ(P)で型付けされた閉じたラムダ式が対応する。 証明の…