二重否定の除去 (¬¬P → P は成立するが P → ¬¬P のみ)

二重否定の除去は、¬¬PからPを導く推論である。古典論理では成立するが、構成的論理ではPの具体的な証明を得たことを意味しないため、一般には原理として採用されない。

仕組みと確認

対象の論理体系を明示し、P、¬P、¬¬Pの意味を真理値表または証明規則で比較する。プログラム対応では、否定の否定から実行可能な証人を構成できるかを確認する。

限界と注意点

古典論理の変形を直観主義論理や矛盾許容論理へ無条件に適用しない。未判定・エラー・欠損を二重否定の形式だけで処理しない。