Avigad.Chapter3

Propositions and Proofs

Exercise 1

Prove the following identities.

theorem Avigad.Chapter3.ex1.and_comm' (p : Prop) (q : Prop) : p ∧ q ↔ q ∧ p

theorem Avigad.Chapter3.ex1.or_comm' (p : Prop) (q : Prop) : p ∨ q ↔ q ∨ p

theorem Avigad.Chapter3.ex1.and_assoc (p : Prop) (q : Prop) (r : Prop) : (p ∧ q) ∧ r ↔ p ∧ q ∧ r

theorem Avigad.Chapter3.ex1.or_assoc' (p : Prop) (q : Prop) (r : Prop) : (p ∨ q) ∨ r ↔ p ∨ q ∨ r

theorem Avigad.Chapter3.ex1.and_or_left (p : Prop) (q : Prop) (r : Prop) : p ∧ (q ∨ r) ↔ p ∧ q ∨ p ∧ r

theorem Avigad.Chapter3.ex1.or_and_left (p : Prop) (q : Prop) (r : Prop) : p ∨ q ∧ r ↔ (p ∨ q) ∧ (p ∨ r)

theorem Avigad.Chapter3.ex1.imp_imp_iff_and_imp (p : Prop) (q : Prop) (r : Prop) : p → q → r ↔ p ∧ q → r

theorem Avigad.Chapter3.ex1.or_imp (p : Prop) (q : Prop) (r : Prop) : p ∨ q → r ↔ (p → r) ∧ (q → r)

theorem Avigad.Chapter3.ex1.nor_or (p : Prop) (q : Prop) : ¬(p ∨ q) ↔ ¬p ∧ ¬q

theorem Avigad.Chapter3.ex1.not_and_or_mpr (p : Prop) (q : Prop) : ¬p ∨ ¬q → ¬(p ∧ q)

theorem Avigad.Chapter3.ex1.and_not_self (p : Prop) : ¬(p ∧ ¬p)

theorem Avigad.Chapter3.ex1.not_imp_o_and_not (p : Prop) (q : Prop) : p ∧ ¬q → ¬(p → q)

theorem Avigad.Chapter3.ex1.false_elim_self (p : Prop) (q : Prop) : ¬p → p → q

theorem Avigad.Chapter3.ex1.not_or_imp_imp (p : Prop) (q : Prop) : ¬p ∨ q → p → q

theorem Avigad.Chapter3.ex1.or_false_iff (p : Prop) : p ∨ False ↔ p

theorem Avigad.Chapter3.ex1.and_false_iff (p : Prop) : p ∧ False ↔ False

theorem Avigad.Chapter3.ex1.imp_imp_not_imp_not (p : Prop) (q : Prop) : (p → q) → ¬q → ¬p

Exercise 2

Prove the following identities. These require classical reasoning.

theorem Avigad.Chapter3.ex2.imp_or_mp (p : Prop) (r : Prop) (s : Prop) (hp : p) : (p → r ∨ s) → (p → r) ∨ (p → s)

theorem Avigad.Chapter3.ex2.not_and_iff_or_not (p : Prop) (q : Prop) : ¬(p ∧ q) → ¬p ∨ ¬q

theorem Avigad.Chapter3.ex2.not_imp_mp (p : Prop) (q : Prop) : ¬(p → q) → p ∧ ¬q

theorem Avigad.Chapter3.ex2.not_or_of_imp (p : Prop) (q : Prop) : (p → q) → ¬p ∨ q

theorem Avigad.Chapter3.ex2.not_imp_not_imp_imp (p : Prop) (q : Prop) : (¬q → ¬p) → p → q

theorem Avigad.Chapter3.ex2.or_not (p : Prop) : p ∨ ¬p

theorem Avigad.Chapter3.ex2.imp_imp_imp (p : Prop) (q : Prop) : ((p → q) → p) → p

Exercise 3

Prove ¬(p ↔ ¬p) without using classical logic.

theorem Avigad.Chapter3.ex3.iff_not_self (p : Prop) (hp : p) : ¬(p ↔ ¬p)