数学联邦政治世界观
超小超大

数学问题

实际上,在具有 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),接着再看更方便。

相关小说

学生们的成长手册 连载中
学生们的成长手册
仙女丝
(已弃坑)
10.4万字9个月前
章鱼本本(午版) 连载中
章鱼本本(午版)
林林林七七
泥嚎!这里是午版章鱼本本!
0.1万字9个月前
你也穿越了?! 连载中
你也穿越了?!
流火丶
一朝重生,他从高高在上的仙界上仙变成了一个不起眼家族的嫡子死后穿越,他从现代一个跑龙套的变成了修仙小说中的标配男主白雪峰:这二货哥哥怎么老想......
12.4万字9个月前
悠闲末世小店 连载中
悠闲末世小店
七两啊啊
看习惯打打杀杀的了来看看末世的日常,作者无能没有太多的打戏,有的只是日常。女主的全能的,男主是在外大灰狼在内小白兔。1对1决对甜。以后还请多......
2.9万字9个月前
神兵小将之危机再来 连载中
神兵小将之危机再来
慕久惜
神兵小将们来到玉明,在经历五个国的困难之后,终于取得胜利。众人之间的情与恨,探索之中明白……
3.4万字9个月前
水默恋叶罗丽 连载中
水默恋叶罗丽
你,不简单
天呐!王默居然是叶罗丽灵犀阁阁主的女儿灵沫。
0.8万字9个月前