Chapter 3: Exercises

Prove the following identities, replacing the "sorry" placeholders with actual proofs.

variable (
p: Prop
p 
q: Prop
q 
r: Prop
r : 
Prop: Type
Prop)

-- commutativity of ∧ and ∨
example: ∀ (p q : Prop), p ∧ q ↔ q ∧ p
example
Warning: declaration uses 'sorry' : 
p: Prop
p ∧ 
q: Prop
q ↔ 
q: Prop
q ∧ 
p: Prop
p := 
sorry: p ∧ q ↔ q ∧ p
sorry
example: ∀ (p q : Prop), p ∨ q ↔ q ∨ p
example
Warning: declaration uses 'sorry' : 
p: Prop
p ∨ 
q: Prop
q ↔ 
q: Prop
q ∨ 
p: Prop
p := 
sorry: p ∨ q ↔ q ∨ p
sorry

-- associativity of ∧ and ∨
example: ∀ (p q r : Prop), (p ∧ q) ∧ r ↔ p ∧ q ∧ r
example
Warning: declaration uses 'sorry' : (
p: Prop
p ∧ 
q: Prop
q) ∧ 
r: Prop
r ↔ 
p: Prop
p ∧ (
q: Prop
q ∧ 
r: Prop
r) := 
sorry: (p ∧ q) ∧ r ↔ p ∧ q ∧ r
sorry
example: ∀ (p q r : Prop), (p ∨ q) ∨ r ↔ p ∨ q ∨ r
example
Warning: declaration uses 'sorry' : (
p: Prop
p ∨ 
q: Prop
q) ∨ 
r: Prop
r ↔ 
p: Prop
p ∨ (
q: Prop
q ∨ 
r: Prop
r) := 
sorry: (p ∨ q) ∨ r ↔ p ∨ q ∨ r
sorry

-- distributivity
example: ∀ (p q r : Prop), p ∧ (q ∨ r) ↔ p ∧ q ∨ p ∧ r
example
Warning: declaration uses 'sorry' : 
p: Prop
p ∧ (
q: Prop
q ∨ 
r: Prop
r) ↔ (
p: Prop
p ∧ 
q: Prop
q) ∨ (
p: Prop
p ∧ 
r: Prop
r) := 
sorry: p ∧ (q ∨ r) ↔ p ∧ q ∨ p ∧ r
sorry
example: ∀ (p q r : Prop), p ∨ q ∧ r ↔ (p ∨ q) ∧ (p ∨ r)
example
Warning: declaration uses 'sorry' : 
p: Prop
p ∨ (
q: Prop
q ∧ 
r: Prop
r) ↔ (
p: Prop
p ∨ 
q: Prop
q) ∧ (
p: Prop
p ∨ 
r: Prop
r) := 
sorry: p ∨ q ∧ r ↔ (p ∨ q) ∧ (p ∨ r)
sorry

