Zulip Chat Archive

Stream: new members

Topic: barber's paradox


view this post on Zulip Claus-Peter Becke (Sep 09 2020 at 08:32):

variables (men : Type*) (barber : men)
variable (shaves : men  men  Prop)

example (h :  x : men, shaves barber x  ¬ shaves x x) : false :=
begin
end

It is to prove that a contradiction follows from the hypotheses. My goal is to find two hypotheses which contradict each other. The first I would like to do is to remove the universal quantifier from the hypothesis. To be able to do that, x should be introduced. But to introduce it as an arbitrary object presupposes that the quantified x appears inside the goal. The only way to achieve this is to use the revert-tactic as far as I see. But after having done that I'll get an implication forall x ... -> false. Which alternatives do I have?

view this post on Zulip Kenny Lau (Sep 09 2020 at 08:32):

have h1 := h barber

view this post on Zulip Claus-Peter Becke (Sep 09 2020 at 08:36):

@Kenny Lau
Thanks.

view this post on Zulip Alexandre Rademaker (Sep 10 2020 at 00:16):

why using Type* ? Why not only Type?

view this post on Zulip Scott Morrison (Sep 10 2020 at 00:20):

Don't you have barbers in your universe? :-)

view this post on Zulip Alexandre Rademaker (Sep 10 2020 at 01:00):

Sorry, I didn't understand.

view this post on Zulip Kenny Lau (Sep 10 2020 at 06:10):

Type* means in an arbitrary universe

view this post on Zulip Eric Wieser (Sep 10 2020 at 10:47):

A proof of the barber paradox was discussed before in https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/barber.20paradox/near/206917550


Last updated: May 11 2021 at 22:14 UTC