Re: [請益] 反證法

[MathTurtle (恩典)]

※ 引述《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
→ Favonia:我喜歡的符號跟你用的好像完全不一樣 xD 然後我覺以為直覺
→ Favonia:直覺邏輯大都有爆炸原理也有 RAA2 和 RAA4 ?
→ Favonia:（經過適當翻譯後）
→ MathTurtle:you are exactly right! 所以我那句話是錯的!
→ MathTurtle:直覺主義是沒有排中律和RAA1與RAA3, 但是有explosion
→ MathTurtle:然後有一個minimal logic是三個都沒有的...
→ MathTurtle:所以這樣就清楚了。直覺主義是針對排中律來的, 以及可
→ MathTurtle:以導出排中律的RAA1也被拒絕。而 relevant logic是針對
→ MathTurtle:explosion來的, 以及會導致explosion的 RAA1 也要拒絕
→ MathTurtle:而 paraconsistent logic是容許truth-value glut,
→ MathTurtle:所以排中律(沒有 gap)可成立但explosion和RAA1也不成立
→ MathTurtle:所以這三個之間的關係大概是這樣吧
→ Favonia:hmm 我對於相關邏輯（relevant logic）沒有研究就是了 xD
→ Favonia:雖然我對 paraconsistent logic 也超不熟不過我找到一個
→ Favonia:有趣的資料也許你會有興趣：http://plato.stanford.edu
→ Favonia:/entries/logic-paraconsistent/#ManyValLog
→ Favonia:你的 ? 跟網站中的 b (both) 好像一樣 xD (1966 的論文？)
→ MathTurtle:對...一樣的, 因為我的table就是從Priest的書上拿來的
→ MathTurtle:而那篇我看了一下好像也是 Priest 寫的
→ Favonia:哈哈不過真正來源應該是 1966 年 Asenjo 的 PhD 畢業論文