6. Predicate Logic (2)

24/10/22

Types: A: Type Quantifiers

• ∀ x:A, PP x forall
• ∃ x:A, PP x exists Predicates: PP: A→Prop
• A: Students
• PP x: x wears blue jeans
• QQ x: x wears a red hat

(∀ x:A, PP x ∧ QQ x) ↔ (∀ x:A, PP x) ∧ (∀ x:A, QQ x) (∃ x:A, PP x ∨ QQ x) ↔ (∃ x:A, PP x) ∨ (∃ x:A, QQ x)

	How to prove	How to use
∀ x:A, PP x	assume y,	apply h
∃ x:A, PP	exists a,	cases h with x ppx,
P → Q	assume h,	apply h,
P ∧ Q	constructor,	cases with p q,
a = b	reflectivity,	rewrite h,

variables A B C : Type
variables P Q R : Prop
variables PP QQ : A → Prop

open classical

example : (∃ x : A, PP x ∨ QQ x) ↔ (∃ x:A, PP x) ∨ (∃ x:A, QQ x) :=
begin
  constructor,
  assume h,
  cases h with a ppa,
  cases ppa with pa qa,
  left,
  existsi a,
  exact pa,
  right, 
  existsi a,
  exact qa,
  assume h,
  cases h with p q,
  cases p with a pa,
  existsi a,
  left,
  exact pa,
  cases q with a qa,
  existsi a,
  right,
  exact qa,
end

-- A is non empty ∃ x : A, true
-- A is empty     ∀ x : A, false

example : (∃ x: A, true) → (∀ x:A, PP x) → (∃ x:A, PP x) :=
begin
  assume h hh,
  cases h with person dontcare,
  existsi person,
  apply hh,
end 

-- (P ∧ Q → R) ↔ (P → Q → R)
-- A = students
-- PP x = x is clever
-- R = the lecturer is happy

example : ((∃ x : A, PP x) → R) ↔ (∀ x: A, PP x → R) :=
begin
  constructor,
  assume h y ppy,
  apply h,
  existsi y,
  exact ppy,

  assume h hh,
  cases hh with a ppa,
  apply h,
  exact ppa,
end

-- equality
-- a = b : Prop given a,b : A

example : ∀ x : A, x = x :=
begin
  assume x,
  reflexivity,
end

example : ∀ x y : A, x = y → PP y → PP x :=
begin
  assume x y e py,
  rewrite e,
  exact py,
end

example : ∀ x y : A, x = y → PP x → PP y :=
begin
  assume x y e px,
  rewrite←  e,
  exact px,
end

example : ∀ x y : A, x = y → y = x :=
begin
  assume x y exy,
  rewrite exy,
end

example : ∀ x y z : A, x = y → y = z → x = z :=
begin
  assume x y z exy eyz,
  rewrite exy,
  exact eyz,
end