BHK 解釈

論理式 $A$ の証明とは何かを、論理記号に沿って次のように説明する（形式的な定義ではなく、意味の説明である）。

• $A\wedge B$ の証明とは、$A$ の証明と $B$ の証明の組である。
• $A\vee B$ の証明とは、$A$ の証明か $B$ の証明のどちらかと、どちらであるかの印である。
• $A\to B$ の証明とは、$A$ の任意の証明を $B$ の証明に変換する方法（構成）である。
• $\bot$ の証明は存在しない。$\neg A$ の証明は、$A$ の証明を $\bot$ の証明に変える方法である。
• $\forall x\,A(x)$ の証明とは、各 $x$ に $A(x)$ の証明を対応させる方法、$\exists x\,A(x)$ の証明とは、具体的な $a$ と $A(a)$ の証明の組である。