作者MathTurtle (恩典)
看板logic
标题Re: [请益] P→((-P or Q)→Q)
时间Tue Jun 14 18:15:48 2011
仔细想一想之後发现一些很让我困惑的东西,
主要就是到底在自然演译法当中, 如果不用 '-> - introduction'
(或等价的 CP，或 deductive theorem)
我们会有哪些东西证不出来呢?
其中一点是, 如果我们有 Impl (即: (~P v Q) -||- (P ->Q) )
那麽好像并不难, 因为我们可以把 '->' 的推论规则都用 'v' 来取代。
不过 Impl 一般而言并不是 primitive 的推论规则,
而如果要证明 Impl 的话好像一定要用到 if-introduction 之类的规则。
我稍微在网上查了一下资料,
好像在 Quantum logic 里面 deductive theorem 是不成立的,
它相应的差异包括了类似於原 po 问的那个 [P & (~P v Q)] -> Q
也是不成立的, 而有趣的是, 在quantum logic里面
我们必须要假设 (P->Q) 才能推出 [P & (~P v Q)] -> Q
另外一个似乎会 fail 的就是 Impl.
也就是说似乎在 Quantum logic里面, (P->Q) 不是等价於 (~P v Q),
而是等价於一个比较复杂一点的, 即
(P->Q) -||- ~P v (P & Q).
而这使得上述用了Impl的论证, 在一个 if-intro 规则会 fail 的系统中,
似乎是无法推的过去。
不过我并没有想的很清楚,
我对 Quantum logic 的了解不是很深入, 所以上面讲的有可能是错的,
不过觉得这里面似乎有许多好玩的东西可以去研究一下。
有兴趣的人不妨找来玩一玩。
--
※ 发信站: 批踢踢实业坊(ptt.cc)
◆ From: 86.30.200.58
※ 编辑: MathTurtle 来自: 86.30.200.58 (06/14 18:18)
1F：推 Yures:都用 "V" 来推的问题是 V 引入规则 (其实就是 Add) 必须存在 06/14 18:26
2F：→ Yures:某个前提，而不能在毫无前提的状况下引入 V 吧？ 06/14 18:27
3F：→ Yures:除非这个系统允许直接写下某些语句，其实就是公设啦。 06/14 18:27
4F：→ Yures:可是自然演绎法就是个只有规则、缺乏公设的方法所以... 06/14 18:28
5F：→ MathTurtle:对...没错....有RAA的话就可以, 但RAA也是CP的一种变型 06/14 18:29
6F：→ MathTurtle:然後你讲的这个也是我正在想的, 就是CP的特殊性在於可 06/14 18:31
7F：→ MathTurtle:以让你引入某个前提然後再 discharge, 而这一步骤似乎 06/14 18:32
8F：→ MathTurtle:正是 quantum logic 要反对的 (在某种诠释之下) 06/14 18:32
9F：→ MathTurtle:不过我头脑现在一团糊...愈讲愈不清楚 XD 06/14 18:33