Re: [請益] 證明a=b,then b=a
※ 引述《susophist (窄宅)》之銘言：
: ※ 引述《MathTurtle (恩典)》之銘言：
想跟著這個討論釐清一下自己也常常混淆的一些概念問題，還請各位不吝指正。
: 把該「axiom scheme」(用拉丁文等)給符號化(symbolize)，以「個例化」出特定的
: 「axiom」，如「(x)(y)[x=y → (x=x≡y=x)]」，再UI成「a=b → (a=a≡b=a)」，不正
: 是個邏輯上清楚的推導麼。該「axiom scheme」亦能合邏輯推導規則地「自我證明」為
: 「公理」，不是如此麼。
我想你好像不是很明白axiom和axiom scheme兩個概念的區別。
區分axiom和axiom scheme的功能主要是在於：有了axiom scheme，
我們可以在證明的任意一個步驟中加入我們想要的合於此scheme的句子，以進行證明；
換句話說，一個axiom scheme應該被當作所有合於此形式的句子(也就是axiom)的集合，
這個集合內的所有語句都能被加進證明中，
在axiom scheme出現以前，邏輯學家們做的事情乍看之下是差不多的，
是將axiom內的propositional letter指定替換成另一個propositional letter，
譬如說我現在想要用的句子是(P→Q)→(R→(P→Q))，
但axiom的內容是P→(Q→P)，我就指定一個Substitution scheme，
（抱歉，有點不確定是不是叫做這個名字了）寫成：
P├ P→Q
Q├ R
藉此可以得到我想要的(P→Q)→(R→(P→Q))。
當然你可以說這兩件事情是一樣的意思，
但不同公理化方式會有一些理論上的優劣不同，
這個部份我不是非常清楚，還請各位補充。
無論如何，你要說的不是完全錯的，
只是你應該要知道做出這個區分的目的何在。
: 這裡是邏輯的證明，引用維基百科，學術嚴謹度很可疑；除非，是在做社會學的資料統
: 計，等等，較不數理式的論說，「維基」可能還有一些參考的價值。
我以為這個部分比較像是邏輯史的簡單考究，援引一些大家都方便查到的東西做參考；
揪著資料來源質疑，並不能讓你所做出的證明更有說服力。我想這裡不必著墨太多。
: : 3. susophist 在後面那篇給的那個簡單的證明，我認為和我一開始給的那個
: : 是一樣的。惟一的差別只是你要把那條推論規則／公設稱為 law of identity
: : 還是稱它是 Leibniz's Law。
: 我想，「I」既然是個邏輯推論的規則，就會像其他的邏輯推論規則(MP, DeM, CP, etc.)
: 一樣，能夠在其系統內「自我證明」，要不就是「後設地證明」；不太可能會有「不同
: 的」詮釋的空間，因此，你說的「LL」與我說的「I」，應該是不完全相同的東西。
這裡的說明我也看得不是很懂，
你的意思是說：LL有詮釋的空間，而你使用的I沒有；所以你使用的I與LL不同？
: 您的「(3):if a=b then a=a iff b=a」也就是「a=b → (a=a≡b=a)」，其中「a」與「b
: 」是指特定的東西(individual)，如此，您的(3)怎麼會是個「axiom」呢。
這裡的(3)是axiom，正是因為他是從scheme個例化而來；
我可以同樣地帶入任何其他的individual，這個句子都還是axiom。
你的質疑仍然是源自於混淆axiom和axiom scheme。
: : 7. 因此, susophist 第一篇文章的那個二階證明是錯的。
: : 問題出在這裡:
: : (5) b=a ≡ (Gb≡Ga) (3) x/b, y/a, F/G
: : ..........
: : 1(9) Gb≡Ga (8) '≡' equivalent
: : 1(10) b=a (9), (5) MP
: : 很明顯, (5) 是錯誤的LL, 所以你不應該能夠從 Gb≡Ga 推得 b=a
: : Gb≡Ga 只告訴你 a 和 b 同時有G或同時沒有G, 但這無法推得它們是同一個東西
: 我不會說(5)是個「LL」，(5)只是個從LL「個例化(UI)」而來的句子之一。
: 按照邏輯(語法/符號上的)規則，從(5)與(9)，依「前斷律(MP)」得，(10): b=a，沒錯
: 吧；你說的「(Gb≡Ga)」只有在「同時有G或同時沒有G」時為真，但，
: 「b=a ≡ (Gb≡Ga)」整句要為真，「(Gb≡Ga)」不一定要為真、也可以為假，
: 這是「實質蘊涵」(materially imply)的意思、也就是「→」的真值表(truth table)；
: 更何況，我的(5)...(9)和(10)，是在(2)的歸謬法的假設之中，不論如何，只要有「矛
: 盾句」，便可得與假設反面的結論「b=a」。要推得它們是同一個, 你必須要有
: (G)(Gb≡Ga); 而不是 Gb≡Ga。請注意，我的「G」是「代入述詞全稱量詞(F)的G」，
: 「G」不是一個量詞(quantifier)
大家都知道這裡的G不是一個量詞，問題在於：
你對LL做了三次UI，而得到(5) b=a ≡(Gb≡Ga)，
照正確的LL，應該是做兩次UI，而得到 b=a ≡ (G)(Ga≡Gb)，
也就是說，你要有(G)(Ga≡Gb)這個句子，才能用MP得到a=b，
(for all G, Ga iff Gb)
這個句子的意思顯然跟這個句子做UI以後差很多，
一個是在說：對所有性質G，a具有G的性質，若且唯若b有G的性質；
它做UI以後的結果變成是：a具有一個特定性質G若且唯若b也具有性質G
從這一個句子推到a=b顯然是很奇怪的，
這就像是說a跟b都在吃西瓜，所以他們是同一個東西，
在推到a=b這一步的時候，你需要的是有全稱量限詞的那個句子，
也就是不管a怎樣（吃西瓜、削鉛筆、打撞球），b也都是這樣，
這才能讓我們得到a=b。
另外也對推文提出一點疑問：
→
12/22 06:13,
12/22 06:13
→
12/22 06:14,
12/22 06:14
→
12/22 06:15,
12/22 06:15
→
12/22 06:18,
12/22 06:18
→
12/22 06:19,
12/22 06:19
我想，邏輯本身當然需要很多非形式的說明，
很多定理的證明都包含大量非形式的部分，尤其在闡述某些特定作法的時候，
因此，使用這些說明做為輔助並無不妥；
這跟吊書袋好像沒有太大的關係，
相較起來，我覺得言必稱某某老師更像是一種無謂的訴諸權威，
當然，我想你或許沒有那個意思，但這個行為跟引經據典是相類似的，
書袋或否，大可不必如此認真看待。
--
※ 發信站: 批踢踢實業坊(ptt.cc)
◆ From: 80.114.132.174
※ 編輯: sindarin 來自: 80.114.132.174 (12/23 05:34)
→
12/23 08:37, , 1F
12/23 08:37, 1F
→
12/23 08:38, , 2F
12/23 08:38, 2F
→
12/23 08:39, , 3F
12/23 08:39, 3F
→
12/23 08:43, , 4F
12/23 08:43, 4F
→
12/23 08:48, , 5F
12/23 08:48, 5F
討論串 (同標題文章)
以下文章回應了本文：
完整討論串 (本文為第 10 之 13 篇)：