-- other properties
example: ∀ (p q r : Prop), p → q → r ↔ p ∧ q → r
example
Warning: declaration uses 'sorry' : (
p: Prop
p → (
q: Prop
q → 
r: Prop
r)) ↔ (
p: Prop
p ∧ 
q: Prop
q → 
r: Prop
r) := 
sorry: p → q → r ↔ p ∧ q → r
sorry
example: ∀ (p q r : Prop), p ∨ q → r ↔ (p → r) ∧ (q → r)
example
Warning: declaration uses 'sorry' : ((
p: Prop
p ∨ 
q: Prop
q) → 
r: Prop
r) ↔ (
p: Prop
p → 
r: Prop
r) ∧ (
q: Prop
q → 
r: Prop
r) := 
sorry: p ∨ q → r ↔ (p → r) ∧ (q → r)
sorry
example: ∀ (p q : Prop), ¬(p ∨ q) ↔ ¬p ∧ ¬q
example
Warning: declaration uses 'sorry' : ¬(
p: Prop
p ∨ 
q: Prop
q) ↔ ¬
p: Prop
p ∧ ¬
q: Prop
q := 
sorry: ¬(p ∨ q) ↔ ¬p ∧ ¬q
sorry
example: ∀ (p q : Prop), ¬p ∨ ¬q → ¬(p ∧ q)
example
Warning: declaration uses 'sorry' : ¬
p: Prop
p ∨ ¬
q: Prop
q → ¬(
p: Prop
p ∧ 
q: Prop
q) := 
sorry: ¬p ∨ ¬q → ¬(p ∧ q)
sorry
example: ∀ (p : Prop), ¬(p ∧ ¬p)
example
Warning: declaration uses 'sorry' : ¬(
p: Prop
p ∧ ¬
p: Prop
p) := 
sorry: ¬(p ∧ ¬p)
sorry
example: ∀ (p q : Prop), p ∧ ¬q → ¬(p → q)
example
Warning: declaration uses 'sorry' : 
p: Prop
p ∧ ¬
q: Prop
q → ¬(
p: Prop
p → 
q: Prop
q) := 
sorry: p ∧ ¬q → ¬(p → q)
sorry
example: ∀ (p q : Prop), ¬p → p → q
example
Warning: declaration uses 'sorry' : ¬
p: Prop
p → (
p: Prop
p → 
q: Prop
q) := 
sorry: ¬p → p → q
sorry
example: ∀ (p q : Prop), ¬p ∨ q → p → q
example
Warning: declaration uses 'sorry' : (¬
p: Prop
p ∨ 
q: Prop
q) → (
p: Prop
p → 
q: Prop
q) := 
sorry: ¬p ∨ q → p → q
sorry
example: ∀ (p : Prop), p ∨ False ↔ p
example
Warning: declaration uses 'sorry' : 
p: Prop
p ∨ 
False: Prop
False ↔ 
p: Prop
p := 
sorry: p ∨ False ↔ p
sorry
example: ∀ (p : Prop), p ∧ False ↔ False
example
Warning: declaration uses 'sorry' : 
p: Prop
p ∧ 
False: Prop
False ↔ 
False: Prop
False := 
sorry: p ∧ False ↔ False
sorry
example: ∀ (p q : Prop), (p → q) → ¬q → ¬p
example
Warning: declaration uses 'sorry' : (
p: Prop
p → 
q: Prop
q) → (¬
q: Prop
q → ¬
p: Prop
p) := 
sorry: (p → q) → ¬q → ¬p
sorry

Prove the following identities, replacing the "sorry" placeholders with actual proofs. These require classical reasoning.

variable (
p: Prop
p 
q: Prop
q 
r: Prop
r : 
Prop: Type
Prop)

example: ∀ (p q r : Prop), (p → q ∨ r) → (p → q) ∨ (p → r)
example
Warning: declaration uses 'sorry' : (
p: Prop
p → 
q: Prop
q ∨ 
r: Prop
r) → ((
p: Prop
p → 
q: Prop
q) ∨ (
p: Prop
p → 
r: Prop
r)) := 
sorry: (p → q ∨ r) → (p → q) ∨ (p → r)
sorry
example: ∀ (p q : Prop), ¬(p ∧ q) → ¬p ∨ ¬q
example
Warning: declaration uses 'sorry' : ¬(
p: Prop
p ∧ 
q: Prop
q) → ¬
p: Prop
p ∨ ¬
q: Prop
q := 
sorry: ¬(p ∧ q) → ¬p ∨ ¬q
sorry
example: ∀ (p q : Prop), ¬(p → q) → p ∧ ¬q
example
Warning: declaration uses 'sorry' : ¬(
p: Prop
p → 
q: Prop
q) → 
p: Prop
p ∧ ¬
q: Prop
q := 
sorry: ¬(p → q) → p ∧ ¬q
sorry
example: ∀ (p q : Prop), (p → q) → ¬p ∨ q
example
Warning: declaration uses 'sorry' : (
p: Prop
p → 
q: Prop
q) → (¬
p: Prop
p ∨ 
q: Prop
q) := 
sorry: (p → q) → ¬p ∨ q
sorry
example: ∀ (p q : Prop), (¬q → ¬p) → p → q
example
Warning: declaration uses 'sorry' : (¬
q: Prop
q → ¬
p: Prop
p) → (
p: Prop
p → 
q: Prop
q) := 
sorry: (¬q → ¬p) → p → q
sorry
example: ∀ (p : Prop), p ∨ ¬p
example
Warning: declaration uses 'sorry' : 
p: Prop
p ∨ ¬
p: Prop
p := 
sorry: p ∨ ¬p
sorry
example: ∀ (p q : Prop), ((p → q) → p) → p
example
Warning: declaration uses 'sorry' : (((
p: Prop
p → 
q: Prop
q) → 
p: Prop
p) → 
p: Prop
p) := 
sorry: ((p → q) → p) → p
sorry

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