Re: [請益] 證明a=b,then b=a
※ 引述《sindarin (官)》之銘言：
: ※ 引述《susophist (窄宅)》之銘言：
: 想跟著這個討論釐清一下自己也常常混淆的一些概念問題，還請各位不吝指正。
: : 把該「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))。
: 當然你可以說這兩件事情是一樣的意思，
哪兩件事？
: 但不同公理化方式會有一些理論上的優劣不同，
: 這個部份我不是非常清楚，還請各位補充。
: 無論如何，你要說的不是完全錯的，
: 只是你應該要知道做出這個區分的目的何在。
請回到源頭，有人問臺大試題：證「a=b, therefore b=a」，所給的答案理當是純符號化
的推導過程，你的例子是非該題之純符號化由「axiom scheme」到「axiom」的一例，這些
都是清楚的推導或證明的一種，而「axiom scheme」是個「邏輯真」，理當也可以證明之
；而不是只是說『某個句子如(2)是「axiom scheme」，那個句子是它的「axiom」』。
: : 這裡是邏輯的證明，引用維基百科，學術嚴謹度很可疑；除非，是在做社會學的資料統
: : 計，等等，較不數理式的論說，「維基」可能還有一些參考的價值。
: 我以為這個部分比較像是邏輯史的簡單考究，援引一些大家都方便查到的東西做參考；
: 揪著資料來源質疑，並不能讓你所做出的證明更有說服力。我想這裡不必著墨太多。
一樣；有人問「a=b, therefore b=a」證明的試題解答，M君說他自己如維基百科，將其
「(1): (x)(x=x)」稱作「reflexivity」，然而，兩者事實上有別。
: : 我想，「I」既然是個邏輯推論的規則，就會像其他的邏輯推論規則(MP, DeM, CP, etc.)
: : 一樣，能夠在其系統內「自我證明」，要不就是「後設地證明」；不太可能會有「不同
: : 的」詮釋的空間，因此，你說的「LL」與我說的「I」，應該是不完全相同的東西。
: 這裡的說明我也看得不是很懂，
: 你的意思是說：LL有詮釋的空間，而你使用的I沒有；所以你使用的I與LL不同？
文章大家來回數篇，有些東西「滑動了」；我的「LL」是「(x)(y)(F)[x=y ≡ (Fx≡Fy)]
」，M君的「LL」是「axiom scheme: (x)(y)[x=y → (Fx≡Fy), F是後設語言的符號」，
我的意思是，推論規則「I」與M君的「LL」作為「axiom scheme」，是不同的；不是在說
你說的「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。
如推論：
1(1) a=b A.
2(2) a=a A.
1,2(3) b=a (2), (1) I
1(4) a=a → b=a (2)-(3) CP
5(5) b=a A.
1,5(6) a=a (5), (1) I
1(7) b=a → a=a (5)-(6) CP
1(8) (a=a → b=a) & (b=a → a=a) (4), (7) Conj
1(9) a=a≡b=a (8) Equi
(10) a=b → (a=a≡b=a) (1)-(9) CP
(11) (x)(y)[x=y → (x=x≡y=x) (10)UG, a/x, b/y
{}├ a=b → (a=a≡b=a)
{}├ (x)(y)[x=y → (x=x≡y=x)
至此，我同意「(3):if a=b then a=a iff b=a」，可以是一個「axiom」，理由是：它是
「自我證明的」。但，沒給證明就說是個「axiom」，有疑慮。
: : 我不會說(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。
我不認為「(x)(y)[x=y ≡ (F)(Fx≡Fy)]」是「『正確的』LL」，所謂「正確的LL」與臺
大彭孟堯教授的「LL」不一樣，其他的理由與意見，有部份被你拿掉了，這裡看不到，例
如：LL與「正確的LL」可能等價，等等；有需要請回看。
: 另外也對推文提出一點疑問：
: → susophist:我覺得你在吊書袋，邏輯就是每一步都很清楚，不需要「簡 12/22 06:13
: → susophist:化」、「是____的意思」，等等的說詞，只要按部就班，沒 12/22 06:14
: → susophist:學過的人也可以看得懂。 12/22 06:15
: → susophist:就像證「if a=b then b=a」一樣，證(2)是「axiom schema 12/22 06:18
: → susophist:」、證從(2)得到「Law of Identity」，沒能證明嗎。 12/22 06:19
: 我想，邏輯本身當然需要很多非形式的說明，
: 很多定理的證明都包含大量非形式的部分，尤其在闡述某些特定作法的時候，
: 因此，使用這些說明做為輔助並無不妥；
: 這跟吊書袋好像沒有太大的關係，
: 相較起來，我覺得言必稱某某老師更像是一種無謂的訴諸權威，
: 當然，我想你或許沒有那個意思，但這個行為跟引經據典是相類似的，
: 書袋或否，大可不必如此認真看待。
「很多定理的證明都包含大量非形式的部分」不同意這句，「證明」不就是純符號的推導
麼；還有，你的「非形式的說明」是什麼。證明就是證明、與給出試題的答案一樣，不是
要別人去看你指的資料，來作為「證明」，那不是「證明」；你跟我講的「吊書袋」，是
一樣的意思嗎。其他的意見，在你那篇的推文裡。
--
※ 發信站: 批踢踢實業坊(ptt.cc)
◆ From: 180.176.200.225
※ 編輯: susophist 來自: 180.176.200.225 (12/23 11:15)
討論串 (同標題文章)