M40001 Sheet 1

Stream: new members

[Michael]

Hello, sorry if this is a silly question but how do I get rid of a universal quantifier in a hypothesis?

lemma question_2a_false : ¬ (∀ P Q : Prop, (P → Q) → (Q → P)) :=
begin
  intro h,
  sorry
end

leaves me with

h: ∀ (P Q : Prop), (P → Q) → Q → P
⊢ false

and I don't know how to make any more progress.

[Alex J. Best]

A forall is an implication, so its really a function that you can plug input into.
In this case its a function from propositions to some implications between their proofs so you can apply it to some specific (well-chosen) propositions of interest using have to make a new hypothesis (called this by default, specialising the old one), e.g.:

lemma question_2a_false : ¬ (∀ P Q : Prop, (P → Q) → (Q → P)) :=
begin
  intro h,
  have := h true false,
  sorry
end

this is just a random example, not a spoiler / hint (probably).

[Eric Wieser]

What's your maths proof?

[Michael]

Since the question asks whether → is symmetric, I have a counter-example to the idea that → is symmetric: if P is false and Q is true then P → Q is true and Q → P is false and so we have true → false which is false.

[Eric Wieser]

"set P to false and Q to true" is spelt have := h false true