Re: [討論] 關于構造邏輯

看板logic作者 (XOO)時間10年前 (2015/02/09 06:50), 10年前編輯推噓0(0推 0噓 0→)
留言0則, 0人參與, 最新討論串2/2 (看更多)
※ 發信站: 批踢踢實業坊(ptt.cc), 來自: 124.77.89.116 ※ 文章網址: https://www.ptt.cc/bbs/logic/M.1423026514.A.572.html
推
02/04 16:32,
構造邏輯到底是啥? 我GOOGLE後看了維基還是看不懂它是啥
02/04 16:32
→
02/04 16:51,
就是排中律(exclusion of middle）不成立的普通邏輯
02/04 16:51
推
02/04 16:54,
所以他是重新建立的一套系統,可能是只適用在某些狀況瞜?
02/04 16:54
→
02/04 16:54,
不然你隨便看一個直言命題,排中律都成立呀
02/04 16:54
推
02/04 21:03,
@1F: constructive logic, intuitionistic logic
02/04 21:03
→
02/04 21:18,
排中律有可能不成立的，比如命題：圓周率pi中含7個數字7
02/04 21:18
→
02/04 21:19,
的連續串。這個命題現在無法證明是真是假。
02/04 21:19
推
02/04 21:28,
可是即使這個命題無法被證明,也沒証明排中律不成立呀
02/04 21:28
排中律成不成立是依照不同的邏輯來說的，單純就 forall P . P v ~ P 來說， 在構造式邏輯下是不成立的，驗證的方式可以透過構造式邏輯的模型來判斷。 例如由 實數的開集合跟交集聯集 形成的代數結構，可作為構造式邏輯的模型， A -> B 則是取「 A^c 聯集 B 的 interior set」。那麼 ~P 則詮釋成「 P -> 空集合」 也就是 A^c 的 interior set。在這個模型下可以看出排中律並不恆真。
推
02/06 02:30,
（下列的說明可能不夠精確）就我所知，構造邏輯的起
02/06 02:30
→
02/06 02:31,
源跟一些數學家對於「數學證明要長什麼樣子，數學的
02/06 02:31
→
02/06 02:31,
基礎才夠穩固」的立場有關。有些數學家認為，有幾分
02/06 02:31
→
02/06 02:31,
證據才能說幾分話，想說P有證明，就要直接給出P的證
02/06 02:31
→
02/06 02:32,
明，不能用「非P沒有證明所以P有證明」這種迂迴的方
02/06 02:32
→
02/06 02:32,
式。非P沒有證明，不能保證P一定有證明。
02/06 02:32
→
02/06 02:32,
構造邏輯沒有要證明排中律不成立，而是，基於某些數
02/06 02:32
→
02/06 02:33,
學家對於「數學證明該長什麼樣子的期望」，經過一些人
02/06 02:33
→
02/06 02:33,
研究後發現，要拒絕排中律，才能得到一套能夠用來捕
02/06 02:33
→
02/06 02:33,
捉「那些數學家心中理想的數學證明」的邏輯系統。
02/06 02:33
推
02/06 13:08,
如果是這樣的話,那那些數學家也太一廂情願了,只是感覺
02/06 13:08
→
02/06 13:09,
反證法怪怪的就認為不該用,如果沒有反證法,那非歐幾何
02/06 13:09
→
02/06 13:10,
就不會存在了,沒有非歐幾何,相對論也無法存在了
02/06 13:10
→
02/06 18:26,
為何阿? 這個怎麼推論的?
02/06 18:26
推
02/06 21:13,
這些數學家之所以持這樣的立場，背後是有他們的考量
02/06 21:13
→
02/06 21:15,
的，不過因為我才疏學淺，不確定要怎麼講述他們的考量
02/06 21:15
→
02/06 21:15,
，才不會讓他們看起來很蠢或一廂情願。
02/06 21:15
→
02/06 21:15,
（我不確定構造邏輯的起源跟哥德爾不完備定理有沒有
02/06 21:15
→
02/06 21:15,
關係，但，或許看了以下的說法會讓你比較不那麼反感他
02/06 21:15
→
02/06 21:16,
們的立場？）哥德爾的不完備定理說，如果一個系統夠強
02/06 21:16
→
02/06 21:16,
（例如皮亞諾算數就夠強），那麼在那個系統裡，就會
02/06 21:16
→
02/06 21:17,
有一些為真的陳述P無法證明出來。難道我們要因為那個
02/06 21:17
→
02/06 21:17,
為真的陳述P沒有證明，就說非P有證明嗎？
02/06 21:17
→
02/06 21:18,
在古典邏輯裡，有些用反證法證出來的句子，其實不用
02/06 21:18
→
02/06 21:18,
反證法也證得出來，不過證明過程可能會比較複雜麻煩一
02/06 21:18
→
02/06 21:19,
點。
02/06 21:19
推
02/06 21:31,
我不確定拿哥德爾的不完備定理來說明這些數學家的考量
02/06 21:31
→
02/06 21:31,
合不合適。但總之，這些數學家的考量是，他們要的是「
02/06 21:31
→
02/06 21:31,
構式」的數學（跟我們數學教育裡的建構式數學大概沒
02/06 21:31
→
02/06 21:32,
啥關係），數學成果必須是一磚一瓦結結實實地蓋上去
02/06 21:32
→
02/06 21:32,
的，這樣他們才安心。
02/06 21:32
→
02/06 21:33,
漏字了：他們要的是「建構式」的數學
02/06 21:33
推
02/06 23:33,
我認為你的說法依然無法表達出他們的考量,有一些為真的
02/06 23:33
→
02/06 23:35,
陳述P無法證明出來,那麼如果運用了排中律,你只能說
02/06 23:35
→
02/06 23:37,
[陳述P可證]該命題為假,而不會說非P可證
02/06 23:37
→
02/06 23:38,
我想如果我想了解他們的考量的話可能得去參考相關書籍吧
02/06 23:38
推
02/07 01:39,
我目前認為，這可能跟我們是在哪個層面上談排中律有
02/07 01:39
→
02/07 01:39,
關。有一種對「P或非P」的詮釋是，「要嘛P有證明，要
02/07 01:39
→
02/07 01:40,
嘛非P有證明」。採建構式的數學家不接受「要嘛P有證
02/07 01:40
→
02/07 01:40,
明，要嘛非P有證明」是不證自明的，所以在構造邏輯的
02/07 01:40
→
02/07 01:41,
系統裡自然不允許排中律。
02/07 01:41
→
02/07 01:41,
邏輯系統裡的排中律的意義，跟一般日常生活中使用的
02/07 01:41
→
02/07 01:41,
排中律的意義，可能不太一樣。
02/07 01:41
另一個說法是，構造式邏輯具有計算意義，能夠用構造式邏輯證明的描述， 自然就能夠將目標造出來，要證明所有的自然數都可以寫成 2n + k, k = 0, 1 自然就是給一個型式的構造，說明如何給定任意自然數，都能夠推算成以上的形式。 這在當今邏輯的應用領域——形式驗證——占了舉足輕重的地位。
推
02/07 11:51,
有道理,在你重新闡述他們對排中律的定義後我就大概能
02/07 11:51
→
02/07 11:51,
理解他們的考量了
02/07 11:51
→
02/07 11:54,
話說我在想構造邏輯中"排中律"的定義是否和形式邏輯中
02/07 11:54
→
02/07 11:54,
的"排中律"的定義有些微的不同?
02/07 11:54
兩者排中律的形式是一樣的。另外補充一點，事實上我們可以將古典邏輯的語句 透過 Double-negation translation 翻譯成構造式邏輯的語句，那麼當一個 語句是古典下恆真 iff 該翻譯的語句是構造式恆真 也就是說，構造式邏輯是比古典邏輯還要更精微的語言， 而古典邏輯下不能夠分辨可不可構造。 -- ※ 發信站: 批踢踢實業坊(ptt.cc), 來自: 85.180.232.188 ※ 文章網址: https://www.ptt.cc/bbs/logic/M.1423435804.A.7CF.html ※ 編輯: xcycl (85.180.232.188), 02/09/2015 06:50:23
‣ 更多 xcycl 的文章
文章代碼(AID): #1Kr-WSVF (logic)
討論串 (同標題文章)
本文引述了以下文章的的內容：
完整討論串 (本文為第 2 之 2 篇)：
排序： 最新先 | 最舊先 | 留言數
在新視窗開啟完整討論串 (共2篇)
‣ 更多 xcycl 的文章
文章代碼(AID): #1Kr-WSVF (logic)