@@ -0,0 +1,161 @@
1+module Data.Logic.Propositional
2+
3+%default total
4+%access public export
5+
6+-- Idris uses intuitionistic logic, so it does not validate the
7+-- principle of excluded middle (PEM) or similar theorems of classical
8+-- logic. But it does validate certain relations among these
9+-- propositions, and that's what's in this file.
10+
11+||| The principle of excluded middle
12+PEM : Type -> Type
13+PEM p = Either p (Not p)
14+
15+||| Double negation elimination
16+DNE : Type -> Type
17+DNE p = Not $ Not p -> p
18+
19+||| The consensus theorem (at least, the interesting part)
20+Consensus : Type -> Type -> Type -> Type
21+Consensus p q r = (q, r) -> Either (p, q) (Not p, r)
22+
23+||| Peirce's law
24+Peirce : Type -> Type -> Type
25+Peirce p q = ((p -> q) -> p) -> p
26+
27+||| Not sure if this one has a name, so call it Frege's law
28+Frege : Type -> Type -> Type -> Type
29+Frege p q r = (p -> r) -> (q -> r) -> ((p -> q) -> q) -> r
30+
31+||| The converse of contraposition: (p -> q) -> Not q -> Not p
32+Transposition : Type -> Type -> Type
33+Transposition p q = (Not q -> Not p) -> p -> q
34+
35+||| This isn't a good name.
36+Switch : Type -> Type
37+Switch p = (Not p -> p) -> p
38+
39+-- PEM and the others can't be proved outright, but it is possible to
40+-- prove the double negations (DN) of all of them.
41+
42+||| The double negation of a proposition
43+DN : Type -> Type
44+DN p = Not $ Not p
45+
46+pemDN : DN $ PEM p
47+pemDN f = f $ Right $ \x => f $ Left x
48+
49+dneDN : DN $ DNE p
50+dneDN f = f $ \g => void $ g $ \x => f $ \_ => x
51+
52+consensusDN : DN $ Consensus p q r
53+consensusDN f = f $ \(y, z) => Right (\x => f $ \(_, _) => Left (x, y), z)
54+
55+peirceDN : DN $ Peirce p q
56+peirceDN f = f $ \g => g $ \x => void $ f $ \_ => x
57+
58+fregeDN : DN $ Frege p q r
59+fregeDN f = f $ \g, h, i => h $ i $ \x => void $ f $ \_, _, _ => g x
60+
61+transpositionDN : DN $ Transposition p q
62+transpositionDN f = f $ \g, x => void $ g (\y => f $ \_, _ => y) x
63+
64+switchDN : DN $ Switch p
65+switchDN f = f $ \g => g $ \x => f $ \_ => x
66+
67+-- It's easy to prove all these theorems assuming PEM.
68+
69+dnePEM : PEM p -> DNE p
70+dnePEM (Left l) _ = l
71+dnePEM (Right r) f = void $ f r
72+
73+consensusPEM : PEM p -> Consensus p q r
74+consensusPEM (Left l) (y, _) = Left (l, y)
75+consensusPEM (Right r) (_, z) = Right (r, z)
76+
77+peircePEM : PEM p -> Peirce p q
78+peircePEM (Left l) _ = l
79+peircePEM (Right r) f = f $ \x => void $ r x
80+
81+fregePEM : PEM p -> Frege p q r
82+fregePEM (Left l) f _ _ = f l
83+fregePEM (Right r) _ g h = g $ h $ \x => void $ r x
84+
85+transpositionPEM : PEM p -> Transposition q p
86+transpositionPEM (Left l) _ _ = l
87+transpositionPEM (Right r) f x = void $ f r x
88+
89+switchPEM : PEM p -> Switch p
90+switchPEM (Left l) _ = l
91+switchPEM (Right r) f = f r
92+
93+-- It's trivial to prove these theorems assuming double negation
94+-- elimination (DNE), since their double negations can all be proved.
95+
96+||| Eliminate double negations
97+EDN : DN p -> DNE p -> p
98+EDN f g = g f
99+
100+pemDNE : DNE $ PEM p -> PEM p
101+pemDNE = EDN pemDN
102+
103+-- It's possible to prove the theorems assuming Peirce's law, but some
104+-- thought must be given to choosing the right instances. Peirce's law
105+-- is therefore weaker than PEM on an instance-by-instance basis, but
106+-- all the instances together are equivalent.
107+
108+pemPeirce : Peirce (PEM p) Void -> PEM p
109+pemPeirce f = f $ \g => Right $ \x => g $ Left x
110+
111+dnePeirce : Peirce p Void -> DNE p
112+dnePeirce f g = f $ \h => void $ g h
113+
114+consensusPeirce : Peirce (Consensus p q r) Void -> Consensus p q r
115+consensusPeirce f (y, z) =
116+ f (\g, (_, _) => Right (\x => g (\_ => Left (x, y)), z)) (y, z)
117+
118+fregePeirce : Peirce (Frege p q r) Void -> Frege p q r
119+fregePeirce f g h i =
120+ f (\j, _, _, _ => h $ i $ \x => void $ j $ \_, _, _ => g x) g h i
121+
122+transpositionPeirce : Peirce (Transposition p q) Void -> Transposition p q
123+transpositionPeirce f g x =
124+ f (\h, _, _ => void $ g (\y => h $ \_, _ => y) x) (\j, _ => g j x) x
125+
126+-- There are a variety of single axioms sufficient for deriving all of
127+-- classical logic. The earliest of these is known as Nicod's axiom,
128+-- but it is written using only nand operators and doesn't lend itself
129+-- to Idris's type system. Meredith's axiom, on the other hand, is
130+-- written using implication and negation.
131+
132+||| Meredith's axiom, sufficient for deriving all of classical logic
133+Meredith : (p, q, r, s, t : Type) -> Type
134+Meredith p q r s t =
135+ ((((p -> q) -> Not r -> Not s) -> r) -> t) -> (t -> p) -> s -> p
136+
137+-- The Meredith axiom implies all of classical logic, and so in
138+-- particular it implies PEM, and therefore cannot be proved in
139+-- intuitionistic logic. As usual, however, its double negation can be
140+-- proved.
141+
142+meredithDN : DN $ Meredith p q r s t
143+meredithDN f =
144+ f $ \g, h, x =>
145+ h $ g $ \i =>
146+ void $ i
147+ (\y => void $ f $ \_, _, _ => y)
148+ (\z => f $ \_, _, _ => h $ g $ \_ => z)
149+ x
150+
151+-- Meredith can be proved assuming PEM, since the type system itself
152+-- takes care of the rest.
153+
154+meredithPEM : PEM p -> Meredith p q r s t
155+meredithPEM (Left l) _ _ _ = l
156+meredithPEM (Right r) f g x =
157+ g $ f $ \h =>
158+ void $ h
159+ (\y => void $ r y)
160+ (\z => r $ g $ f (\_ => z))
161+ x