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.