作者MathTurtle (恩典)
看板logic
标题Re: [请益] 反证法
时间Mon Dec 26 03:53:26 2011
※ 引述《Favonia (小西风最乖了*^^*)》之铭言：
: : *反过来说*, ~P 是前提. 这「反过来说」的跳跃应该不大.
: 这个「反过来说」之所以成立，我觉得跟排中原理比较有关。
: （逻辑系统牵一发而动全身，感觉很难定义什麽叫做跟某某原理有
: 关... orz）正如 intontu 所说，古典逻辑如果用一般的自然演绎
: 系统写出来，反证法的基础之一是排中原理。爆炸原理不一定每个
: 逻辑系统都成立一样，同样的，排中原理也不是每个系统都成立。
这里让我想了很久。
究竟反证法与排中律以及explosion之间的关联是什麽?
我觉得这是一个很难的问题,
因为比较常见的像是直觉逻辑或许多的relevant logic系统是三者都不成立,
而其它非古典逻辑是三者都成立, 所以很难想像它们的差别在哪。
paraconsistent logic 是针对 explosion 而来 (即 P & ~P |- Q)
而通常因为拒绝了 explosion, 就很自然要拒绝 RAA
因为从 RAA 很容易可以导出 explosion (只须加上 weakening rule A |- B ->A)
[假设 RAA (比较强的那种, 即 ~P -> (Q&~Q) |- P), 假设我们现在有矛盾 Q&~Q
由 weakening 我们得 ~P -> (Q&~Q), 因此有 P, 得证 ]
但排中律呢?
所以我在想, 有没有可能有一个逻辑系统是包含排中律,
但却没有 explosion 或是 RAA 的?
explosion这部份比较容易想, 因为 Priest 的 paraconsistent logic
好像就可以是这样的一个系统。而 RAA 则是要看你是哪一个版本的,
大致上我们可以区分四种强弱不等的 RAA:
RAA1 ~P -> (Q&~Q) |- P
RAA2 P -> (Q&~Q) |- ~P
RAA3 ~P -> P |- P
RAA4 P -> ~P |- ~P
我稍微做了一下, 找到这个系统是 Excluded middle成立,
但是 explosion 和 RAA1, RAA2 都不成立的。
比较简单的讲可以用以下的三值逻辑给出语义:
~| &|1 ? 0 or|1 ? 0 ->|1 ? 0
----- --------- ---------- -----------
1|0 1|1 ? 0 1|1 1 1 1|1 ? 0
?|? ?|? ? 0 ?|1 ? ? ?|1 ? ?
0|1 0|0 0 0 0|1 ? 0 0|1 1 1
然後 designated value 是 {1, ?}
Excluded middle 会成立是因为 P or not P 会是 1或是?, 因此成立。
explosion不成立是因为当 Q 是 ? 而 P 是 0 时, (Q&~Q)|=P 会是 ?|=0 故不成立
RAA1和RAA2也是同样地, 在 Q=? P=0 时会是 ?|=0 而不成立。
不过缺点是在这系统中, RAA3和RAA4仍然会成立就是了。
--
※ 发信站: 批踢踢实业坊(ptt.cc)
◆ From: 86.27.186.91
1F：→ Favonia:我喜欢的符号跟你用的好像完全不一样 xD 然後我觉以为直觉 12/28 15:09
2F：→ Favonia:直觉逻辑大都有爆炸原理也有 RAA2 和 RAA4 ? 12/28 15:12
3F：→ Favonia:（经过适当翻译後） 12/28 15:12
4F：→ MathTurtle:you are exactly right! 所以我那句话是错的! 12/28 21:13
5F：→ MathTurtle:直觉主义是没有排中律和RAA1与RAA3, 但是有explosion 12/28 21:15
6F：→ MathTurtle:然後有一个minimal logic是三个都没有的... 12/28 21:15
7F：→ MathTurtle:所以这样就清楚了。直觉主义是针对排中律来的, 以及可 12/28 21:16
8F：→ MathTurtle:以导出排中律的RAA1也被拒绝。而 relevant logic是针对 12/28 21:17
9F：→ MathTurtle:explosion来的, 以及会导致explosion的 RAA1 也要拒绝 12/28 21:18
10F：→ MathTurtle:而 paraconsistent logic是容许truth-value glut, 12/28 21:20
11F：→ MathTurtle:所以排中律(没有 gap)可成立但explosion和RAA1也不成立 12/28 21:21
12F：→ MathTurtle:所以这三个之间的关系大概是这样吧 12/28 21:22
13F：→ Favonia:hmm 我对於相关逻辑（relevant logic）没有研究就是了 xD 12/29 01:40
14F：→ Favonia:虽然我对 paraconsistent logic 也超不熟不过我找到一个 12/30 14:19
16F：→ Favonia:/entries/logic-paraconsistent/#ManyValLog 12/30 14:19
17F：→ Favonia:你的 ? 跟网站中的 b (both) 好像一样 xD (1966 的论文？) 12/30 14:21
18F：→ MathTurtle:对...一样的, 因为我的table就是从Priest的书上拿来的 12/30 17:32
19F：→ MathTurtle:而那篇我看了一下好像也是 Priest 写的 12/30 17:33
20F：→ Favonia:哈哈不过真正来源应该是 1966 年 Asenjo 的 PhD 毕业论文 12/31 00:15