證明轉置理論

我在命題邏輯中證明了一些定理。證明轉置理論

說，肯定前件，其中指出，如果P蘊含Q和P是真的，那麼Q是真正

P → Q 
P 
----- 
Q

將在Haskell被解釋爲

modus_ponens :: (p -> q) -> p -> q 
modus_ponens pq p = pq p

您可能會發現它與類型相當於定理和程序相當於證明。

邏輯和

data p \/ q = Left p 
      | Right q

邏輯與

data p /\ q = Conj p q

當且僅當

type p <-> q = (p -> q) /\ (q -> p)

承認是假設一個公理沒有證據

admit :: p 
admit = admit

現在我無法證明換位定理：

(P → Q) ↔ (¬Q → ¬P)

它由兩個部分組成：

左至右：

P → Q 
¬Q 
----- 
¬P

從右至左：

¬Q → ¬P 
P 
------- 
Q

我已經證明了第一個pa RT與Modus tollens，但不能用於第二部分想出一個辦法：

transposition :: (p -> q) <-> (Not q -> Not p) 
transposition = Conj left_right right_left 
       where left_right p_q not_q = modus_tollens p_q not_q 
         right_left = admit 

modus_tollens :: (p -> q) -> Not q -> Not p 
modus_tollens pq not_q = \p -> not_q $ pq p 

double_negation :: p <-> Not (Not p) 
double_negation = Conj (\p not_p -> not_p p) admit

看來，它可以作爲寫：

(¬Q) → (¬P) 
¬(¬P) 
----------- 
¬(¬Q)

但我不知道該怎麼做了否定（也許雙重否定）在這個系統。

有人可以幫我嗎？

總計劃：

{-# LANGUAGE TypeOperators  #-} 
{-# LANGUAGE GADTs    #-} 
{-# LANGUAGE NoImplicitPrelude #-} 
{-# LANGUAGE PolyKinds   #-} 
{-# LANGUAGE DataKinds   #-} 
{-# LANGUAGE TypeFamilies   #-} 
{-# OPTIONS_GHC -fwarn-incomplete-patterns #-} 

import Prelude (Show(..), Eq(..), ($), (.), flip) 

-- Propositional Logic -------------------------------- 

-- False, the uninhabited type 
data False 

-- Logical Not 
type Not p = p -> False 

-- Logical Disjunction 
data p \/ q = Left p 
      | Right q 

-- Logical Conjunction 
data p /\ q = Conj p q 

-- If and only if 
type p <-> q = (p -> q) /\ (q -> p) 

-- Admit is used to assume an axiom without proof 
admit :: p 
admit = admit 

-- There is no way to prove this axiom in constructive logic, therefore we 
-- leave it admitted 
excluded_middle :: p \/ Not p 
excluded_middle = admit 

absurd :: False -> p 
absurd false = admit 

double_negation :: p <-> Not (Not p) 
double_negation = Conj (\p not_p -> not_p p) admit 

modus_ponens :: (p -> q) -> p -> q 
modus_ponens = ($) 

modus_tollens :: (p -> q) -> Not q -> Not p 
modus_tollens pq not_q = \p -> not_q $ pq p 

transposition :: (p -> q) <-> (Not q -> Not p) 
transposition = Conj left_right right_left 
       where left_right = modus_tollens 
         right_left = admit

來源

2016-10-04 Wentao

從技術上說，'modus_ponens'將有型'（P - > Q，P） - > q'（或你的'（P - > q）/ \ p - > q'），但顯然你的定義是通過currying等價的。 –

當你在這種情況下陷入困境時，有可能你找到了一種不是直覺主義的古典重言式。在這種情況下，一個可能的策略開始在某些（可能是所有）命題變量上應用'excluded_middle'。如果全部完成，這基本上等於構建完整的真值表 - 效率低下，無聊但有效。 – chi

你理所當然地注意到，

-- There is no way to prove this axiom in constructive logic, therefore we 
-- leave it admitted 
excluded_middle :: p \/ Not p 
excluded_middle = admit

事實上，當加入到建設性的邏輯，以下是等價的公理：

法Excluded Middle
雙重否定
對換句法（你叫什麼換位定理）
皮爾士定律

因此，你需要用你已經承認公理（LEM的）你雙重否定的證明。我們可以申請LEM獲得p \/ Not p。然後，在這個分解中應用個案。在Left p的情況下，很容易顯示Not (Not p) -> p。在Right q的情況下，我們使用Not (Not p)來達到False，從中我們可以得出結論p。

要機智，這就是你缺少的部分：

double_negation_rev :: Not (Not p) -> p 
double_negation_rev = \nnp -> case excluded_middle of 
    Left p -> p 
    Right q -> absurd (nnp q)

來源

2016-10-04 02:57:39

證明轉置理論

回答

相關問題