作者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