直観主義論理とは？

ちょっかんしゅぎろんり

構成的証明のみを認め、排中律を公理として受け入れない論理体系です。

直観主義論理（intuitionistic logic）はブラウワーの構成主義数学を基盤にアロンゾ・ハイティングが形式化した論理体系で、命題の証明とはその構成的証明（計算的な証拠）の提示であるとする。排中律 P ∨ ¬P を公理として採用せず、二重否定除去 ¬¬P → P も一般には成立しない。カリー・ハワード対応を通じて計算理論と密接に結びつく。