Negations of existentials and universals in constructive logic

ExistentialsAndUniversals.hs

{-# language GADTs, RankNTypes, KindSignatures, PolyKinds, EmptyCase #-}
module ExistentialsAndUniversals where

-- To prove:
-- 1. ∀a.p a → ¬∃a.¬p a
-- 2. ∃a.p a → ¬∀a.¬p a
-- 3. ∀a.¬(p a) → ¬∃a.p a
-- 4. ∃a.¬(p a) → ¬∀a.p a

-- First some simple types

-- Falsehood
data Void where

-- the elimination form for false hood says that if I give you false,
-- you can conclude anything.  Absurd!
absurd :: Void -> r
absurd x = case x of {}

-- Negation of a simple proposition.  The introduction form says that
-- if I give you an a and you prove falsehood, then that's a
-- refutation of a.  The elimination form says that if you have both a
-- and a refutation of a, then you can prove falsehood (and from that
-- you can prove anything, absurd!)
newtype Not a where
  -- contra :: Not a -> a -> Void
  Not :: { contra :: a -> Void} -> Not a

-- This is enough to prove something.  If whenever a holds, b holds,
-- and if you are given a refutation of b, you can construct a
-- refutation of a.
contrapos :: (a -> b) -> Not b -> Not a
contrapos f (Not fromB) = Not (fromB . f)

-- We also need negation of a predicate.
newtype Not1 (p :: k -> *) a where
  -- contra1 :: Not1 p a -> p a -> Void
  Not1 :: { contra1 :: (p a) -> Void } -> Not1 p a

-- We can prove double negation introductions for both Not and Not1
-- if you have a proof of a, you have a refutation of Not a.

dni :: a -> Not (Not a)
dni x = Not (\notX -> contra notX x)

-- and also for predicates - if you have that p holds of a, you have a refutation of Not1 p a

dni1 :: p a -> Not1 (Not1 p) a
dni1 x = Not1 (\notX -> contra1 notX x)

-- Now let's add existential and universal quantification

-- The elimination for All p says if you pick an a, p holds of it.
-- Conversely, to introduce an All p you have to give it a function that will for any a give back a (p a).
newtype All (p :: k -> *) where
  -- elimAll :: All p -> p a
  All :: { elimAll :: (forall a . p a)} -> All p

-- Existentials work the other way around.  If you have a (p a) you
-- can make an Ex p
data Ex (p :: k -> *) where
  Ex :: p a -> Ex p

-- we don't really need the elim for (we will use pattern matching
-- directly), but if you have an (Ex p) and you have a function that
-- whenever it's given an a and a (p a) it produces some result, you
-- can produce that result.
elimEx :: (forall a . p a -> r) -> Ex p -> r
elimEx cont (Ex p) = cont p

-- Both All p and Ex p let you change the predicate under the
-- quantifier provided that you have a way of changing it that works
-- for all possible a's.  That is, they're functors in * -> *

class Functor1 alpha where
  fmap1 :: (forall a . p a -> q a) -> alpha p -> alpha q

instance Functor1 Ex where
  fmap1 phi (Ex p) = Ex (phi p)

instance Functor1 All where
  fmap1 phi (All p) = All (phi p)

-- back to proving things.

-- As is well known, double negation elimination doesn't hold in constructive logic.
-- If you have a refutation of Not a, you can't turn that into a construction of a.

-- But interestingly, triple negation elimination does work.
-- If you have a refutation of Not (Not a), then you have a refutation of a:
-- Suppose someone gives you an a - by double negation introduction you can turn it into Not (Not a)
-- But you have a refutation of Not (Not a) in hand, so you can construct a contradiction.

tne :: Not (Not (Not a)) -> Not a
tne nnnX = Not (\x -> contra nnnX (dni x))

-- And the same thing with predicates

tne1 :: Not1 (Not1 (Not1 p)) a -> Not1 p a
tne1 nnnX = Not1 (\x -> contra1 nnnX (dni1 x))

-- And we can combine double negation introduction with the
-- contrapositive to get a sort of tripe negation elimination under an
-- existential
--
-- Ex p -> Ex (Not1 (Not1 p))
-- and therefore
-- Not (Ex (Not1 (Not1 p))) -> Not (Ex p)
tneEx :: Not (Ex (Not1 (Not1 p))) -> Not (Ex p)
tneEx = tneF1

-- and the same thing for universal quantification with the same proof
tneAll :: Not (All (Not1 (Not1 p))) -> Not (All p)
tneAll = tneF1

-- actually we can just do the proof once for all functors in * -> *

tneF1 :: Functor1 alpha => Not (alpha (Not1 (Not1 p))) -> Not (alpha p)
tneF1 = contrapos (fmap1 dni1)

-- ok and now let's do some actual logic

-- If there's an a such that (p a) holds, then it's not the case that for every a,  Not1 p a holds.
existNotAllNot :: Ex p -> Not (All (Not1 p))
existNotAllNot (Ex withEx) = Not (\(All withAll) -> contra1 withAll withEx)

-- If for every a, (p a) holds, then it's not the case that there exists some a for which Not1 p a holds.
allNotExistNot :: All p -> Not (Ex (Not1 p))
allNotExistNot (All withP) = Not (\(Ex notP) -> contra1 notP withP)

-- If for every a, Not1 p a holds, then there doesn't exist some a for which (p a) holds
allNotNotExist :: All (Not1 p) -> Not (Ex p)
allNotNotExist allNot = tneEx (allNotExistNot allNot)

-- If there exists some a for which Not1 p a holds, then it's not the case that for every a, p a holds.
existNotNotAll :: Ex (Not1 p) -> Not (All p)
existNotNotAll exNot = tneAll (existNotAllNot exNot)

-- But actually, for the last two, there's a more direct way. The last two are contrapositives of the first two

allNotNotExist' :: All (Not1 p) -> Not (Ex p)
allNotNotExist' allNot = contrapos existNotAllNot (dni allNot)

existNotNotAll' :: Ex (Not1 p) -> Not (All p)
existNotNotAll' exNot = contrapos allNotExistNot (dni exNot)


-- That's all