※ 引述《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 ※ 编辑: sindarin 来自: 80.114.132.174 (02/07 15:58)