barber paradox & classical logic

Stream: new members

[Kristian Notari]

I have tried to solve the examples in the TPL4 and I've encountered the barber paradox at exercise 3 here (end of the page).

I've solved it this way:

open Classical

variable (men : Type) (barber : men)
variable (shaves : men → men → Prop)
variable (p : shaves barber barber)

example (h : ∀ x : men, shaves barber x ↔ ¬ shaves x x) : False :=
  match (h barber) with
    | ⟨l, r⟩ =>
      let p := shaves barber barber
      Or.elim (em p)
        (fun a => absurd a (l a))
        (fun b => absurd (r b) b)

Besides my syntax usage that could be improved for sure, do I always need classical logic to prove this? I'm using classical with the em bit for stating p v !p basically.

[Eric Rodriguez]

no, you don't need classical logic; ¬(p ↔ ¬p) suffices, and it's a fun exercise to prove that one intuistionistically

[Kristian Notari]

Thanks for answering. I'm not sure I correctly understood what "intuistionistically" means in this context. It has nothing to do with Lean, right? It was like saying "prove that in your mind, with words, it should be fun" ?

By the way I'm not getting how to prove that with ¬(p ↔ ¬p) honestly :( I'll try again asap

[Martin Dvořák]

No. They were referring to intuitionistic logic, that is, constructive proof required.

[Kristian Notari]

Ok, so to be clear, constructive proof --> proof by actually instantiating a value for the given proof, by using lean terms directly instead of using tactics. Am I right?

Sorry for being new to all this, I'm going through the TPL4 as I'm writing this

[Eric Rodriguez]

A constructive proof is one that doesn't need classical logic like em, and in some ways yes, you just write a function in terms of recursors etc

[Ryan McCorvie]

I had this exact same question doing the exercises. On careful rereading, I see ¬ ( p ↔ ¬ p) is on the list of propositions at the end of chapter three , in the section of which doesn't rely on classical logic. However it's not on the list of exercise problems, and in fact it's the only proposition listed which is not also an exercise! With this hint that it's possible, it is a fun bit of diagram chasing.