(オプション) 直観主義論理における証明論 (BHK解釈)

直観主義論理における証明論は、命題の真偽を外部から仮定するのではなく、証明を構成できることとして理解する。BHK解釈は、含意・連言・選言・存在命題にどのような証拠が対応するかを与える読み方である。

仕組みと確認

自然演繹や型理論で、各結合子の導入・除去規則と証明項を対応付ける。排中律や二重否定除去を使わず、実際に証人・変換手続き・分岐の証拠を構成できるかを確認する。

限界と注意点

構成的証明があることは、プログラムの停止、性能、外部サービスの可用性を保証しない。証明の消去、実行時に残る計算、非構成的な公理、I/O境界を別々に記述する。