haskell - 证明转置定理

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)