構文論と証明体系
出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2022/08/10 14:35 UTC 版)
直観主義論理の論理式の構文は古典命題論理や古典述語論理と類似である。しかしながら、直観主義的な論理結合子は、古典論理におけるように、他の論理結合子を用いて定義することはできない。（そのため { → , ⊥ } {\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} の拒絶は古典論理に親しい者には奇妙に思われるが、直観主義論理で命題論理式を証明するには、全ての可能な命題論理式に対して真または偽の証明が要求され、これは様々な理由によって不可能である。 多くの古典論理で妥当な恒真式は直観主義論理では定理でないが、全ての直観主義論理で妥当な定理は古典論理に於いても妥当であるから、直観主義論理は古典論理を弱めたものであるという見方ができる。ただし直観主義論理は古典論理にはない良い性質を多く持っている。
※この「構文論と証明体系」の解説は、「直観主義論理」の解説の一部です。
「構文論と証明体系」を含む「直観主義論理」の記事については、「直観主義論理」の概要を参照ください。
- 構文論と証明体系のページへのリンク
