直観主義論理
直観主義論理の意味論は古典論理のそれよりも複雑である。直観主義論理のモデル論はハイティング代数やクリプキ意味論として与えられている。最近ではタルスキ流のモデル論の完全性がBob Constableによって証明せられた。ただしこの完全性は通常の意味のそれとは異なる。
∃ {\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と同様の条件を満たす
( φ → ψ ) ↔ ( ( φ ∨ ψ ) ↔ ψ ) {\displaystyle (\phi \to \psi )\leftrightarrow ((\phi \lor \psi )\leftrightarrow \psi )}
( φ → ψ ) ↔ ( ( φ ∧ ψ ) ↔ φ ) {\displaystyle (\phi \to \psi )\leftrightarrow ((\phi \land \psi )\leftrightarrow \phi )}
( φ ∧ ψ ) ↔ ( ( φ → ψ ) ↔ φ ) {\displaystyle (\phi \land \psi )\leftrightarrow ((\phi \to \psi )\leftrightarrow \phi )}
( φ ∧ ψ ) ↔ ( ( ( φ ∨ ψ ) ↔ ψ ) ↔ φ ) {\displaystyle (\phi \land \psi )\leftrightarrow (((\phi \lor \psi )\leftrightarrow \psi )\leftrightarrow \phi )}
とりわけ { ∨ , ↔ ⊥ } {\displaystyle \{\vee ,\leftrightarrow \bot \}} と { ∨ , ↔ ¬ } {\displaystyle \{\vee ,\leftrightarrow \neg \}} は直観主義的結合子の完全な基底となる。
古典論理の体系は次のどれかを公理に追加することによって得られる:
φ ∨ ¬ φ {\displaystyle \phi \lor \lnot \phi } (排中律。これは ( φ → χ ) → ( ( ¬ φ → χ ) → χ ) {\displaystyle (\phi \to \chi )\to ((\lnot \phi \to \chi )\to \chi )} とも定式化できる。)
¬ ¬ φ → φ {\displaystyle \lnot \lnot \phi \to \phi } (二重否定除去)
( ( φ → χ ) → φ ) → φ {\displaystyle ((\phi \to \chi )\to \phi )\to \phi } (パースの法則)
一般に、古典論理の恒真式で二元クリプキ・フレーム ∘ ⟶ ∘ {\displaystyle \circ {\longrightarrow }\circ } で妥当でない公理を追加したもの(言い換えればSmetanich論理に含まれないもの)を考えれば、これは古典論理に等しい。