Re: [請益] 證明a=b,then b=a
簡短回應:
1. zoneline 的回應沒有錯, 我那個證明用的
for all x for all y, if x=y, then Fx iff Fy
是一個 axiom scheme。
2. 我覺得很大的一部份是名稱問題。在一般的 first-order logic裡,
一定會有這一條, 只是有的把它放在 axioms裡為一個axiom scheme,
有的把它看成是inference rule。有的人稱它為 LL (Leibniz's law),
有的人稱它為 SI (substitution of identity), 有的人稱它為
Identity elimination。我這裡的是把它叫做 LL, 這種稱法我自認為
是很傳統的稱呼。例如 wiki 這裡也是這樣叫
http://en.wikipedia.org/wiki/First-order_logic#Equality_and_its_axioms
(我手中沒有其它網路上有的資料).
(在 wiki 這裡也是稱我的(1)和(2)為 reflexivity 和 SI (或LL)，
I think that's a standard name).
3. susophist 在後面那篇給的那個簡單的證明，我認為和我一開始給的那個
是一樣的。惟一的差別只是你要把那條推論規則／公設稱為 law of identity
還是稱它是 Leibniz's Law。
4. 我原本的證明的確不夠嚴緊, 我發現裡面有一個錯誤, 是在這裡:
3. if a=b then a=a iff b=a (2) UI
在我的證明裡我把它稱為 (2) 的UI, 但這是錯的。
應該是UI這個稱呼讓 susophist 誤會我沒有把它看成 axiom scheme
正確的寫法應該是:
3. if a=b then a=a iff b=a (axiom) instance of (2)
也就是說, 這條直接是公設的instance, 不是用 UI 得來的。
5. Second order logic 可以定義 Identity, 這時也會把這定義稱為是
Leibniz's law, 但這個Leibniz's Law 與 first order logic中被當成
是 axiom scheme/rule 的 LL 是不同的。
6. 在 Second-order logic 中的 Leibniz's Law 是這一個:
(x)(y)[x=y ≡ (F)(Fx≡Fy)]
(請注意 (F) 的 scope). susophist 在第一篇文章裡給的是有錯的.
差別在於, 你只能從所有的性質都滿足(Fa≡Fb)時你才能推出 a=b
而不是對於任何的F, 若(Fa≡Fb)則a=b.
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, 但這無法推得它們是同一個東西。
要推得它們是同一個, 你必須要有 (G)(Gb≡Ga); 而不是 Gb≡Ga。
以上回應, 希望對討論有幫助。
--
※ 發信站: 批踢踢實業坊(ptt.cc)
◆ From: 111.249.188.40
※ 編輯: MathTurtle 來自: 111.249.188.40 (12/22 12:14)
討論串 (同標題文章)
以下文章回應了本文：
完整討論串 (本文為第 8 之 13 篇)：