作者MathTurtle (恩典)
看板logic
标题Re: [请益] 证明a=b,then b=a
时间Sun Dec 22 12:04:12 2013
简短回应:
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)