直觉主义逻辑（一） (6-4)

10. (¬¬p → p) → p∨¬p

自然演绎（natural deduction）

直觉主义逻辑的一个证明系统是自然演绎系统NJ(→，⊥，∧，∨) 。其中J代表直觉主义逻辑。NK是经典逻辑的自然演绎系统。

定义2

1. 自然演绎里的判断（judgement）是一个对子，写作 Γ ⊢ ф ，读作“Gamma证明phi”，包括一个有限逻辑式集合 Γ 和一个逻辑式 ф .

2. {ф₁，ф₂} ⊢ ψ 简写为 ф₁，ф₂ ⊢ ψ； Γ ∪ Δ 简写为 Γ，Δ； Γ∪{ф} 简写为 Γ，ф ； ∅ ⊢ ф 简写为 ⊢ ф .

3. Γ ⊢ ф 的形式证明（proof）或推导（derivation）是一个满足下列条件的有限判断树：

• 根标记为 Γ ⊢ ф ；

所有的叶子都是公理（公设，axioms），即形如 Γ，ф ⊢ ф 的判断；

• 其他节点的符号都可以从子节点借助下述法则得到：

(Ax)Γ，ф ⊢ ф

Γ，ф ⊢ ψ

(→ l) ────

Γ ⊢ ф → ψ

Γ，ф ⊢ ф → ψ Γ ⊢ ф

(→ E) ───────────

Γ ⊢ ψ

Γ ⊢ ф Γ ⊢ ψ

(∧ l) ───────

Γ ⊢ ф∧ψ

Γ ⊢ ф∧ψ Γ ⊢ ф∧ψ

(∧ E) ─────；─────

Γ ⊢ ф Γ ⊢ ψ

Γ ⊢ ф Γ ⊢ ψ

(∨ l) ─────；─────

Γ ⊢ ф∨ψ Γ ⊢ ф∨ψ

Γ，ф ⊢ θ Γ，ψ ⊢ θ Γ ⊢ ф∨ψ

(∨ E) ────────────────

Γ ⊢ θ

Γ ⊢ ⊥

(⊥ E) ────

Γ ⊢ ф

4. 如果⊢ ф ，那么我们称 ф 是一个定理（theorem）。

弱化（Weakening）和替换（Substitution）

Γ ⊢ ф Γ ⊢ ф

─────；───────────

Γ，ψ ⊢ ф Γ[p：＝ψ] ⊢ ф[p：＝ψ]

经典逻辑的代数语义学‬

定义3（格，lattice）

数学联邦政治世界观提示您：看后求收藏（同人小说网http://tongren.me），接着再看更方便。