※ 引述《maylaw (讨厌傲娇)》之铭言： : ※ 引述《MathTurtle (恩典)》之铭言： : : 一命题是否为一个恒「真」句, : : 有时要看你给的 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 不是可证的。 : 如果一个语句具有可证性，则是因为它有真假可言。不具有真假可言的语句还谈 : 什麽恒真恒假？形式逻辑的系统只适用於有真假可言的语句，你拿没有真假可言 : 的语句作为例子不是很奇怪吗？形式逻辑的效力有限，它并不能百分之百吻合我 : 们的思维，这我想所有的逻辑学家都会承认。 为何我拿了没有真假可言的语句作例子呢? 假设p表示「任何大於2的偶数皆为两个质数的和。」, 这个命题是有真假可言的: p为真, 若且惟若, 任何大於2的偶数皆为两个质数的和。 但是p目前没有被证出来, 它的反命题~p, 也就是「存在一大於2的偶数不是两个质数和」 也没有被证出来, 因此如果我们用有没有被证出来, 来诠释Kripke semantics中以「可证」给出logical connectives的semantics, 那麽, pv~p在这里是不成立的。 这里我们还是要区分, 「可证」作为Kripke semantics的一种诠释方式, 以及「可证」作为实际上的证明。 前者只是一种我们在meta-theory中所给予某一特定proof theory (如: natural deduction of intuistic logic)的semantics。 这有点confusing我知道, 因为「可证」拿来当成了semantics的概念, 这也是为何我其实不太喜欢用可证来诠释Kripke semantics, 还是比较偏好用possible world semantics来诠释。 : 另外就是恒真句是否可引入推论之中的问题，很抱歉我看的书比较少，目前看到 : 有人这样用的就是Stephen F. Barker，他写的逻辑书"The Elements of Logic" : ，有这样的用法。 他这麽用, 我猜, 是建立在两个假设上: 1. 这里的系统是古典逻辑(classical logic), 而古典逻辑我们知道是完备的。 2. 这系统含有某种类似於cut theorem的meta-theorem (或structure theorem)。 把它符号化後, 这两个假设分别是: 1. 若p是tautology, 则 |- p; 2. 若 Γ |- p 且 Γ, p |- q, 则 Γ |- q。 作为基本逻辑的教科书, 或许作者不会把这两个 "meta-theorem"加以证明, 不过他的确是应该交待一下, 引入恒真句作为前提, 我们会需要这两个定理成立, 而1.在很多系统中不成立是大家都知道的(如: 代数系统, 某些二阶逻辑等等), 而2.虽然作为structure theorem在大部份的proof theory都会成立, 但在很多proof theory之中是需要假设它来characterise一个proof的概念是什麽。 而虽然intuistic logic在Kripke semantics下是完备的(我应该没记错), 但提到intuistic logic是一个直接可以指出在证明中引入 R v ~R 可能会有的问题。 : 虽然我没办法举出有哪些逻辑学家这样用，但是我们其实也是这样在做推论的。 : 当我们知道一个断言会导出矛盾的时候，我们就会说那断言不成立。例如怀疑论 : 者主张：「我什麽都不知道」，则有人马上会回应：「那对於『你什麽都不知道』 : 的这件事情你知不知道呢？如果不知道的话，那你说出的话则无意义，如果你知 : 道的话，则你就不是什麽都不知道，你至少知道了一件事情。」 : 我举的例子可能形式上不太吻合，也请大家不要去深究那个例子，否则便是 : 离题。我想说的是，我们的确会这样在思考，下列以"P"&"Q"表有真假可言 : 的陈述，箭头表若则符号。 : 主张P会导出矛盾，我们便会说主张P不成立，符号化的话就是： : P→(Q&～Q) : ∵～P : 上述我们省略了的步骤便是否定那个矛盾句，矛盾句的否定就是恒真句， : 然後再用否定後件则否定前件的规则，我们平常就是这样在思考的，而形 : 式逻辑便是在明示出我们如何思考，若我们平日就是这样在推论的，怎麽 : 可能符号化後就不能这样做推论呢？当我们平常在说：「这样矛盾」的时 : 候，我们的意思也蕴含了怎麽样做才不矛盾，但我们有先证明这不矛盾怎 : 麽来的才开始推论吗？ 上面所讲的「主张P会导出矛盾，我们便会说主张P不成立」 或许争议比较不大, 但它并无法用来证明 (R v ~R) 会成立, 因为它只能用来证明某个东西「不成立」, 而无法证明某个东西「会成立」。 而要能够证明 (R v ~R)的, 通常是另外一个看起来类似, 但不太一样的思考过程, 即: 「主张P的否定会导出矛盾, 我们便会说P是成立的」 也就是 ~P |- (Q&～Q) 则 |- P. 这个思考过程正好就是直觉主义所不接受的 RAA证明。 因为在某种诠释下, 主张~P会导出矛盾, 是主张~P无法在这系统中被接受, 或许这表示~~P是成立的, 但这和直接宣称P是成立的, 即 P 为定理, 是不一样的。 这差别的关键也许是和negation的意义有关(在natural deduction中可以这样理解), 但在某些直觉主义者的看法中, 更是较为原初的认为RAA的理解是有问题的, 因为你只能宣称你不接受~P, 但你无法因此强迫任何人去接受P, 中间所需要的, 正是古典逻辑认为理所当然的归谬, 而直觉逻辑认为是属非建构式的理解, 而因此不能被接受。 : 另外，回应前文推文的问题。其实我们实在不需要去谈什麽定义不定义一 : 只红蚂蚁，这边请拿剃刀把它剃掉；对於S大的问题，我只说那只蚂蚁红 : 色的部份就不会是黑色的，那只蚂蚁黑色的部份就不会是红色的。你也许 : 会说这是废话，但对於这个问题的回答也就只能这样。 --

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