{- Computer Aided Formal Reasoning (G53CFR, G54CFR) Thorsten Altenkirch Exercise 4: Predicate Logic (19/2/09) Deadline: 26/2/09, 12:00 Use the coursework submission (id: 267)) system to submit the coursework after demonstrating it in the lab to me or Darin. Prove the following propositions of predicate logic by completing the sheds { .. }. Note that not all propositions may be provable. If you think that a proposition is unprovable clearly mark this one by adding a line: -- impossible. -} module ex04 where open import l05 open import l06 open import l07 ∃∨-lem-1 : {A : Set}{P Q : A → Prp} → (∃ A λ a → P a ∨ Q a) ⇒ (∃ A λ a → P a) ∨ (∃ A λ a → Q a) ∃∨-lem-1 (a , d) with d ∃∨-lem-1 (a , d) | left pa = left (a , pa) ∃∨-lem-1 (a , d) | right qa = right (a , qa) ∃∨-lem-2 : {A : Set}{P Q : A → Prp} → (∃ A λ a → P a) ∨ (∃ A λ a → Q a) ⇒ (∃ A λ a → P a ∨ Q a) ∃∨-lem-2 (left (a , pa)) = a , left pa ∃∨-lem-2 (right (a , qa)) = a , right qa ∃∨-lem : {A : Set}{P Q : A → Prp} → (∃ A λ a → P a ∨ Q a) ⇔ (∃ A λ a → P a) ∨ (∃ A λ a → Q a) ∃∨-lem = ∃∨-lem-1 , ∃∨-lem-2 ∀∀com : {A B : Set}{R : A → B → Prp} → ∀' A (λ a → ∀' B (λ b → R a b)) ⇒ ∀' B (λ b → ∀' A (λ a → R a b)) ∀∀com f b a = f a b -- same as flip ∃∃com : {A B : Set}{R : A → B → Prp} → ∃ A (λ a → ∃ B (λ b → R a b)) ⇒ ∃ B (λ b → ∃ A (λ a → R a b)) ∃∃com (a , (b , p)) = b , (a , p) ∀∃com : {A B : Set}{R : A → B → Prp} → ∀' A (λ a → ∃ B (λ b → R a b)) ⇒ ∃ B (λ b → ∀' A (λ a → R a b)) ∀∃com = {!!} -- impossible. Take A = B = {0,1} and R the equality on {0,1}. Then ∀a ∃b a=b but we don't have ∃b∀a a=b because 0≠1. -- This argument can be carried out in Agda, here using {false, true} instead of {0, 1}: data Bool : Set where false : Bool true : Bool not : Bool → Bool not true = false not false = true ¬[notb≢b] : (b : Bool) → not b ≡ b → ⊥ ¬[notb≢b] true () ¬[notb≢b] false () ∀a∃b-a≡b : ∀' Bool (λ a → ∃ Bool (λ b → a ≡ b)) ∀a∃b-a≡b a = (a , refl) ¬∀∃com[Bool,≡] : ¬(∀' Bool (λ a → ∃ Bool (λ b → a ≡ b)) ⇒ ∃ Bool (λ b → ∀' Bool (λ a → a ≡ b))) ¬∀∃com[Bool,≡] h with h ∀a∃b-a≡b ... | (b , f) = ¬[notb≢b] b (f (not b)) -- This refutes the second order statement that for all sets A, B and relation R we have ∀∃com {A} {B} {R}. -- We can then derive ⊥ from ∀∃com. Therefore ∀∃com is not provable, as ⊥ is not provable. FALSE : ⊥ FALSE = ¬∀∃com[Bool,≡] ∀∃com ∃∀com : {A B : Set}{R : A → B → Prp} → ∃ B (λ b → ∀' A (λ a → R a b)) ⇒ ∀' A (λ a → ∃ B (λ b → R a b)) ∃∀com ( b , f) a = b , f a deMorgan¬∃ : {A : Set}{P : A → Prp} → ¬ (∃ A (λ x → P x)) ⇒ ∀' A (λ x → ¬ (P x)) deMorgan¬∃ ne a pa = ne (a , pa) deMorgan∀¬ : {A : Set}{P : A → Prp} → ∀' A (λ x → ¬ (P x)) ⇒ ¬ (∃ A (λ x → P x)) deMorgan∀¬ f (a , pa) = f a pa deMorgan¬∀ : {A : Set}{P : A → Prp} → ¬ (∀' A (λ x → P x)) ⇒ ∃ A (λ x → ¬ (P x)) deMorgan¬∀ = {!!} -- Impossible, else we could define deMorgan¬∧ as follows, but it is not definable (lecture 5). if₁ : {P Q : Prp} → Bool → Prp if₁ {P} {Q} true = P if₁ {P} {Q} false = Q deMorgan¬∧ : {P Q : Prp} → ¬ (P ∧ Q) ⇒ (¬ P) ∨ (¬ Q) deMorgan¬∧ npq with deMorgan¬∀ {Bool} {if₁} (λ y → npq (y true , y false)) ... | true , np = left np ... | false , nq = right nq deMorgan∃¬ : {A : Set}{P : A → Prp} → ∃ A (λ x → ¬ (P x)) ⇒ ¬ (∀' A (λ x → P x)) deMorgan∃¬ (a , npa) f = npa (f a)