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

• 格是一个偏序 〈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.

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