ブラウワー、ハイティングによる形式化

BHK解釈は、命題の証明を、その命題に対応する構成的な証拠として読む考え方である。存在命題なら具体的な証人、含意なら証明を変換する手続きに対応させる。

読み方

結合子ごとの証拠の形を定め、証明が実際に構成できるかを確認する。プログラムと型の対応を考えるときは、実行可能性・停止性・副作用を別途明示する。

限界と注意点

古典論理の真理値解釈と同一ではなく、排中律や二重否定除去の扱いが異なる。数学的な証明の読み替えを、実装の安全保証と混同しない。