排中律 (P ∨ ¬P) の不承認

排中律は、任意の命題PについてPまたは¬Pが成り立つという原理である。古典論理では採用されるが、構成的論理では、どちらかの証明を具体的に構成できるとは限らないため一般には採用しない。

仕組みと確認

対象の論理体系と証明の意味を固定し、排中律を使う証明と使わない証明を区別する。プログラム対応では、判定手続きや証人を実際に構成できるかを確認する。

限界と注意点

「まだ分かっていない」と「Pまたは¬Pのどちらかが証明済み」は同じではない。データや監視の欠損を、古典論理の二値へ無理に押し込めない。