Re: [請益] 證明a=b,then b=a
※ 引述《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
→
12/24 00:43, , 1F
12/24 00:43, 1F
→
12/24 00:48, , 2F
12/24 00:48, 2F
→
12/24 00:50, , 3F
12/24 00:50, 3F
→
12/24 00:51, , 4F
12/24 00:51, 4F
→
12/24 00:52, , 5F
12/24 00:52, 5F
※ 編輯: sindarin 來自: 80.114.132.174 (02/07 15:58)
討論串 (同標題文章)