※ 引述《MathTurtle (恩典)》之铭言： : 简短回应: : 1. zoneline 的回应没有错, 我那个证明用的 : for all x for all y, if x=y, then Fx iff Fy : 是一个 axiom scheme。 把该「axiom scheme」(用拉丁文等)给符号化(symbolize)，以「个例化」出特定的 「axiom」，如「(x)(y)[x=y → (x=x≡y=x)]」，再UI成「a=b → (a=a≡b=a)」，不正是 个逻辑上清楚的推导麽。该「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。 我想，「I」既然是个逻辑推论的规则，就会像其他的逻辑推论规则(MP, DeM, CP, etc.) 一样，能够在其系统内「自我证明」，要不就是「後设地证明」；不太可能会有「不同的 」诠释的空间，因此，你说的「LL」与我说的「I」，应该是不完全相同的东西。 : 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 得来的。 您的「(3):if a=b then a=a iff b=a」也就是「a=b → (a=a≡b=a)」，其中「a」与「b 」是指特定的东西(individual)，如此，您的(3)怎麽会是个「axiom」呢。 : 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. 是这样子吗，你是对的吗？如果说我有错，那也会是台大教授彭孟尧的错，因为我的「LL: (x)(y)(F)[x=y ≡ (Fx≡Fy)]」是从彭的讲义引用来的，在我的发文里有该讲义的网址； 有没有可能「(x)(y)[x=y ≡ (F)(Fx≡Fy)]」与「(x)(y)(F)[x=y ≡ (Fx≡Fy)]」是逻辑 上「等价」的，即，两者可相互推导得出彼此，假如是，那就没有你说的「差别」了： (x)(y)(F)[x=y ≡ (Fx≡Fy)]▕— (x)(y)[x=y ≡ (F)(Fx≡Fy)] (x)(y)[x=y ≡ (F)(Fx≡Fy)]▕— (x)(y)(F)[x=y ≡ (Fx≡Fy)] : 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, 但这无法推得它们是同一个东西。 我不会说(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)。 --

※ 发信站: 批踢踢实业坊(ptt.cc) ◆ From: 140.114.118.67 ※ 编辑: susophist 来自: 140.114.118.67 (12/22 22:12)