lec25.lean

section exercise1

variable U : Type
variables A B C: U → Prop

example (h : ∀ x, A x → B x)
        (k : ∃ x, A x)
 : ∃ x, B x
 := sorry



/-
exists.elim k
 (assume t : U,
  assume p : A t,
  have q : B t, from h t p,
  exists.intro t q)
-/
end exercise1



section politicians

/-
Consider some of the various ways of expressing “nobody trusts a politician” in first-order logic:

∀𝑥(politician(𝑥)→∀𝑦(¬trusts(𝑦,𝑥)))

∀𝑥,𝑦(politician(𝑥)→¬trusts(𝑦,𝑥))

¬∃𝑥,𝑦(politician(𝑥)∧trusts(𝑦,𝑥))

∀𝑥,𝑦(trusts(𝑦,𝑥)→¬politician(𝑥))

They are all logically equivalent. Show this for the second and the fourth, by giving natural deduction proofs of each from the other. (As a shortcut, in the ∀
introduction and elimination rules, you can introduce / eliminate both variables in one step.)
-/

variable U : Type --shorter than "people"

variable politician : U → Prop
variable trusts : U → U → Prop

example (h : ∀ x, ∀ y, politician x → ¬ trusts y x) 
 : ∀ x, ∀ y, trusts y x → ¬ politician x
:= sorry




/-
assume t : U,
assume s : U,
assume h1 : trusts s t,
assume h2 : politician t,
have k : politician t → ¬trusts s t, from h t s,
k h2 h1
-/

example (h : ∀ x, ∀ y, trusts y x → ¬ politician x)
 : ¬ ∃ x y, (politician x ∧ trusts y x)
:= sorry


/-
assume k : ∃ x y, (politician x ∧ trusts y x),
exists.elim k
(assume t : U,
 assume l : ∃ (y : U), politician t ∧ trusts y t,
 exists.elim l 
 (assume s : U,
  assume r : politician t ∧ trusts s t ,
  have f : trusts s t → ¬ politician t, from h t s,
  f (and.elim_right r) (and.elim_left r))
)
-/


example (h : ¬ ∃ x y, (politician x ∧ trusts y x)) 
 : ∀ x, ∀ y, trusts y x → ¬ politician x
:= sorry

/-
assume t : U,
assume s : U,
assume p : trusts s t,
assume q : politician t,
h 
(exists.intro t 
  (exists.intro s 
   (and.intro q p)))
-/


end politicians




section bonus

variable U : Type
variables P R : U → Prop
variable Q : Prop

example (h1 : ∃ x, P x ∧ R x) (h2 : ∀ x, P x → R x → Q) : Q :=
exists.elim h1
(assume t : U,
 assume h : P t ∧ R t,
 h2 t (and.elim_left h) (and.elim_right h) )

end bonus