Does the Barber Paradox require classical reasoning?

Stream: new members

[Martin C. Martin]

Does the Barber paradox require classical reasoning? From TPiL chapter 4 exercises:

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

example (h : ∀ x : men, shaves barber x ↔ ¬ shaves x x) :
  false := sorry

[Martin C. Martin]

It reduces to $\neg (p \iff \neg p)$

[Violeta Hernández]

(deleted)

[Martin C. Martin]

Oh I think I see it now, thanks.

[Violeta Hernández]

Sorry, thought I had seen a classical proof but I'm not sure anymore

[Kevin Buzzard]

Yeah this can be proved constructively but it's a little tricky. There are many threads about this question here!

[Patrick Johnson]

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

lemma x (h : ∀ x : men, shaves barber x ↔ ¬ shaves x x) : false :=
(h barber).mp ((h barber).mpr (id (λ (h₃ : shaves barber barber), (h barber).mp h₃ h₃)))
((h barber).mpr (id (λ (h₃ : shaves barber barber), (h barber).mp h₃ h₃)))

#print axioms x -- no axioms

[Martin C. Martin]

This is just a reframing of the last question in chapter 3.

The way I think of it is: once you've assumed the premise, and your goal is simply false, you're in a world where the context contains a contradiction. So you should be able to prove anything. Proving something directly is hard, partly because you don't know whether the predicate is true or false. So trying proving $\neg P$ by assuming $P$ and looking for a contradiction.