作者carelai (風云人物)
看板logic
標題[討論] 關于構造邏輯
時間Wed Feb 4 13:08:31 2015
在構造邏輯（非經典邏輯）中，排中律是不可用的，即未必P和not(P)有一個必為真。
由此，可以知not(not(P))無法推出P（即傳統的反證法不成立）。但是，
not(not(not(P)))卻可以推出not(P)。還有，如果P能推出R，not(P)也能推出R，
那么我們可以得出結論，not(not(R))成立（R卻不必然成立）。太神奇了！
--
※ 發信站: 批踢踢實業坊(ptt.cc), 來自: 124.77.89.116
※ 文章網址: https://webptt.com/m.aspx?n=bbs/logic/M.1423026514.A.572.html
1F：推 ppu12372: 構造邏輯到底是啥? 我GOOGLE後看了維基還是看不懂它是啥 02/04 16:32
2F：→ carelai: 就是排中律(exclusion of middle）不成立的普通邏輯 02/04 16:51
3F：推 ppu12372: 所以他是重新建立的一套系統,可能是只適用在某些狀況瞜? 02/04 16:54
4F：→ ppu12372: 不然你隨便看一個直言命題,排中律都成立呀 02/04 16:54
5F：推 suhorng: @1F: constructive logic, intuitionistic logic 02/04 21:03
6F：→ carelai: 排中律有可能不成立的，比如命題：圓周率pi中含7個數字7 02/04 21:18
7F：→ carelai: 的連續串。這個命題現在無法證明是真是假。 02/04 21:19
8F：推 ppu12372: 可是即使這個命題無法被證明,也沒証明排中律不成立呀 02/04 21:28
9F：推 rossignols: （下列的說明可能不夠精確）就我所知，構造邏輯的起 02/06 02:30
10F：→ rossignols: 源跟一些數學家對於「數學證明要長什麼樣子，數學的 02/06 02:31
11F：→ rossignols: 基礎才夠穩固」的立場有關。有些數學家認為，有幾分 02/06 02:31
12F：→ rossignols: 證據才能說幾分話，想說P有證明，就要直接給出P的證 02/06 02:31
13F：→ rossignols: 明，不能用「非P沒有證明所以P有證明」這種迂迴的方 02/06 02:32
14F：→ rossignols: 式。非P沒有證明，不能保證P一定有證明。 02/06 02:32
15F：→ rossignols: 構造邏輯沒有要證明排中律不成立，而是，基於某些數 02/06 02:32
16F：→ rossignols: 學家對於「數學證明該長什麼樣子的期望」，經過一些人 02/06 02:33
17F：→ rossignols: 研究後發現，要拒絕排中律，才能得到一套能夠用來捕 02/06 02:33
18F：→ rossignols: 捉「那些數學家心中理想的數學證明」的邏輯系統。 02/06 02:33
19F：推 ppu12372: 如果是這樣的話,那那些數學家也太一廂情願了,只是感覺 02/06 13:08
20F：→ ppu12372: 反證法怪怪的就認為不該用,如果沒有反證法,那非歐幾何 02/06 13:09
21F：→ ppu12372: 就不會存在了,沒有非歐幾何,相對論也無法存在了 02/06 13:10
22F：→ suhorng: 為何阿? 這個怎麼推論的? 02/06 18:26
23F：推 rossignols: 這些數學家之所以持這樣的立場，背後是有他們的考量 02/06 21:13
24F：→ rossignols: 的，不過因為我才疏學淺，不確定要怎麼講述他們的考量 02/06 21:15
25F：→ rossignols: ，才不會讓他們看起來很蠢或一廂情願。 02/06 21:15
26F：→ rossignols: （我不確定構造邏輯的起源跟哥德爾不完備定理有沒有 02/06 21:15
27F：→ rossignols: 關係，但，或許看了以下的說法會讓你比較不那麼反感他 02/06 21:15
28F：→ rossignols: 們的立場？）哥德爾的不完備定理說，如果一個系統夠強 02/06 21:16
29F：→ rossignols: （例如皮亞諾算數就夠強），那麼在那個系統裡，就會 02/06 21:16
30F：→ rossignols: 有一些為真的陳述P無法證明出來。難道我們要因為那個 02/06 21:17
31F：→ rossignols: 為真的陳述P沒有證明，就說非P有證明嗎？ 02/06 21:17
32F：→ rossignols: 在古典邏輯裡，有些用反證法證出來的句子，其實不用 02/06 21:18
33F：→ rossignols: 反證法也證得出來，不過證明過程可能會比較複雜麻煩一 02/06 21:18
34F：→ rossignols: 點。 02/06 21:19
35F：推 rossignols: 我不確定拿哥德爾的不完備定理來說明這些數學家的考量 02/06 21:31
36F：→ rossignols: 合不合適。但總之，這些數學家的考量是，他們要的是「 02/06 21:31
37F：→ rossignols: 構式」的數學（跟我們數學教育裡的建構式數學大概沒 02/06 21:31
38F：→ rossignols: 啥關係），數學成果必須是一磚一瓦結結實實地蓋上去 02/06 21:32
39F：→ rossignols: 的，這樣他們才安心。 02/06 21:32
40F：→ rossignols: 漏字了：他們要的是「建構式」的數學 02/06 21:33
41F：推 ppu12372: 我認為你的說法依然無法表達出他們的考量,有一些為真的 02/06 23:33
42F：→ ppu12372: 陳述P無法證明出來,那麼如果運用了排中律,你只能說 02/06 23:35
43F：→ ppu12372: [陳述P可證]該命題為假,而不會說非P可證 02/06 23:37
44F：→ ppu12372: 我想如果我想了解他們的考量的話可能得去參考相關書籍吧 02/06 23:38
45F：推 rossignols: 我目前認為，這可能跟我們是在哪個層面上談排中律有 02/07 01:39
46F：→ rossignols: 關。有一種對「P或非P」的詮釋是，「要嘛P有證明，要 02/07 01:39
47F：→ rossignols: 嘛非P有證明」。採建構式的數學家不接受「要嘛P有證 02/07 01:40
48F：→ rossignols: 明，要嘛非P有證明」是不證自明的，所以在構造邏輯的 02/07 01:40
49F：→ rossignols: 系統裡自然不允許排中律。 02/07 01:41
50F：→ rossignols: 邏輯系統裡的排中律的意義，跟一般日常生活中使用的 02/07 01:41
51F：→ rossignols: 排中律的意義，可能不太一樣。 02/07 01:41
52F：推 ppu12372: 有道理,在你重新闡述他們對排中律的定義後我就大概能 02/07 11:51
53F：→ ppu12372: 理解他們的考量了 02/07 11:51
54F：→ ppu12372: 話說我在想構造邏輯中"排中律"的定義是否和形式邏輯中 02/07 11:54
55F：→ ppu12372: 的"排中律"的定義有些微的不同? 02/07 11:54
56F：推 turboho: 回六樓，圓周率在24658601開始連續出現九個7 02/09 22:36