Prove the Transposition Theorem

Question

I'm proving some theorems in Propositional Logic.

Says, Modus Ponens, which states that if P implies Q and P is true, then Q is true

P → Q
P
-----
Q

would be interpreted in Haskell as

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

You might find it types are equivalent to theorems and programs are equivalent to proofs.

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

Now I am having trouble proving the Transposition Theorem:

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

which consists of 2 parts:

left to right:

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

right to left:

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

I already proved the 1st part with Modus tollens but couldn't figure out a way for 2nd part:

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

It seems that it could write as:

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

But I have no idea how to do the negation (and maybe double negation) in this system.

Could someone help me with that?

---

Total program:

{-# 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

You rightfully note that

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

In fact, the following are equivalent axioms when added to constructive logic:

• Law of Excluded Middle
• Double Negation
• Law of Contrapositive (what you've called the Transposition Theorem)
• Peirce's law

Therefore, you need to use the axiom that you've admitted (the LEM) in your proof of double negation. We may apply LEM to obtain p \/ Not p. Then, apply casework on this disjunction. In case Left p, it is easy to show Not (Not p) -> p. In case Right q, we use Not (Not p) to arrive at False, from which we can conclude p.

To wit, this is the part you're missing:

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