[討論] 關于構造邏輯

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