Some statements of classical logic

ClassicalLogic.hs

-- | Some statements of classical logic
 {-# language RankNTypes, ScopedTypeVariables, EmptyDataDecls, EmptyCase, TypeApplications #-}
module ClassicalLogic where

-- | Falsehood
data Void

-- | The elimination rule for falsehood
absurd :: Void -> a
absurd void = case void of { }

-- | Negation
type Not a = a -> Void

-- | If you have a proof of a proposition and of its negation, you can
-- prove anything.
raa :: forall p a . p -> Not p -> a
raa p notp = absurd (notp p)

-- | If you have a negation of either p or q, then you can make a
-- negation of p and a negation of q.  This is true intuitionistically.
notEitherBoth :: Not (Either p q) -> (Not p, Not q)
notEitherBoth notEither = (\a -> raa (Left a) notEither, \b -> raa (Right b) notEither)


-- | The law of excluded middle: for all propositions p, either p is
-- true or its negation is.
type ExMiddle' p = Either p (Not p)
type ExMiddle = forall p . ExMiddle' p

-- | Double negation elimination: From the refuatation of the
-- refutation of p you can make a p.
type DNE' p = Not (Not p) -> p
type DNE = forall p . DNE' p

-- | The converse of DNE is intuitionistically true.
pToRefutationRefutation :: forall p . p -> Not (Not p)
pToRefutationRefutation = raa @p @Void


-- | Peirce's law. (I don't know of a way to say it other than to just
-- read off the connectives.)
type Peirce' p q = ((p -> q) -> p) -> p
type Peirce = forall p q . Peirce' p q


-- | One direction of DeMorgan's law for disjunction.
type DeMorganNotAnd' p q = Not (Not p, Not q) -> Either p q
type DeMorganNotAnd = forall p q . DeMorganNotAnd' p q

-- | The other direction of DeMorgan's law is intuitionistically
-- provable.
eitherToNotBothNot :: forall p q. Either p q -> Not (Not p, Not q)
eitherToNotBothNot pOrQ = \(notp, notq) -> case pOrQ of
                                             Left p -> raa p notp
                                             Right q -> raa q notq

-- | For a proof that p implies q to be true, either q must be true or
-- p must be false.
type ImpliesToOr' p q  = (p -> q) -> Either q (Not p)
type ImpliesToOr = forall p q . ImpliesToOr' p q

-- | If q is true or p is false, then p implies q.  This is true
-- intuitionistically.
eitherQOrNotPImpliesImplication :: Either q (Not p) -> (p -> q)
eitherQOrNotPImpliesImplication eitherQOrNotP = \p -> case eitherQOrNotP of
                                                        Left q -> q
                                                        Right notp -> raa p notp

-- | Law of excluded middle implies double negation elimination
exMiddleDNE :: forall p . ExMiddle -> DNE' p
exMiddleDNE exMid = \notnotp -> case exMid of
                                  Left p -> p
                                  Right notp -> raa notp notnotp
-- | And double negation eliminiation implies the law of excluded middle.
-- So the two are equivalent
dneExMiddle :: forall p . DNE -> ExMiddle' p
dneExMiddle dne = dne (\notEither -> case notEitherBoth notEither of
                                         (notp, notnotp) -> raa notp notnotp)

-- | Implication as disjunction implies the law of excluded middle.
impToOrToExMiddle :: forall p . ImpliesToOr -> ExMiddle' p
impToOrToExMiddle impToOr = impToOr @p id

-- | The law of excluded middle implies Implication as disjunction.
-- So implication as disjunction is equivalent to the law of excluded middle.
exMiddleImplToOr :: forall p q . ExMiddle -> ImpliesToOr' p q
exMiddleImplToOr exMiddle = \pToQ -> case exMiddle @p of
                                       Left p -> Left (pToQ p)
                                       Right notp -> Right notp

-- | DeMorgan's law of disjunction implies double negation
-- elimination.  Since DNE is equivalent to law of excluded middle,
-- DeMorgan's law of disjunction implies excluded middle.
deMorganNotAndToDNE :: forall p . DeMorganNotAnd -> DNE' p
deMorganNotAndToDNE deMorgan = \notnotp -> case deMorgan @p @p (\bothNotP -> raa (fst bothNotP) notnotp) of 
                                             Left p -> p
                                             Right p -> p

-- | Law of excluded middle implies DeMorgan's law of disjunction.
-- Together with the previous statement DeMorgan's law of disjunction
-- is equivalent to excluded middle.
exMiddleToDeMorganNotAnd :: forall p q . ExMiddle -> DeMorganNotAnd' p q
exMiddleToDeMorganNotAnd exMiddle = \notBothNot -> case exMiddle @(Either p q) of
                                                     Left eitherPQ -> eitherPQ
                                                     Right notEither -> case notEitherBoth notEither of
                                                       notPAndNotQ -> raa notPAndNotQ notBothNot

-- | Excluded middle implies Peirce's Law.
exMidToPeirce :: forall p q . ExMiddle -> Peirce' p q
exMidToPeirce exMiddle = \pqp -> case exMiddle @p of
                           Left p -> p
                           Right notp -> pqp (\p -> raa p notp)


-- | Peirce's law implies double-negation elimination.  Together with
-- all of the above, Peirce's law is equivalent to the law of excluded
-- middle (and the other 4).
peirceToDNE:: forall p . Peirce -> DNE' p
peirceToDNE peirce = \notnotp -> peirce @p @Void (\notp -> raa notp notnotp)