Re: [請益] P→((-P or Q)→Q)

看板logic作者MathTurtle (恩典)時間14年前 (2011/06/14 18:15)推噓1(1推 0噓 8→)

留言9則, 2人參與討論串4/4 (看更多)

仔細想一想之後發現一些很讓我困惑的東西, 主要就是到底在自然演譯法當中, 如果不用 '-> - 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)

推

Yures

06/14 18:26, , 1^F

06/14 18:26, 1^F

→

Yures

06/14 18:27, , 2^F

06/14 18:27, 2^F

→

Yures

06/14 18:27, , 3^F

06/14 18:27, 3^F