Zulip Chat Archive

Stream: new members

Topic: barber's paradox

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 :=

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?

Kenny Lau (Sep 09 2020 at 08:32):

have h1 := h barber

Claus-Peter Becke (Sep 09 2020 at 08:36):

@Kenny Lau

Alexandre Rademaker (Sep 10 2020 at 00:16):

why using Type* ? Why not only Type?

Scott Morrison (Sep 10 2020 at 00:20):

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

Alexandre Rademaker (Sep 10 2020 at 01:00):

Sorry, I didn't understand.

Kenny Lau (Sep 10 2020 at 06:10):

Type* means in an arbitrary universe

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: Dec 20 2023 at 11:08 UTC