直觉主义逻辑（一）

何为逻辑？斯坦福哲学百科全书的 Logic and Ontology 条目给出了逻辑的四种常见的概念：

• 对于人工形式语言的研究

• 对于形式有效的推理和逻辑结果的研究

• 对于逻辑真的研究

• 对于判断的普遍特征或形式的研究

这四种概念在特定的研究场景下表现出极强的一致性，在另一些场景下则表现出明显的不同。

最为著名的“经典逻辑（classical logic）”是学习逻辑的一个起点，以及其他逻辑作为参照的标杆。经典逻辑侧重“真值”，陈述的“真值”是其“绝对”特征。一个无歧义的合式陈述（well-formed statement）或真或假。假即非真，真即非假，是为“排中律”（Law/principle of excluded middle,tertium non datur）。

基于经典逻辑，我们可以“非构造地”证明一个命题。例如：

∃x，y ∈ ℝ – ℚ s.t xʸ ∈ ℚ（存在两个无理数 x，y ，使得 xʸ 为有理数）。

证明：如果√2√2 是有理数，那么我们可以取 x＝y＝√2 ，否则可以取 x＝√2√2，y＝√2 .

上面的证明虽然在经典逻辑里没有问题，但我们仍无法确定究竟哪一种情况是正确的。除此之外，我们还可以做出一个构造性证明（constructive proof）：对于x＝√2，y＝2log₂3 ，我们有 xʸ＝3∈ℚ .

这种“构造式”的推理方式对应着“直觉主义逻辑”（intuitionistic logic）。直觉主义逻辑的哲学基础是，不存在绝对真理，只存在理想化数学家（创造主体）的知识和直觉主义构建。逻辑判断为真当且仅当创造主体可以核实它。所以，直觉主义逻辑不接受排中律。

BHK释义（The BHK interpretation）

直觉主义命题逻辑，或称直觉主义命题演算（Intuitionistic propositional calculus, IPC），的语言和经典命题逻辑的语言是一样的。

定义1

假设一个命题变量（propositional variables，或译为变项，为了保持逻辑、数学用语的一致性，类型论驿站中一般采用数学翻译法）无限集合PV，我们定义逻辑式（formulas）的集合 Φ 为满足下列条件的最小集合：

• 所有谓词变量和常量 ⊥ （谬）都是 Φ 的元素；

• 如果 ф，ψ∈Φ ，那么 (ф → ψ)，(ф∨ψ)，(ф∧ψ)∈Φ.

变量和常量被称为原子式（atomic formulas）。子式（subformula）是一个逻辑式（不一定平凡）的构成逻辑式。

否定、等价和真（truth）定义如下：

• ¬ф ≡ df ф → ⊥；

• ф ↔ ψ≡df (ф → ψ) ∧ (ψ → ф)；

• ⊤ ≡ df⊥→⊥.

直觉主义逻辑里的语义不是通过真值表来判断的，而是通过构建模式来解释的。这就是著名的BHK释义（Brouwer-Heyting-Kolmogorov interpretation）。Heyting 是 Brouwer的学生。Kolmogorov有个著名的学生叫Martin-Löf.

• ф₁∧ф₂ 的构造（或证明）包含 ф₁ 的构造和 ф₂ 的构造；

• ф₁∨ф₂ 的构造包含一个指数（indicator） i∈{1，2} 和一个 фᵢ 的构造；

• ф₁ → ф₂的构造是一个把每一个 ф₁ 的构造都转换为 ф₂ 的构造的函数（方法）；

• 不存在 ⊥ 的构造。

练习1：

证明下列命题：

Theorem bot_to_p: False -＞P.

Theorem neglect_Q: P-＞Q-＞P.

Theorem pqr: (P-＞Q-＞R)-＞(P-＞Q)-＞P-＞R.

Theorem doub_neg: P-＞~~P.

Theorem doub_neg_elim: ~~~P-＞~P.

Theorem contra_imp:(P-＞Q)-＞(~Q-＞~P).

Theorem vee_distr: ~(P\/Q) ＜-＞ (~P/\~Q).

Theorem sum_arrow:((P/\Q)-＞R)＜-＞(P-＞(Q-＞R)).

Theorem ex_mid_doub_neg: ~~(P\/~P).

Theorem ex_mid_impl: (P\/~P)-＞~~P-＞P.

参考答案（使用 Coq）：

Section BHK_interpretable.

Hypotheses P Q R:Prop.

Theorem bot_to_p: False -＞P.

Proof.

intros.

elim H.

Qed.

Theorem neglect_Q: P-＞Q-＞P.

Proof.

auto.

Qed.

Theorem pqr: (P-＞Q-＞R)-＞(P-＞Q)-＞P-＞R.

Proof.

auto.

Qed.

Theorem doub_neg: P-＞~~P.

Proof.

auto.

Qed.

Theorem doub_neg_elim: ~~~P-＞~P.

Proof.

auto.

Qed.

Theorem contra_imp:(P-＞Q)-＞(~Q-＞~P).

Proof.

auto.

Qed.

Theorem vee_distr: ~(P\/Q) ＜-＞ (~P/\~Q).

Proof.

unfold iff.

unfold not.

