# 直觉主义逻辑

## 语法

Rieger-Nishimura 格。它的節點是不別直覺邏輯等價之異的一元命題公式，按直覺邏輯蘊含排序。

### 希尔伯特式演算

• THEN-1: φ → (χ → φ)
• THEN-2: (φ → (χ → ψ)) → ((φ → χ) → (φ → ψ))
• AND-1: φ ∧ χ → φ
• AND-2: φ ∧ χ → χ
• AND-3: φ → (χ → (φ ∧ χ))
• OR-1: φ → φ ∨ χ
• OR-2: χ → φ ∨ χ
• OR-3: (φ → ψ) → ((χ → ψ) → (φ ∨ χ → ψ))
• NOT-1: (φ → χ) → ((φ → ¬χ) → ¬ φ)
• NOT-2: φ → (¬φ → χ)

• PRED-1: (∀x Z(x)) → Z(t)
• PRED-2: Z(t) → (∃x Z(x))
• PRED-3: (∀x (WZ(x))) → (W → ∀x Z(x))
• PRED-4: (∀x (Z(x) → W)) → (∃x Z(x) → W)

### 算子的不可互定义性

• ${\displaystyle (\phi \wedge \psi )\to \neg (\neg \phi \vee \neg \psi )}$
• ${\displaystyle (\phi \vee \psi )\to \neg (\neg \phi \wedge \neg \psi )}$
• ${\displaystyle (\neg \phi \vee \neg \psi )\to \neg (\phi \wedge \psi )}$
• ${\displaystyle (\neg \phi \wedge \neg \psi )\leftrightarrow \neg (\phi \vee \psi )}$

• ${\displaystyle (\phi \wedge \psi )\to \neg (\phi \to \neg \psi )}$
• ${\displaystyle (\phi \to \psi )\to \neg (\phi \wedge \neg \psi )}$
• ${\displaystyle (\phi \wedge \neg \psi )\to \neg (\phi \to \psi )}$
• ${\displaystyle (\phi \to \neg \psi )\leftrightarrow \neg (\phi \wedge \psi )}$

• ${\displaystyle (\phi \vee \psi )\to (\neg \phi \to \psi )}$
• ${\displaystyle (\neg \phi \vee \psi )\to (\phi \to \psi )}$
• ${\displaystyle \neg (\phi \to \psi )\to \neg (\neg \phi \vee \psi )}$
• ${\displaystyle \neg (\phi \vee \psi )\leftrightarrow \neg (\neg \phi \to \psi )}$

• ${\displaystyle (\forall x\ \phi (x))\to \neg (\exists x\ \neg \phi (x))}$
• ${\displaystyle (\exists x\ \phi (x))\to \neg (\forall x\ \neg \phi (x))}$
• ${\displaystyle (\exists x\ \neg \phi (x))\to \neg (\forall x\ \phi (x))}$
• ${\displaystyle (\forall x\ \neg \phi (x))\leftrightarrow \neg (\exists x\ \phi (x))}$

• ${\displaystyle ((p\lor q)\land \neg r)\lor (\neg p\land (q\leftrightarrow r)),}$
• ${\displaystyle p\to (q\land \neg r\land (s\lor t)).}$