Докажите теорему транспонирования

Я доказываю некоторые теоремы в пропозициональной логике.

Говорит, 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 используется для принятия аксиомы без доказательства

admit :: p
admit = admit

Теперь у меня возникают проблемы с доказательством теоремы транспонирования:

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

который состоит из двух частей:

слева направо:

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

справа налево:

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

Я уже доказал 1-ю часть с Modus tollens, но не смог найти способ для 2-й части:

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

Ответ 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), в доказательство двойного отрицания. Мы можем применить ЛЕМ для получения 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)