我觉得重点在於, 在一个proof theory里(例如: natural deduction), 引入恒真句并不是一件理所当然的事情, 你通常会需要一些meta-theory来允许你这麽做, 其中一个可能会用到的, 如: 完备性定理, (即: 凡是真的皆可以被证明) 不见得在每一个系统中都成立。 换言之, 恒真句就算是「不管在什麽情况下都会为真」, 也不保证你能在你的系统当中证出它来, 如果你的系统证不出某个恒真句, 你就无法合法地引入它作为你的前提。 如此例中, 如果你的系统证不出 R v ~R, 那麽你无法引入 R v ~R 作为前提。 而的确在直觉主义的自然演译法中, (briefly, 不能使用RAA的自然演译法), 你是证不出 R v ~R的。 ※ 引述《maylaw (讨厌傲娇)》之铭言： : ※ 引述《aletheia (cOnJeCTuRe)》之铭言： : : 你这样说不太对 : : 直觉主义认为排中律并不成立 : : 对於他们来说 (φvψ)指的是 : : "φ可以建构出一个证明或者ψ可以建构出一个证明" : : 对於(pv~p)来说 : : 除非能说明所有的句子与其negation不能皆同时找到证明 : : 那不能说明排中律成立 : : 另外我也觉得自然演绎法在过程中直接放入恒真句怪怪的 : : 有书可以参考一下嘛 我只知道Gentzen版本的 : 「直觉主义认为」是「直觉主义者认为」，只有理性生物会思考，才会认为； : 主义本身不会「认为」。 : 所以目前问题区分成两个部份，是不是有恒真句的问题， : 跟恒真句能否直接引进推论的问题： : 1.恒真句是存在的吗？ : 你这段话： : "φ可以建构出一个证明或者ψ可以建构出一个证明" : 对於(pv~p)来说 : 除非能说明所有的句子与其negation不能皆同时找到证明 : 我看不懂在说什麽，可否举例辅助？ : φ可以建构出一个证明，究竟是以φ为前提来做出论证证明其他陈述？ : 还是以φ为结论，可用论证来证明φ为真？ 一命题是否为一个恒「真」句, 有时要看你给的 semantics是什麽, aletheia的这句话, 是直觉主义对logical connectives (not and if), 所给出的一种可能的semantics, 我们通常称为 Kripke semantics。 用「可证性」来理解一句子的「真」, 是一种对Kripke semantics的理解方式, 也就是说, ~φ 为「可证」, 若且惟若, 在以後时间中都不会找到φ为「可证」, 而因此, (pv~p)有可能在 p不为「可证」, 同时~p也不为「可证」的情形下, (pv~p)也不为「可证」。 举例而言, 我们把哥德巴赫猜想写成命题p, 在这诠释下, p不是可证的, ~p也不是可证的, (虽然未来某刻可能其中一个会被证出来) 而因此 p or not p 不是可证的。 : 话说恒真句对我们而言没有成立或不成立的问题，恒真句不管在什麽情况下都会为真， : 因此它并不从任何有别於它的陈述句导出来，也就是它的真并不依赖於其他叙述、现象、 : 事物等。因此恒真句的真假也不需要被检证。它也无法提供我们任何资讯，例如「白色 : 的墙壁是白色的」，一般我们都会说：「啊这不是废话吗？」不过这是不是为真？是！ : 至於所谓的排中律，若举个例子来讲：「蚂蚁是红色的或蚂蚁不是红色的」，也是恒真句 : ，除了红色跟不是红色以外，还有第三种可能吗？有可能既是红色的又不是红色的吗？ : 尤其这段话： : 「除非能说明所有的句子与其negation不能皆同时找到证明，那不能说明排中律成立」 : 以上述的蚂蚁作为例子，我想问问直觉主义：「你能找到一只同时既是红色的又不是红 : 色的蚂蚁吗？」，没有任何事物存有这样的矛盾，你不能把陈述分开来看，不能找一只 : 不是红色的蚂蚁，跟一只是红色的蚂蚁，然後告诉我：「我同时证明这蚂蚁是红色的跟 : 另一只蚂蚁不是红色的」，问题是那是两只，但是当我说「蚂蚁不可能既是红色的又不 : 是红色的」，这时候我是讲同一只蚂蚁。你要拿两个不同的个例，然後做出两句陈述， : 以选言符号摆在一起当然不会有矛盾，但是当我们陈述同一个例的时候，我们是不可能 : 找到既是肯定它如何如何，又否定它如何如何，的矛盾例子，这是不可能的。 : 至於能否引入恒真句证明容我下次再说，上班去～～ (p & ~p)的不成立, 与 (p v ~p)的成立, 在直觉主义当中是两回事, 大部份的直觉主义不接受 (p & ~p) (除非你是paraconsistent logic) 但却也不接受 (p v ~p)。 [矛盾律与排中律是不一样的, 要从矛盾律导排中律, 你可能要预设某些东西] 而如果你想要从, 假设排中律不成立, 我们可以找到矛盾, 因此排中律成立, 这刚好就是直觉主义者不接受的 RAA 证明方式。 --

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