Q1. Can Barber Paradox be proven false in constructive logic?
I am following the lean tutorial by professor Jeremy Avigad et al. One of the exercises in section 4 asks to prove Barber Paradox false. I can prove it using classical logic, but I can't do it using constructive logic.
Specifically, my proof needs classical logic to prove the lemma
lemma contradictionEquivalence (p : Prop) : ¬(p <-> ¬p) := sorry
The proof of the lemma is straightforward. It uses equivalence elimination and excluded middle followed by two short lambda applications.
variable p : Prop open classical lemma contradictionEquivalence : ¬(p <-> ¬p) := assume LHS : (p <-> ¬p), have Hpnp : (p -> ¬p), from (iff.elim_left LHS), have Hnpp : (¬p -> p), from (iff.elim_right LHS), have ponp : p ∨ ¬p, from (em p), or.elim ponp (take Hp : p, Hpnp Hp Hp) (take Hnp : ¬p, Hpnp (Hnpp Hnp) (Hnpp Hnp))
With the help of this lemma Barber Paradox can be proven false in a single lambda application.
variables (men : Type) (barber : men) (shaves : men → men → Prop) variable (H : ∀ x : men, shaves barber x ↔ ¬shaves x x) theorem barberParadox : false := contradictionEquivalence (shaves barber barber) (H barber)
If I could prove the lemma
contradictionEquivalence in constructive logic, I could answer Q1 in the affirmative.
I suspect that the lemma can be proven in constructive logic, because giving its constructive proof is an exercise in section 3 of the tutorial, but nothing has worked for me so far, so any help would be greatly appreciated.