作者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