直観主義論理

直観主義論理とは

直観主義論理（または構成的論理）は、古典論理とは異なる論理体系です。古典論理では、全ての命題は真か偽のいずれかの真理値を持ちますが、直観主義論理では、命題が真であるとは、その命題に対する直接的な証拠、つまり「証明」が存在することを意味します。

古典論理との違い

古典論理では、ある命題が真であるためには、その命題が偽でないことが示されれば十分です。しかし、直観主義論理では、単に偽でないというだけでは真とは見なされません。真であるためには、実際にその命題を証明する必要があります。このため、直観主義論理では、古典論理で成立する排中律（「命題は真であるか、またはその否定が真である」）や二重否定除去（「命題の否定の否定は、その命題と等しい」）が一般には成立しません。

証明論的視点

直観主義論理は、古典論理を制限した体系と見ることができます。古典論理では、排中律や二重否定除去が公理として認められていますが、直観主義論理では、これらの原理は特定のケースでのみ証明可能であり、一般的には成り立ちません。この制約により、直観主義論理は、証明が具体的な対象の存在を示すような、構成的な数学の基礎として適しています。

意味論

直観主義論理には、いくつかの意味論が存在します。一つは、古典的なブール代数を用いる代わりに、ハイティング代数を用いるものです。ハイティング代数では、論理結合子に対応する演算が、ブール代数とは異なる規則に従います。別の意味論として、クリプキ・モデルがあります。

直観主義論理の構文と証明体系

直観主義論理の論理式の構文は、古典論理とほぼ同じです。ただし、論理結合子（「かつ」、「または」、「ならば」など）の定義が異なります。直観主義論理では、論理結合子を他の結合子で定義することができません。

通常、直観主義命題論理では、含意（→）、論理積（∧）、論理和（∨）、および矛盾（⊥）を基本結合子として用います。否定（¬）は、¬A を A → ⊥ の省略形として扱います。直観主義述語論理では、これに存在量化記号（∃）と全称量化記号（∀）が加わります。

古典論理で成立しない定理

古典論理で真である多くの命題は、直観主義論理では証明できません。排中律（p∨¬p）やパースの法則（((p→q)→p)→p）、二重否定除去（¬¬p→p）はその例です。直観主義論理では、二重否定の導入（p→¬¬p）は定理ですが、除去は定理ではありません。

シークエント計算

ゲンツェンは、古典論理のシークエント計算LKを制限することで、直観主義論理の健全かつ完全な体系LJが得られることを発見しました。LJでは、シークエントの結論（右側）には高々一つの論理式のみが許されます。この制約により、古典論理では許容されるが、直観主義論理では許容されない推論が排除されます。

ヒルベルト流の計算

直観主義論理は、ヒルベルト流の計算によっても定義できます。これは、古典命題論理の公理化に似ています。推論規則としてモーダスポネンス（MP）を使用し、いくつかの公理図式を組み合わせることで証明を行います。

古典論理との関係

古典論理は、直観主義論理に排中律や二重否定除去などの公理を追加することで得られます。直観主義論理は古典論理を弱めたものと見ることができますが、古典論理にはない優れた性質も持っています。例えば、ゲーデル＝ゲンツェン変換によって、古典一階述語論理を直観主義一階述語論理に埋め込むことができます。

論理結合子の定義不可能性

古典論理では、論理積、論理和、含意は否定を用いて定義できますが、直観主義論理ではそうではありません。これは、直観主義論理では二値原理が成り立たないためです。このため、直観主義論理では、古典論理で成立する同値性が、一般には成り立ちません。

例えば、論理和（aまたはb）は「もしaでないならばb」よりも強い主張であり、古典論理で同値となるものが、直観主義論理では一方の含意のみが成立するといった例があります。

直観主義論理の意味論

直観主義論理の意味論は、古典論理よりも複雑です。主なものとして、ハイティング代数意味論とクリプキ意味論があります。

ハイティング代数意味論

古典論理では、真理値はブール代数から取られますが、直観主義論理では、真理値はハイティング代数から取られます。ハイティング代数はブール代数の一般化であり、論理結合子に対応する演算がより柔軟に定義されます。

クリプキ意味論

クリプキ意味論では、論理式の真理値は、可能な世界の集合とその間の到達関係によって解釈されます。この意味論は、様相論理にも関連しています。

その他の関連事項

直観主義論理は、双対直観論理、最小論理、多値論理、中間論理、様相論理、ラムダ計算など、他の論理や計算体系とも関連しています。

直観主義論理と型理論

直観主義論理は、型理論、特に直観主義的型理論の基礎としても利用されています。これは、証明と計算の間の対応関係（カリー＝ハワード対応）に基づいています。

実践的な応用

直観主義論理は、単なる理論的な論理体系に留まらず、プログラム検証、アルゴリズム設計など、計算機科学の分野で広く応用されています。例えば、直観主義論理における証明は、プログラムの仕様であり、証明の構成はプログラムそのものに対応付けられるため、正しいプログラムの開発を支援する上で重要な役割を果たします。

直観主義論理は、数学的厳密さと構成的な証明能力を両立させるための強力なツールとして、今後ますます重要性を増していくと考えられます。

もう一度検索