直観主義論理
(直観論理 から転送)
出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2024/02/11 02:30 UTC 版)
直観主義論理（ちょっかんしゅぎろんり、英: intuitionistic logic）または直観論理（ちょっかんろんり）、あるいは構成的論理（こうせいてきろんり、英: constructive logic）とは、ある種の論理体系であり、伝統的な真理値の概念が構成的証明の概念に置き換わっている点で古典論理とは異なる。例えば古典論理では、全ての論理式に真か偽の真理値 ( ) が割り当てられる。このときその真理値に対する直接的なエビデンスを持つか否かは問題にしない。これはどのような曖昧な命題においても「真か偽かが決定可能である」ということを意味する。対照的に、直観主義論理では確定的に論理式に真理値を割り当てるのではなく、それが真であるとは「直接的なエビデンス」つまり「証明」があることと見做す。
注釈
- ^ ここでの双対はシークエント計算においての双対である。
出典
- ^ Proof Theory by G. Takeuti, ISBN 0-444-10492-5
- ^ a b Sørensen, Morten Heine B; Paweł Urzyczyn (2006). Lectures on the Curry-Howard Isomorphism. Studies in Logic and the Foundations of Mathematics. Elsevier. p. 42. ISBN 0-444-52077-5
- ^ Urbas, Igor (1996-07-01). “Dual-Intuitionistic Logic”. Notre Dame Journal of Formal Logic 37 (3). doi:10.1305/ndjfl/1039886520. ISSN 0029-4527.
- ^ Aoyama, Hiroshi (2004). “LK, LJ, Dual Intuitionistic Logic, and Quantum Logic”. Notre Dame Journal of Formal Logic 45 (4): 193–213. doi:10.1305/ndjfl/1099238445.
- ^ Lévy, Michel (2011年4月29日). “Logique modale propositionnelle S4 et logique intuitioniste propositionnelle” (PDF). pp. 4–5. 2015年5月8日閲覧。
- ^ a b Natasha Alechina, Michael Mendler, Valeria de Paiva, and Eike Ritter. “Categorical and Kripke Semantics for Constructive S4 Modal Logic” (PDF). 2015年5月8日閲覧。
- 1 直観主義論理とは
- 2 直観主義論理の概要
- 3 関連項目
直観論理
出典: フリー百科事典『ウィキペディア（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 が自由変項として出現しない。
※この「直観論理」の解説は、「冠頭標準形」の解説の一部です。
「直観論理」を含む「冠頭標準形」の記事については、「冠頭標準形」の概要を参照ください。
直観論理と同じ種類の言葉
- 直観論理のページへのリンク
