ND
1 What do propositions actually mean in logic
2 Conjunction
\[\frac{\Gamma \vdash M : A \qquad \Gamma \vdash N : B }{ \Gamma \vdash <M,N> : A \land B}\]
\[\frac{\Gamma \vdash M : A \land B}{\Gamma \vdash fst\ M : A}\]
3 Implication
\[ \frac{\Gamma, u: A \vdash M:B}{\Gamma \vdash (\lambda u: A. M): A \rightarrow B}\]
\[\frac{\Gamma \vdash M: A \rightarrow B \qquad \Gamma \vdash N: A}{\Gamma \vdash M\ N : B}\]
\[\cfrac{[A]^u}{\cfrac{...}{\cfrac{B}{A \rightarrow B}}}\]
\[\cfrac{A \rightarrow B \qquad A}{B}\]
4 Disjunction
\[\cfrac{\Gamma \vdash M : A}{\Gamma \vdash inl\ M : A \lor B}\]
\[\cfrac{\Gamma \vdash M : A \lor B \qquad \Gamma,u:A \vdash p : C \qquad \Gamma,w:B \vdash q: C}{\Gamma \vdash case\ M\ of\ (inl\ u \Rightarrow p\ |\ inr\ w \Rightarrow q): C}\]
\[ \cfrac{A\lor B \qquad \cfrac{[A]^u}{\cfrac{...}{C}} \qquad \cfrac{[B]^w}{\cfrac{...}{C}} }{C}\]
{-# LANGUAGE Rank2Types #-}
import Data.Void
import Data.Bifunctor
import Data.Functor.Identity
type Not a = a -> Void
type Peirce = forall a b. ((a -> b) -> a) -> a
type LEM = forall a. Either (Not a) a
callCC_lem :: Peirce -> LEM
callCC_lem callCC = callCC $ \cc -> Left (\a -> cc (Right a))
lem_callCC :: LEM -> Peirce
lem_callCC lem = either (\n -> \f -> f (absurd . n)) const lem
-- Bonus exercise: prove Peirce’s law <=> double negation elimination
type DNE = forall a. Not (Not a) -> a
lem_dne :: LEM -> DNE
lem_dne lem = either (\f -> \g -> absurd (g f)) const lem
dne_lem :: DNE -> LEM
dne_lem dne = dne $ \n -> n (Right . dne $ \m -> n (Left m))
callCC_dne :: Peirce -> DNE
callCC_dne callCC = \dn -> callCC $ \cc -> absurd (dn cc)
dne_callCC :: DNE -> Peirce
dne_callCC dne f = dne $ \n -> n (f . dne $ \m -> m (absurd . n))
-- Self-inflicted exercise: prove dual Frobenius rule <=> everything else
data Voider a = Voider { unVoider :: Void }
type DualFrobenius = forall x p q. (x -> Either (p x) q) -> Either (x -> p x) q
lem_df :: LEM -> DualFrobenius
lem_df lem f = bimap (\nq -> either id (absurd . nq) . f) id lem
df_lem :: DualFrobenius -> LEM
df_lem df = first (\f -> unVoider . f) (df Right)
callCC_df :: Peirce -> DualFrobenius
callCC_df callCC f = callCC $ \cc -> Left $ \x -> either id (cc . Right) (f x)
df_callCC :: DualFrobenius -> Peirce
df_callCC df f = either (\g -> f (absurd . unVoider . g)) id (df Right)
dne_df :: DNE -> DualFrobenius
dne_df dne f = dne $ \n -> n (Left $ \x -> dne $ \m -> either (m) (n . Right) (f x))
df_dne :: DualFrobenius -> DNE
df_dne df dn = either (\f -> (absurd . dn) (unVoider . f)) id (df Right)