split.

intros. (*left implies right*)

refine (conj _ _);auto.

intros (*right implies left*).

elim H0;apply H.

Qed.

Theorem sum_arrow:((P/\Q)-＞R)＜-＞(P-＞(Q-＞R)).

Proof.

unfold iff.

split.

intros.

apply H.

split; [apply H0 | apply H1].

intros;apply H; apply H0.

Qed.

Theorem ex_mid_doub_neg: ~~(P\/~P).

Proof.

unfold not.

auto.

Qed.

Theorem ex_mid_impl: (P\/~P)-＞~~P-＞P.

Proof.

unfold not.

intros.

elim H.

trivial.

intros.

destruct H.

assumption.

elim H0.

exact H.

Qed.

Print bot_to_p. (*查看构造*)

Print ex_mid_impl.

End BHK_interpretable.

下列逻辑式在经典逻辑里是重言式（tautology），但在直觉主义逻辑里却没有构造。

1. ((p → q) → p) → p（Peirce 定律）

2. p∨¬p（排中律）

3. ¬¬p → p（双重否定消除）

4. (¬q → ¬p) → (p → q)（反证法）

5. ¬(p∧q) ↔ (¬p∨¬q)（De Morgan定律）

6. (p → q) → (¬p → q) → q

7. ((p ↔ q) ↔ r) ↔ (p ↔ (q ↔ r))

8. (p → q) ↔ (¬p∨q)（经典逻辑中蕴含的定义）

9. (p∨q → p)∨(p∨q → q)

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）

• 格是一个偏序 〈A，≤〉，其中 A 的每一个双元素子集 {α，b} 都有一个最小上限（least upper bound）和一个最大下限（greatest lower bound）。

• sup{α，b} 记为 α ⊔ b ；

ᴀ

inf{α，b} 记为 α ⊓ b .

ᴀ

• 一个格中的顶端元素通常记为 1，底端元素通常记为 0 .

定义4（分配格，补）

• 格 A 是分配的（distributive），当且仅当：

(α ⊔ b) ⊓ c＝(α ⊓ c) ⊔ (b ⊓ c)；

(α ⊓ b) ⊔ c＝(α ⊔ c) ⊓ (b ⊔ c)

• 设格 A 顶端元素为 1 ，底端元素为 0 ，那么我们称 b 是 α 的补，当且仅当 α ⊔ b＝1 且 α ⊓ b＝0.

定义5（布尔代数）

• 布尔代数（Boolean algebra）是有顶端和底端元素的分配格 B，B 中的每一个元素 α 都有一个补（记为 –α ）。

布尔代数通常记为 B＝〈B，⊔，⊓，–0，1〉 ，其中 α ≤ b ⇔ α ⊓ b＝α .

定义6（赋值）

布尔代数B＝〈B，⊔，⊓，–0，1〉 的一个赋值（valuation）是任意一个从集合 PV 到 B 的映射。逻辑式 ф 在 B 中的值（value）归纳地定义如下：

[[p]]υ＝υ(p)，for p∈PV；

[[⊥]]υ＝0；

[[ф∨ψ]]υ＝[[ф]]υ ⊔ [[ψ]]υ；

[[ф∧ψ]]υ＝[[ф]]υ ⊓ [[ψ]]υ；

[[ф → ψ]]υ＝–[[ф]]υ ⊔ [[ψ]] – υ.

当[[ф]]υ＝1 时，我们记作 B，υ╞ ф ；当对于所有 υ ， B，υ╞ ф 时，我们记作 B ⊢ ф .

定理7

命题逻辑式ф 是经典逻辑重言式（classical tautology）当且仅当对于所有布尔代数 B ， B╞ ф.

海廷代数（Heyting algebra）

布尔代数是经典逻辑的一种语义诠释，而海廷代数则是直觉主义逻辑的代数语义学。在直觉主义逻辑里，我们关注的首要问题是“可证明性”（provability），而非“真值”。

可证明的蕴含关系具备自反性和传递性：

Section Heyting_algebra.

Hypotheses phi psi theta: Prop.

Theorem reflexivity: phi -＞ phi.

Proof.

trivial.

Qed.

Theorem transitivity: ((phi -＞ psi) /\ (psi -＞ theta))-＞ psi -＞ theta.

Proof.

intros H psi'.

elim H.

intros.

auto.

Qed.

下面我们看等价关系。首先我们定义ф∼Γψ ⇔ Γ ⊢ ф → ψ 省略下标，我们有 [⊥]∼＝{ф│Γ ⊢ ¬ф} ， [⊤]∼＝{ф│Γ ⊢ ф } . 设 ԸΓ＝Φ/∼＝{[ф]│ф∈Φ} ，那么 [ф]∼ ≤Γ [ψ]∼ ⇔ Γ ⊢ ф → ψ.等价关系定义为 [ф]∼＝Γ[ψ]∼ ⇔ [ф]∼ ≤ [ψ]∼ [ψ]∼ ≤ [ф]∼. 然后我们会发现 〈ԸΓ，≤〉 是一个格。

数学联邦政治世界观提示您：看后求收藏（笔尖小说网http://www.bjxsw.cc），接着再看更方便。