BHK解釈 (Brouwer-Heyting-Kolmogorov interpretation)

BHK解釈は、命題の証明を、その命題に対応する構成的な証拠として読む。含意は証明を証明へ変換する手続き、存在命題は具体的な証人、連言は二つの証拠の組に対応する。

仕組みと確認

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

限界と注意点

BHK解釈は古典論理の真理値意味論と同じではない。構成的証拠を得たことを、安全性・性能・外部I/Oの保証と混同しない。