数学问题

实际上，在具有 disjunction[1] property（析取性质）[2] 的证喵系统[3]中：

如果A∨B 是系统的定理[4]，那么 A 是系统的定理，或者 B 是系统的定理。

显然，经典逻辑 不具有 析取性质，我们知道(¬A)∨A 是可证的，但是 ¬A 和 A 不是。但是 直觉主义逻辑 具有析取性质。

只需要考察直觉主义逻辑的 sequent calculus 就可以发现，在析取规则这一栏，我们没有一条大一统的右规则，而是有两条右规则，RV1和 RV2：

A，Γ ⇒ C B，Γ ⇒ C

────────── L∨

A∨B，Γ ⇒ C

Γ ⇒ A

──────── R∨₁

Γ ⇒ A∨B

Γ ⇒ B

──────── R∨₂

Γ ⇒ A∨B

对比经典逻辑：

A，Γ ⇒ Δ B，Γ ⇒ Δ

────────── L∨

A∨B，Γ ⇒ Δ

Γ ⇒ Δ，A，B

────────── R∨

Γ ⇒ Δ，A∨B

L 规则几乎是完全一致的，但是你也看到了，经典逻辑允许Δ ，也即，一个命题集合出现在箭头（ ⇒ ，也有作者喜欢在这里用 ⊢ ）的右侧，而直觉主义逻辑只允许单个的公式出现。

在对排中律进行证喵搜索的时候，经典逻辑允许

⇒ A，¬A

──────

⇒ A∨¬A

，而直觉主义逻辑不允许这一步出现，因为 ⇒ 的右侧不允许出现公式集合，也即，逗号“ ’ ”。最终导致排中律在前者中有证喵，而在后者中无证喵。

但是，直觉主义逻辑获得了什么呢？析取性质。R∨₁ 和 R∨₂ 加起来说的就是析取性质。

你看，一个析取语句只有两种方式能得到，要不然通过R∨₁ 得到，要不然通过 R∨₂ 得到。

不过，直觉主义逻辑和经典逻辑之间其实只差一个double negation，也就是说：

ф是经典逻辑可证的，若且唯若[5] ¬¬ф 是直觉主义逻辑可证的。

从头捋一遍：

1. 你要的这种对称性是析取性质。

2. 可证是依赖于系统的概念，在某些人看来应该证明应该具有析取性质。

3. 经典逻辑不具有析取性质是因为经典逻辑的 sequent calculus 中允许右侧出现多个公式，更具体一点，是因为经典逻辑允许排中律存在。

4. 但是排中律在不在其实影响不大。

参考：

1. 有别于 disjuctive property，比如说像 grue、bleen 这样的概念。

2. _and_existence_properties

3. proof system

4. _calculus

5. 当且仅当

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