直観主義論理
直観主義論理（ちょっかんしゅぎろんり、英: intuitionistic logic）または直観論理（ちょっかんろんり）、あるいは構成的論理（こうせいてきろんり、英: constructive logic）とは、ある種の論理体系であり、伝統的な真理値の概念が構成的証明の概念に置き換わっている点で古典論理とは異なる。例えば古典論理では、全ての論理式に真か偽の真理値 ( 直観主義論理の論理式の構文は古典命題論理や古典述語論理と類似である。しかしながら、直観主義的な論理結合子は、古典論理におけるように、他の論理結合子を用いて定義することはできない。（そのため 
直観論理
出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2018/01/28 04:15 UTC 版)
冠頭形への変換規則は古典論理であることに依存している。直観論理では、全ての論理式に等価な冠頭標準形があるわけではない。例えば否定が問題になるが、それだけではない。含意も直観論理と古典論理では扱いが異なる。直観論理では、含意を論理和と否定を使った形式に置き換えられない。 BHK解釈は、なぜ一部の論理式が直観論理で等価な冠頭標準形を持たないのかを示している。この解釈では、次の論理式 ( ∃ x ϕ ) → ∃ y ψ ( 1 ) {\displaystyle (\exists x\phi )\rightarrow \exists y\psi \qquad (1)} ∃ y ( ∃ x ϕ → ψ ) , ( 2 ) {\displaystyle \exists y(\exists x\phi \rightarrow \psi ),\qquad (2)} の証明は、y の特定の値を生成し、 ∃ x ϕ {\displaystyle \exists x\phi } の証明を ψ(y) の証明に変換する関数である。φ を満足する任意の x を使って ψ を満足する y を構築できるが、そのような x の知識なしに y を構築できないなら、論理式 (1) は論理式 (2) と等価ではないことになる。 冠頭標準形への変換規則のうち、直観論理では成り立たないものは以下の通りである。 (1) ∀ x ( ϕ ∨ ψ ) {\displaystyle \forall x(\phi \lor \psi )} なら ( ∀ x ϕ ) ∨ ψ {\displaystyle (\forall x\phi )\lor \psi } (2) ∀ x ( ϕ ∨ ψ ) {\displaystyle \forall x(\phi \lor \psi )} なら ϕ ∨ ( ∀ x ψ ) {\displaystyle \phi \lor (\forall x\psi )} (3) ( ∀ x ϕ ) → ψ {\displaystyle (\forall x\phi )\rightarrow \psi } なら ∃ x ( ϕ → ψ ) {\displaystyle \exists x(\phi \rightarrow \psi )} (4) ϕ → ( ∃ x ψ ) {\displaystyle \phi \rightarrow (\exists x\psi )} なら ∃ x ( ϕ → ψ ) {\displaystyle \exists x(\phi \rightarrow \psi )} (5) ¬ ∀ x ϕ {\displaystyle \lnot \forall x\phi } なら ∃ x ¬ ϕ {\displaystyle \exists x\lnot \phi } なお、(1)と(3)の ψ {\displaystyle \,\psi } では x が自由変項として出現しない。また、(2)と(4)の ϕ {\displaystyle \,\phi } では x が自由変項として出現しない。
※この「直観論理」の解説は、「冠頭標準形」の解説の一部です。
「直観論理」を含む「冠頭標準形」の記事については、「冠頭標準形」の概要を参照ください。
直観論理と同じ種類の言葉
- 直観論理のページへのリンク
