作者xcycl (XOO)
看板logic
標題Re: [討論] 關于構造邏輯
時間Mon Feb 9 06:50:01 2015
※ 發信站: 批踢踢實業坊(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
排中律成不成立是依照不同的邏輯來說的，單純就 forall P . P v ~ P 來說，
在構造式邏輯下是不成立的，驗證的方式可以透過構造式邏輯的模型來判斷。
例如由 實數的開集合跟交集聯集 形成的代數結構，可作為構造式邏輯的模型，
A -> B 則是取「 A^c 聯集 B 的 interior set」。那麼 ~P 則詮釋成「 P -> 空集合」
也就是 A^c 的 interior set。在這個模型下可以看出排中律並不恆真。
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
另一個說法是，構造式邏輯具有計算意義，能夠用構造式邏輯證明的描述，
自然就能夠將目標造出來，要證明所有的自然數都可以寫成 2n + k, k = 0, 1
自然就是給一個型式的構造，說明如何給定任意自然數，都能夠推算成以上的形式。
這在當今邏輯的應用領域——形式驗證——占了舉足輕重的地位。
52F：推 ppu12372: 有道理,在你重新闡述他們對排中律的定義後我就大概能 02/07 11:51
53F：→ ppu12372: 理解他們的考量了 02/07 11:51
54F：→ ppu12372: 話說我在想構造邏輯中"排中律"的定義是否和形式邏輯中 02/07 11:54
55F：→ ppu12372: 的"排中律"的定義有些微的不同? 02/07 11:54
兩者排中律的形式是一樣的。另外補充一點，事實上我們可以將古典邏輯的語句
透過 Double-negation translation 翻譯成構造式邏輯的語句，那麼當一個
語句是古典下恆真 iff 該翻譯的語句是構造式恆真
也就是說，構造式邏輯是比古典邏輯還要更精微的語言，
而古典邏輯下不能夠分辨可不可構造。
--
※ 發信站: 批踢踢實業坊(ptt.cc), 來自: 85.180.232.188
※ 文章網址: https://webptt.com/m.aspx?n=bbs/logic/M.1423435804.A.7CF.html
※ 編輯: xcycl (85.180.232.188), 02/09/2015 06:50:23