カリー＝ハワード同型対応
次の図は ( β → α ) → ( γ → β ) → γ → α {\displaystyle (\beta \to \alpha )\to (\gamma \to \beta )\to \gamma \to \alpha } の自然演繹における証明である。簡単のため、文脈 Γ ⊢ {\displaystyle \Gamma \vdash } は省略してある。
x : β → α y : γ → β z : γ y z : β x ( y z ) : α λ z . x ( y z ) : γ → α λ y . λ z . x ( y z ) : ( γ → β ) → γ → α λ x . λ y . λ z . x ( y z ) : ( β → α ) → ( γ → β ) → γ → α {\displaystyle {\dfrac {\dfrac {{\begin{matrix}{}\\x:\beta \rightarrow \alpha \end{matrix}}\quad {\dfrac {y:\gamma \rightarrow \beta \quad z:\gamma }{yz:\beta }}}{\dfrac {x\,(yz):\alpha }{\lambda z.
型付きCL項の構成規則は以下に示す表の右の列を参照されたい。カリーは各々の行が同型に対応していることを指摘した。この直観論理との対応の制限は、古典論理の恒真式、例えばパースの法則 ( ( α → β ) → α ) → α {\displaystyle ((\alpha \to \beta )\to \alpha )\to \alpha } などがこの対応から締め出されていることを意味する。
もっと抽象的なレベルから見ると、この対応は以下の表のようにして述べ直すことができる。とくに、ヒルベルト流の推論体系における演繹定理(のメタ証明)は、コンビネータ論理における抽象の除去手続きと対応している。
この対応によって、コンビネータ論理の結果をヒルベルト流の推論体系の結果に翻訳できる。その逆もまた同様である。例えば、CL項の簡約はヒルベルト流の証明図の簡約手続きと見ることができる。また、正規なCL項は正規な証明図へと翻訳される。ここで正規とは、これ以上簡約できないことを意味する。正規化定理は型付け可能なCL項は必ず正規形を持つという定理であるが、これはヒルベルト流の証明図は必ず正規形を持つという結果に翻訳できる。
反対に、直観主義論理における例えばパースの法則の証明不能性は、コンビネータ論理における次の結果に翻訳できる:型 ( ( α → β ) → α ) → α {\displaystyle ((\alpha \to \beta )\to \alpha )\to \alpha } を持つCL項は存在しない。
スティーヴン・コール・クリーネの実現可能性解釈は、直観主義的算術の証明を再帰的関数とその関数が論理式を実現していることを表す論理式の証明とに分離する。これにより、例えば「任意の自然数 a と b に対して、a と b を割り切る最大の自然数 c が存在する」ことを直観主義的に証明できたならば、ここから最大公約数を計算する再帰的関数と、それが最大公約数を計算していることの証明を抽出できる。
ゲオルク・クライゼルにより変更された実現可能性解釈を高階の直観主義論理に適用することで、もとの論理式の証明からそれを実現する単純型付けされたラムダ項を帰納的に抽出できることが示せる。命題論理の場合、これはカリー=ハワード対応のステートメントと一致する:抽出されたラムダ項はもとの証明(をラムダ項と見做したもの)と一致し、実現可能性のステートメントは抽出されたラムダ項がもとの論理式の意味する型を持つということの言い換えである。
クルト・ゲーデルのディアレクティカ解釈は計算可能汎関数を備えた直観主義的算術(のある拡張)を実現する。これのラムダ計算との繋がりは自然演繹ほど明白ではない。
de Queiroz, Ruy J.G.B. (1994), “Normalisation and language-games”, Dialectica, 48, pp. 83–123, http://www3.interscience.wiley.com/journal/119262585/abstract?CRETRY=1&SRETRY=0 . (Early version presented at Logic Colloquium '88, Padova. Abstract in JSL 55:425, 1990.)
de Queiroz, Ruy J.G.B. (2001), “Meaning, function, purpose, usefulness, consequences – interconnected concepts”, Logic Journal of the Interest Group in Pure and Applied Logics, 9, pp.
693–734, http://jigpal.oxfordjournals.org/cgi/content/abstract/9/5/693 . (Early version presented at Fourteenth International Wittgenstein Symposium (Centenary Celebration) held in Kirchberg/Wechsel, August 13–20, 1989.)
de Queiroz, Ruy J.G.B. (2008), “On reduction rules, meaning-as-use and proof-theoretic semantics”, Studia Logica, 90, pp. 211–247, http://www.springerlink.com/content/27nk266126k817gq/ .