证明换位定理

Question

我在命题逻辑中证明了一些定理.

Modus Ponens说,如果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

我已经证明了第一部分,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

Answer 1

你理所当然地注意到了

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

实际上,当添加到构造逻辑时,以下是等价的公理:

• 排除中的法则
• 双重否定
• 对立定律(你所谓的换位定理)
• 皮尔士定律

因此,你需要在你的双重否定证明中使用你已经承认的公理(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)