{- Computer Aided Formal Reasoning (G53CFR, G54CFR) Thorsten Altenkirch Lecture 5: Propositional logic In this lecture we start to use Agda as a proof assistant. We define the basic propositional connectives using the Curry-Howard-Isomorphism: we identify a proposition with the set of its proofs, i.e. we set Prop = Set. This is in contrast with the classical identification of Prop = Bool. The latter doesn't really work in a constructive setting, since we would expect that every P : Prop reduces to either true or false. But there is no way to do this since there are many propositions of which we don't know wether they are true or false. -} module l05 where {- we identify Prop and Set, Prop is already reserved in Agda hence we use Prp instead. -} Prp : Set₁ Prp = Set {- implication (⇒ = \=>) We interpret implication by function space. The idea is that we know that P ⇒ Q is true if we have a function transforming proofs of P into proofs of Q. -} _⇒_ : Prp → Prp → Prp P ⇒ Q = P → Q infixr 0 _⇒_ {- We prove a very simple tautology: -} I : {P : Prp} → P ⇒ P I p = p {- conjunction (∧ = \and) A proof of P ∧ Q is a pair of proofs one of P and one of Q. -} data _∧_ (P Q : Prp) : Prp where _,_ : P → Q → P ∧ Q infixr 2 _∧_ {- a simple tautology: ∧ is commutative. Why don't we have to prove the other direction? -} ∧-comm : {P Q : Prp} → P ∧ Q ⇒ Q ∧ P ∧-comm (p , q) = q , p {- disjunction ∨ = \or A proof of P ∨ Q is either a proof of P prefixed with left or a proof of Q prefixed with right. -} data _∨_ (P Q : Prp) : Prp where left : P → P ∨ Q right : Q → P ∨ Q infixr 1 _∨_ {- we show that ∨ is commutative -} ∨-comm : {P Q : Prp} → P ∨ Q ⇒ Q ∨ P ∨-comm (left p) = right p ∨-comm (right q) = left q {- Prove distributivity of ∧ over ∨ -} distrib-∧-∨-1 : {P Q R : Prp} → P ∧ (Q ∨ R) ⇒ (P ∧ Q) ∨ (P ∧ R) distrib-∧-∨-1 (p , left q) = left (p , q) distrib-∧-∨-1 (p , right r) = right (p , r) {- I leave the other direction as an exercise -} {- distrib-∧-∨-2 : {P Q R : Prp} → (P ∧ Q) ∨ (P ∧ R) ⇒ P ∧ (Q ∨ R) distrib-∧-∨-2 pqr = {!!} -} {- Logical equivalence (⇔ = \iff) we define ⇔ in terms of ∧ and ⇒ -} _⇔_ : Prp → Prp → Prp P ⇔ Q = (P ⇒ Q) ∧ (Q ⇒ P) infixr 0 _⇔_ {- we can combine the two lemmas above to prove the distributivity as a logical equivalence. -} {- distrib-∧-∨ : {P Q R : Prp} → P ∧ (Q ∨ R) ⇔ (P ∧ Q) ∨ (P ∧ R) distrib-∧-∨ = distrib-∧-∨-1 , distrib-∧-∨-2 -} {- True (⊤ = \top) has a trivial proof. We can view ⊤ as a special case of ∧ with no arguments. -} data ⊤ : Prp where tt : ⊤ {- False (⊥ = \bot) has no proof. We can view ⊥ as a special case of ∨ with no arguments. -} data ⊥ : Prp where {- We can show that from false everything follows ("ex falso quod libet" in latin) using the impossible pattern in Agda. -} efq : {P : Prp} → ⊥ ⇒ P efq () {- Negation (¬ = \neg) ¬ P is defined as P implies False. -} ¬ : Prp → Prp ¬ P = P ⇒ ⊥ {- Some basic facts about negation. -} contradict : {P : Prp} → ¬ (P ∧ ¬ P) contradict (p , np) = np p contrapos : {P Q : Prp} → (P ⇒ Q) ⇒ ¬ Q ⇒ ¬ P contrapos pq nq p = nq (pq p) {- Let's prove the de Morgan laws -} deMorgan¬∨ : {P Q : Prp} → ¬ (P ∨ Q) ⇒ ¬ P ∧ ¬ Q deMorgan¬∨ npq = (λ p → npq (left p)) , λ q → npq (right q) deMorgan¬∧¬ : {P Q : Prp} → (¬ P) ∧ (¬ Q) ⇒ ¬ (P ∨ Q) deMorgan¬∧¬ (np , nq) (left p) = np p deMorgan¬∧¬ (np , nq) (right q) = nq q deMorgan¬∨¬ : {P Q : Prp} → (¬ P) ∨ (¬ Q) ⇒ ¬ (P ∧ Q) deMorgan¬∨¬ (left np) (p , q) = np p deMorgan¬∨¬ (right nq) (p , q) = nq q {- The last one turns out not to be provable! deMorgan¬∧ : {P Q : Prp} → ¬ (P ∧ Q) ⇒ (¬ P) ∨ (¬ Q) deMorgan¬∧ npq = right (λ q → npq ({!!} , q)) Here is an attempt, the only choice was that we decided to say right. It is easy to see that starting with left leads to a symmetric situation. This intuitively shows that there is no way to prove deMorgan¬∧. But this doesn't mean that its negation is provable, indeed we will show that this is not the case. -} {- to be continued ... -}