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