直観主義論理または直観論理（英: intuitionistic logic）、あるいは構成的論理（英: constructive logic）とは、ある種の論理体系であり、伝統的な真理値の概念が構成的証明
の概念に置き換わっている点で古典論理とは異なる。例えば古典論理では、全ての論理式に真か偽の真理値 ( { ⊤ , ⊥ } {\displaystyle \{\top ,\bot \}} ) が割り当てられる。このときその真理値に対する直接的なエビデンスを持つか否かは問題にしない。これはどのような曖昧な命題においても「真か偽かが決定可能である」ということを意味する。対照的に直観主義論理では確定的に論理式に真理値を割り当てるのではなく、それが真であるとは「直接的なエビデンス」つまり「証明」があることと見做す。証明論的な視点から見ると、直観主義論理は古典論理の制限であって排中律や二重否定除去が公理として許容されないものである。排中律や二重否定除去はいくつかの論理式に対しては個別に証明できることがあるけれども、古典論理のように普遍的に成立することはない。
直観主義論理の色々な意味論が研究されている。ひとつの意味論は古典的なブール代数値意味論を写しとったものでブール代数の代わりにハイティング代数を用いる。別の意味論ではクリプキ・モデルを用いる。
直観主義論理は実際的な有用性を持つ。何故ならばこの制限によって存在具体性を持つ証明が作られるからであり、これは直観主義論理が数学的構成主義のある形態として適当なものとする。非正式には、ある対象が存在することの構成的証明があれば、その構成的証明はそのような対象の例を生成するアルゴリズムとして使える、ということを意味する。
形式化された直観主義論理はアレン・ハイティングによってヤン・ブラウワーの直観主義プログラムの形式的な基礎として発展せられたものである。目次
1 構文論と証明体系
1.1 シークエント計算
1.2 ヒルベルト流の計算
1.2.1 オプションの結合子
1.2.1.1 否定
1.2.1.2 同値
1.2.2 古典論理との関係
1.3 結合子の定義不可能性
2 意味論
2.1 ハイティング代数意味論
2.2 クリプキ意味論
2.3 タルスキ流のモデル論
2.4 他の論理との関係
2.4.1 多値論理との関係
2.4.2 中間論理との関係
2.4.3 様相論理との関係
2.5 ラムダ計算
3 関連項目
4 注釈
5 参考文献
6 外部リンク
構文論と証明体系 Rieger?Nishimura束のハッセ図。これのノードは変数をひとつだけ持つ命題論理式の直観主義的な同値性による同値類で、その順序は直観主義的な含意から誘導されるものである。
直観主義論理の論理式の構文は古典命題論理や古典述語論理と類似である。しかしながら、直観主義的な論理結合子は、古典論理におけるように、他の論理結合子を用いて定義することはできない。（そのため { → , ⊥ } {\displaystyle \{\to ,\bot \}} , { ∧ , ¬ } {\displaystyle \{\wedge ,\neg \}} , { ∨ , ¬ } {\displaystyle \{\vee ,\neg \}} などの論理結合子だけを用いて定式化することはできない。）直観主義命題論理では習慣的に → , ∧ , ∨ , ⊥ {\displaystyle \to ,\wedge ,\vee ,\bot } を基本的な結合子として採用する。ここで ¬ A {\displaystyle \neg A} は A → ⊥ {\displaystyle A\to \bot } の省略形として扱う。直観主義述語論理ではこれに量化記号 ∃ , ∀ {\displaystyle \exists ,\forall } を加える。
多くの古典論理の恒真式は直観主義的には証明できない。排中律 p ∨ ¬ p {\displaystyle p\vee \neg p} だけでなくパースの法則 ( ( p → q ) → p ) → p {\displaystyle ((p\to q)\to p)\to p} や二重否定除去 ¬ ¬ p → p {\displaystyle \neg \neg p\to p} などがその例である。古典論理において二重否定導入 p → ¬ ¬ p {\displaystyle p\to \neg \neg p} と二重否定除去 はともに定理である。直観主義論理においては前者のみが定理である。すなわち二重否定を導入することはできるが、除去することはできない。ただし三重否定除去 ¬ ¬ ¬ p → ¬ p {\displaystyle \neg \neg \neg p\to \neg p} は定理である。排中律 p ∨ ¬ p {\displaystyle p\vee \neg p} の拒絶は古典論理に親しい者には奇妙に思われるが、直観主義論理で命題論理式を証明するには、全ての可能な命題論理式に対して真または偽の証明が要求され、これは様々な理由によって不可能である。
多くの古典論理で妥当な恒真式は直観主義論理では定理でないが、全ての直観主義論理で妥当な定理は古典論理に於いても妥当であるから、直観主義論理は古典論理を弱めたものであるという見方ができる。ただし直観主義論理は古典論理にはない良い性質を多く持っている。
