{- Computer Aided Formal Reasoning (G53CFR, G54CFR) Thorsten Altenkirch Lecture 6: Classical principles In this lecture we are exploring principles which follow from the classical identification of Prop and Bool. -} module l06 where open import l05 -- we are going to use the definitions from the previous lecture {- we start with a warm up: proving the basic combinators of combinatory logic -} K : {P Q : Prp} → P ⇒ Q ⇒ P -- K = λ p → λ q → p K p q = p S : {P Q R : Prp} → (P ⇒ Q ⇒ R) ⇒ (P ⇒ Q) ⇒ (P ⇒ R) S = λ pqr → λ pq → λ p → pqr p (pq p) {- S, K are universal for propositional logic with ⇒ only. That means we can prove any provable proposition just containing ⇒ just by combining S and K. As an example we prove I (there is just a minor glitch that we have to instatiate a propositional variable explicitely. -} II : {P : Prp} → P ⇒ P II {P} = S K (K {Q = ⊤}) {- Combinatory logic can also be extended to the other connectives. An example is orcase a basic combinator for disjunction. -} orcase : {P Q R : Prp} → (P ⇒ R) ⇒ (Q ⇒ R) ⇒ (P ∨ Q ⇒ R) orcase pr qr (left p) = pr p orcase pr qr (right q) = qr q {- We noticed in the previous lecture that the last de Morgan law is not provable: deMorgan¬∧ : {P Q : Prp} → ¬ (P ∧ Q) ⇒ (¬ P) ∨ (¬ Q) deMorgan¬∧ npq = right (λ q → npq ({!!} , q)) Here are some other troublesome tautologies: -} {- TND = tertium non datur (excluded middle) states that every proposition is either true or false. It clearly expresses the idea that Prop = Bool. -} TND : Set₁ TND = {P : Prp} → P ∨ ¬ P {- Any attempt to prove TND fails quickly. How would we know wether P is true or false without even looking at it. Actually even if we were allowed to look at it, we don't know for every proposition wether it is true or false once we have introduced predicate logic. tnd : TND tnd = {!!} -} {- RAA = reductio ad absurdum (proof by contradiction) states that to prove P it is enough to show that assuming ¬ P leades to a contradiction. We can conviniently represent this using double negation: -} ¬¬ : Prp → Prp ¬¬ P = ¬ (¬ P) RAA : Set₁ RAA = {P : Prp} → ¬¬ P ⇒ P {- An attempt to prove RAA quickly leads to an infinite regress... raa : {P : Prp} → ¬¬ P ⇒ P raa = λ nnp → efq (nnp (λ p → nnp {!!})) -} {- note that the other direction is fine: -} raainv : {P : Prp} → P ⇒ ¬¬ P raainv p np = np p {- As another example we investigate the definition of ⇒ in terms of ∨ and ¬, namely P => Q ⇔ ¬ P ∨ Q. We try to prove both direction of this equivalence: -} ⇒lem-1 : {P Q : Prp} → ¬ P ∨ Q ⇒ (P ⇒ Q) ⇒lem-1 (left np) p = efq (np p) ⇒lem-1 (right q) p = q {- this one is fine, what about the other ? -} {- ⇒lem-2 : {P Q : Prp} → (P ⇒ Q) ⇒ ¬ P ∨ Q ⇒lem-2 pq = {!!} any attempt fails. -} {- Going back to TND, we can't prove it but can we prove that we can't prove it? To the contrary, we can prove that it is not the case that we cannot prove it. :-) I mean we can prove the double negation of TND : -} ¬¬tnd : {P : Prp} → ¬¬ (P ∨ ¬ P) ¬¬tnd npnp = npnp (right (λ p → npnp (left p))) {- I illustrated this proof with a little fairy tale involving time travel... -} {- A consequene is that RAA proves TND. -} RAA→TND : RAA → TND RAA→TND raa = raa ¬¬tnd {- I leave the other direction for homework: TND → RAA TND→RND = {!!} and also the double negation of the last deMorgan law: ¬¬deMorgan¬∧ : {P Q : Prp} → ¬ (P ∧ Q) ⇒ ¬¬ ((¬ P) ∨ (¬ Q)) ¬¬deMorgan¬∧ = {!!} -}