ヒルベルト流の計算
出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2022/03/25 04:07 UTC 版)
直観主義論理は次のようにヒルベルト流の計算を用いても定義できる。これは古典命題論理の公理化（Propositional calculus#Alternative calculus）に類似である。 命題論理では、推論規則としてモーダスポネンス MP: ϕ {\displaystyle \phi } および ϕ → ψ {\displaystyle \phi \to \psi } から ψ {\displaystyle \psi } を導く を取り、公理図式として次のものを取る： THEN-1: ϕ → ( χ → ϕ ) {\displaystyle \phi \to (\chi \to \phi )} THEN-2: ( ϕ → ( χ → ψ ) ) → ( ( ϕ → χ ) → ( ϕ → ψ ) ) {\displaystyle (\phi \to (\chi \to \psi ))\to ((\phi \to \chi )\to (\phi \to \psi ))} AND-1: ϕ ∧ χ → ϕ {\displaystyle \phi \land \chi \to \phi } AND-2: ϕ ∧ χ → χ {\displaystyle \phi \land \chi \to \chi } AND-3: ϕ → ( χ → ( ϕ ∧ χ ) ) {\displaystyle \phi \to (\chi \to (\phi \land \chi ))} OR-1: ϕ → ϕ ∨ χ {\displaystyle \phi \to \phi \lor \chi } OR-2: χ → ϕ ∨ χ {\displaystyle \chi \to \phi \lor \chi } OR-3: ( ϕ → ψ ) → ( ( χ → ψ ) → ( ϕ ∨ χ → ψ ) ) {\displaystyle (\phi \to \psi )\to ((\chi \to \psi )\to (\phi \lor \chi \to \psi ))} FALSE: ⊥ → ϕ {\displaystyle \bot \to \phi } 一階述語論理の体系を作るには次の推論規則を加える： ∀ {\displaystyle \forall } -GEN: ψ → ϕ {\displaystyle \psi \to \phi } から ψ → ( ∀ x ϕ ) {\displaystyle \psi \to (\forall x\ \phi )} を導く；ただし固有変数条件「 x {\displaystyle x} は ψ {\displaystyle \psi } に自由に現れない」を満たす ∃ {\displaystyle \exists } -GEN: ϕ → ψ {\displaystyle \phi \to \psi } から ( ∃ x ϕ ) → ψ {\displaystyle (\exists x\ \phi )\to \psi } を導く；ただし固有変数条件「 x {\displaystyle x} は ψ {\displaystyle \psi } に自由に現れない」を満たす また次のものを公理図式に加える： PRED-1: ( ∀ x ϕ ( x ) ) → ϕ ( t ) {\displaystyle (\forall x\ \phi (x))\to \phi (t)} ただし項 t は ϕ {\displaystyle \phi } の中の x への代入について自由である (つまり t の中の変数記号は ϕ ( t ) {\displaystyle \phi (t)} の中で束縛されていない) PRED-2: ϕ ( t ) → ( ∃ x ϕ ( x ) ) {\displaystyle \phi (t)\to (\exists x\ \phi (x))} ただしPRED-1と同様の条件を満たす
※この「ヒルベルト流の計算」の解説は、「直観主義論理」の解説の一部です。
「ヒルベルト流の計算」を含む「直観主義論理」の記事については、「直観主義論理」の概要を参照ください。
- ヒルベルト流の計算のページへのリンク
