直観主義論理とは？
ちょっかんしゅぎろんり
直観主義論理とは、数学的対象の存在を証明可能な構成によってのみ認め、排中律を認めない論理体系のことです。
直観主義論理（intuitionistic logic）とは、数学における構成主義的な立場から生まれた論理体系で、L.E.J.ブラウワーの直観主義数学を論理として形式化したものです。オランダの数学者ブラウワーは20世紀初頭、数学的真理は人間の精神による「構成（construction）」によって初めて確立されるという立場を提唱しました。
直観主義論理が古典論理と最も大きく異なる点は、排中律（P∨¬P、法則）を定理として認めないことです。古典論理では「PかP¬かのいずれかは必ず真」とされますが、直観主義論理では「Pを証明できるか、Pを反駁できるか」のどちらかが実際に示されなければ真偽は確定しないと考えます。
直観主義論理で認められない（または制限される）推論の例には以下があります。
- 排中律：P∨¬P（任意の命題について真か偽かが決まる）
- 二重否定除去：¬¬P → P（不可能ではないことが成立することを意味しない）
カリー＝ハワード対応により、直観主義論理の証明はプログラム（型付きラムダ計算）と対応することが知られており、型理論や関数型プログラミング、定理証明支援系（Coq、Agdaなど）の理論的基盤となっています。
使い方・例文
古典論理では「√2が有理数でないか、有理数である」は自明に真ですが、直観主義論理ではこの主張を受け入れるには実際にどちらかを示す構成が必要です。定理証明器でプログラムを検証する文脈で、直観主義論理の証明手法が実際に使われています。
この用語をシェア
最終更新: