※ 引述《sindarin (官)》之铭言： : ※ 引述《susophist (窄宅)》之铭言： : 想跟着这个讨论厘清一下自己也常常混淆的一些概念问题，还请各位不吝指正。 : : 把该「axiom scheme」(用拉丁文等)给符号化(symbolize)，以「个例化」出特定的 : : 「axiom」，如「(x)(y)[x=y → (x=x≡y=x)]」，再UI成「a=b → (a=a≡b=a)」，不正 : : 是个逻辑上清楚的推导麽。该「axiom scheme」亦能合逻辑推导规则地「自我证明」为 : : 「公理」，不是如此麽。 : 我想你好像不是很明白axiom和axiom scheme两个概念的区别。 : 区分axiom和axiom scheme的功能主要是在於：有了axiom scheme， : 我们可以在证明的任意一个步骤中加入我们想要的合於此scheme的句子，以进行证明； : 换句话说，一个axiom scheme应该被当作所有合於此形式的句子(也就是axiom)的集合， : 这个集合内的所有语句都能被加进证明中， : 在axiom scheme出现以前，逻辑学家们做的事情乍看之下是差不多的， : 是将axiom内的propositional letter指定替换成另一个propositional letter， : 譬如说我现在想要用的句子是(P→Q)→(R→(P→Q))， : 但axiom的内容是P→(Q→P)，我就指定一个Substitution scheme， : （抱歉，有点不确定是不是叫做这个名字了）写成： : P├ P→Q : Q├ R : 藉此可以得到我想要的(P→Q)→(R→(P→Q))。 : 当然你可以说这两件事情是一样的意思， 哪两件事？ : 但不同公理化方式会有一些理论上的优劣不同， : 这个部份我不是非常清楚，还请各位补充。 : 无论如何，你要说的不是完全错的， : 只是你应该要知道做出这个区分的目的何在。 请回到源头，有人问台大试题：证「a=b, therefore b=a」，所给的答案理当是纯符号化 的推导过程，你的例子是非该题之纯符号化由「axiom scheme」到「axiom」的一例，这些 都是清楚的推导或证明的一种，而「axiom scheme」是个「逻辑真」，理当也可以证明之 ；而不是只是说『某个句子如(2)是「axiom scheme」，那个句子是它的「axiom」』。 : : 这里是逻辑的证明，引用维基百科，学术严谨度很可疑；除非，是在做社会学的资料统 : : 计，等等，较不数理式的论说，「维基」可能还有一些参考的价值。 : 我以为这个部分比较像是逻辑史的简单考究，援引一些大家都方便查到的东西做参考； : 揪着资料来源质疑，并不能让你所做出的证明更有说服力。我想这里不必着墨太多。 一样；有人问「a=b, therefore b=a」证明的试题解答，M君说他自己如维基百科，将其 「(1): (x)(x=x)」称作「reflexivity」，然而，两者事实上有别。 : : 我想，「I」既然是个逻辑推论的规则，就会像其他的逻辑推论规则(MP, DeM, CP, etc.) : : 一样，能够在其系统内「自我证明」，要不就是「後设地证明」；不太可能会有「不同 : : 的」诠释的空间，因此，你说的「LL」与我说的「I」，应该是不完全相同的东西。 : 这里的说明我也看得不是很懂， : 你的意思是说：LL有诠释的空间，而你使用的I没有；所以你使用的I与LL不同？ 文章大家来回数篇，有些东西「滑动了」；我的「LL」是「(x)(y)(F)[x=y ≡ (Fx≡Fy)] 」，M君的「LL」是「axiom scheme: (x)(y)[x=y → (Fx≡Fy), F是後设语言的符号」， 我的意思是，推论规则「I」与M君的「LL」作为「axiom scheme」，是不同的；不是在说 你说的「LL有诠释的空间」。 : : 您的「(3):if a=b then a=a iff b=a」也就是「a=b → (a=a≡b=a)」，其中「a」与「b : : 」是指特定的东西(individual)，如此，您的(3)怎麽会是个「axiom」呢。 : 这里的(3)是axiom，正是因为他是从scheme个例化而来； : 我可以同样地带入任何其他的individual，这个句子都还是axiom。 : 你的质疑仍然是源自於混淆axiom和axiom scheme。 如推论： 1(1) a=b A. 2(2) a=a A. 1,2(3) b=a (2), (1) I 1(4) a=a → b=a (2)-(3) CP 5(5) b=a A. 1,5(6) a=a (5), (1) I 1(7) b=a → a=a (5)-(6) CP 1(8) (a=a → b=a) & (b=a → a=a) (4), (7) Conj 1(9) a=a≡b=a (8) Equi (10) a=b → (a=a≡b=a) (1)-(9) CP (11) (x)(y)[x=y → (x=x≡y=x) (10)UG, a/x, b/y {}├ a=b → (a=a≡b=a) {}├ (x)(y)[x=y → (x=x≡y=x) 至此，我同意「(3):if a=b then a=a iff b=a」，可以是一个「axiom」，理由是：它是 「自我证明的」。但，没给证明就说是个「axiom」，有疑虑。 : : 我不会说(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) : 大家都知道这里的G不是一个量词，问题在於： : 你对LL做了三次UI，而得到(5) b=a ≡(Gb≡Ga)， : 照正确的LL，应该是做两次UI，而得到 b=a ≡ (G)(Ga≡Gb)， : 也就是说，你要有(G)(Ga≡Gb)这个句子，才能用MP得到a=b， : (for all G, Ga iff Gb) : 这个句子的意思显然跟这个句子做UI以後差很多， : 一个是在说：对所有性质G，a具有G的性质，若且唯若b有G的性质； : 它做UI以後的结果变成是：a具有一个特定性质G若且唯若b也具有性质G : 从这一个句子推到a=b显然是很奇怪的， : 这就像是说a跟b都在吃西瓜，所以他们是同一个东西， : 在推到a=b这一步的时候，你需要的是有全称量限词的那个句子， : 也就是不管a怎样（吃西瓜、削铅笔、打撞球），b也都是这样， : 这才能让我们得到a=b。 我不认为「(x)(y)[x=y ≡ (F)(Fx≡Fy)]」是「『正确的』LL」，所谓「正确的LL」与台 大彭孟尧教授的「LL」不一样，其他的理由与意见，有部份被你拿掉了，这里看不到，例 如：LL与「正确的LL」可能等价，等等；有需要请回看。 : 另外也对推文提出一点疑问： : → susophist:我觉得你在吊书袋，逻辑就是每一步都很清楚，不需要「简 12/22 06:13 : → susophist:化」、「是____的意思」，等等的说词，只要按部就班，没 12/22 06:14 : → susophist:学过的人也可以看得懂。 12/22 06:15 : → susophist:就像证「if a=b then b=a」一样，证(2)是「axiom schema 12/22 06:18 : → susophist:」、证从(2)得到「Law of Identity」，没能证明吗。 12/22 06:19 : 我想，逻辑本身当然需要很多非形式的说明， : 很多定理的证明都包含大量非形式的部分，尤其在阐述某些特定作法的时候， : 因此，使用这些说明做为辅助并无不妥； : 这跟吊书袋好像没有太大的关系， : 相较起来，我觉得言必称某某老师更像是一种无谓的诉诸权威， : 当然，我想你或许没有那个意思，但这个行为跟引经据典是相类似的， : 书袋或否，大可不必如此认真看待。 「很多定理的证明都包含大量非形式的部分」不同意这句，「证明」不就是纯符号的推导 麽；还有，你的「非形式的说明」是什麽。证明就是证明、与给出试题的答案一样，不是 要别人去看你指的资料，来作为「证明」，那不是「证明」；你跟我讲的「吊书袋」，是 一样的意思吗。其他的意见，在你那篇的推文里。 --

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