# 直觉主义逻辑

## 语法

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)

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

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

• $(\phi \wedge \psi) \to \neg (\phi \to \neg \psi)$
• $(\phi \to \psi) \to \neg (\phi \wedge \neg \psi)$
• $(\phi \wedge \neg \psi) \to \neg (\phi \to \psi)$
• $(\phi \to \neg \psi) \leftrightarrow \neg (\phi \wedge \psi)$

• $(\phi \vee \psi) \to (\neg \phi \to \psi)$
• $(\neg \phi \vee \psi) \to (\phi \to \psi)$
• $\neg (\phi \to \psi) \to \neg (\neg \phi \vee \psi)$
• $\neg (\phi \vee \psi) \leftrightarrow \neg (\neg \phi \to \psi)$

• $(\forall x \ \phi(x)) \to \neg (\exist x \ \neg \phi(x))$
• $(\exist x \ \phi(x)) \to \neg (\forall x \ \neg \phi(x))$
• $(\exist x \ \neg \phi(x)) \to \neg (\forall x \ \phi(x))$
• $(\forall x \ \neg \phi(x)) \leftrightarrow \neg (\exist x \ \phi(x))$

Alexander Kuznetsov 的證明，任一下述定義的連結詞可以充當直覺邏輯的自足算子:[1]

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

## 语义

### 海廷代数语义

Value(¬(A ∧ ¬A)) =
(Value(A ∧ ¬A))C° =
(Value(A) ∩ Value(¬A))C° =
(X ∩ (Value(A))C°)C° =
(XXC°)C°

øC° =(R2)° = R2

## 注释

1. ^ Alexander Chagrov, Michael Zakharyaschev, Modal Logic, vol. 35 of Oxford Logic Guides, Oxford University Press, 1997, pp. 58–59.
2. ^ Intuitionistic Logic. Written by Joan Moschovakis. Published in Stanford Encyclopedia of Philosophy.

## 引用

• Van Dalen, Dirk, 2001, "Intuitionistic Logic," in Goble, Lou, ed., The Blackwell Guide to Philosophical Logic. Blackwell.
• Morten H. Sørensen, Pawel Urzyczyn, 2006, Lectures on the Curry-Howard Isomorphism (chapter 2: "Intuitionistic Logic"). Studies in Logic and the Foundations of Mathematics vol. 149, Elsevier.