※ 引述《susophist (窄宅)》之銘言： : ※ 引述《sindarin (官)》之銘言： 謝謝你的回應，對回文內容作刪減，是因為想作一些整理， 略去我覺得可能不是重點而不必提的部分， 因此刪除了部分重要而容易導致誤解的內容，是我的不對，還請見諒。 以下想先對你回應的內容作一些簡單的回應， 再跟著補充幾個可能比較有趣的問題。 : 哪兩件事？ 1. 使用axiom scheme，並在證明中個例化出它的instance， 2. 使用axiom，而在需要的時候用substitution scheme替換成需要的語句。 這兩件事情乍看之下沒有太大的分別， 但牽涉到的是這個系統有沒有辦法被有限的公理給公理化， 從而會致使這個理論有不同的性質，所以才會說二者之間有差異。 : 請回到源頭，有人問臺大試題：證「a=b, therefore b=a」，所給的答案理當是純符號 : 的推導過程，你的例子是非該題之純符號化由「axiom scheme」到「axiom」的一例，這 : 都是清楚的推導或證明的一種，而「axiom scheme」是個「邏輯真」，理當也可以證明 對的，但如同zoneline所說，你會需要再多證一些其他的東西。 其實癥結在底下，中間這一段我想先刪除， : 至此，我同意「(3):if a=b then a=a iff b=a」，可以是一個「axiom」，理由是：它 : 「自我證明的」。但，沒給證明就說是個「axiom」，有疑慮。 如果你只是想要對這個單一axiom的證明，我想給一個model應該就可以了； 如果你想要的是對axiom scheme的證明，就像zoneline提過的，會複雜一些， 大概可以想像要怎麼做，應該是去證明這個axiom scheme的所有instance都是tautology。 不過我沒有看過原本的內容，這點還請zoneline有空的話做些補充。 : 我不認為「(x)(y)[x=y ≡ (F)(Fx≡Fy)]」是「『正確的』LL」，所謂「正確的LL」與 : 大彭孟堯教授的「LL」不一樣，其他的理由與意見，有部份被你拿掉了，這裡看不到， : 如：LL與「正確的LL」可能等價，等等；有需要請回看。 所以這裡的意思會是二階邏輯中也可以有像是一階邏輯中PNF theorem？ 這我不敢說到底有沒有，我只是想重述原發文者的意思，而他的說法看起來也比較合理。 去年當彭老師助教的時候沒有注意到這點，也是我太疏忽，有機會會再向他請教。 : 「很多定理的證明都包含大量非形式的部分」不同意這句，「證明」不就是純符號的推 : 麼；還有，你的「非形式的說明」是什麼。證明就是證明、與給出試題的答案一樣，不 : 要別人去看你指的資料，來作為「證明」，那不是「證明」；你跟我講的「吊書袋」， : 一樣的意思嗎。其他的意見，在你那篇的推文裡。 你對證明的認識可能有一點naive， 我想指出的是：有很多定理的證明包含了非形式語言的使用。 從我手邊找得到的一份講義為例，擷取一段證明， Lemma 3 (Lindenbaum) Every consistent set of sentence Δ can be extended to a maximal consistent set Δ'. Proof: Let f be a bijection with the natural numbers {1, 2, 3, . . .} as domain andthe set of sentences as range (下略) 這裡的內容當然是非形式的， 而在很多其他定理的證明中，包含非常多非形式的部分， 尤其是證明中某一些巧妙的部分，也都得以這樣的方式說明， 我曾和數學系的朋友聊過，我想在數學裡面應該有更多的例子。 是因為這樣，我才說zoneline沒有你所指出的問題。 看到最後可以歸結到兩個問題： 1. Axiom到底是怎樣的東西？ 在Carnap提出了Principle of tolerance以後， 我想應該很少有人會要求axiom非得是self-evident的， 也並非所有self-evident的東西都是axiom； 你在axiom的選擇上好像有弄混的地方。 這部分和邏輯史的發展比較有關係。 2. 我們為什麼使用形式語言？ 相比之下，我覺得這是更大的一個問題； 形式語言到底是日常語言的抽象，還是只是另一個更方便我們寫證明的語言？ 照你對證明的要求，我想會傾向選擇前者，但有越來越多哲學家不同意這一點。 不過這是題外話，如果大家都有興趣才需要談。 簡單一些回應，希望對板友們的討論有些幫助。 --

※ 發信站: 批踢踢實業坊(ptt.cc) ◆ From: 80.114.132.174 ※ 編輯: sindarin 來自: 80.114.132.174 (02/07 15:58)