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

数学问题

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

相关小说

宿主我在每个时代风生水起 连载中
宿主我在每个时代风生水起
小小小小布丁
范小七是一只鲤鱼,她不想变青龙,想变漂亮的蛟龙,但是上级让她做任务,去帮那些缺了点气运的女主,于是她绑定了系统害第一个世界高考,什么玩意女主......
6.7万字9个月前
惊悚游戏,亦正亦邪双生子 连载中
惊悚游戏,亦正亦邪双生子
鸘s
0.4万字9个月前
喜灰之我摊牌了,不装了 连载中
喜灰之我摊牌了,不装了
阿念不吃糖
我从不剧透/已签约
5.2万字9个月前
百鬼图鉴录 连载中
百鬼图鉴录
宜禾
[百鬼夜行,生人回避]据说在某些特定的时间,地狱里的恶鬼会爬出来游荡人间。夜晚的阴风阵阵,惨白的月光照在地面上,树枝错综复杂的影子交叠在一起......
2.4万字9个月前
coc玩家并不想扮演角色卡 连载中
coc玩家并不想扮演角色卡
咸鱼塘
小白上路,轻喷有跑团成分无CP但团宠向,全文不掉马,很苏很尬,内含很多装X环节。男主聪明但作者不聪明,我尽力。每天只更一千左右,周六日会尽量......
7.9万字9个月前
穿越之师尊圣宠 连载中
穿越之师尊圣宠
忆轩孤梦
别人穿越过去不是王妃就是皇后,在差的也是什么状元夫人,富家商人之妻,想她林小冉居然穿成了个乞丐?天天要饭不说,还经常被人虐打成伤。天哪!还不......
31.0万字9个月前