Constructive proof of Barber Paradox

Question

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.

Answer 1

Assume $p\to\neg p$ and $\neg p \to p$.

• Asume $p$. Then, since $p\to\neg p$, also $\neg p$. But $p$ and $\neg p$ are a contradiction.
• Thus, we have proved $\neg p$.
• Since $\neg p\to p$, also $p$.
• But $\neg p$ and $p$ are a contradiction.

The assumption $(p\to \neg p)\land(\neg p\to p)$ led to a contradiction, so $\neg((p\to \neg p)\land(\neg p\to p))$.

Answer 2

The answer of Henning Makholm is almost perfect, with one exception: according to the tutorial, proof by contradiction by_contradiction can only be used in the classical setting. I have worked around it by using the following lambda application Hpnp Hp Hp. This is a full constructive proof of the lemma:

variable p : Prop

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 Hnp : ¬p, from (assume Hp : p, Hpnp Hp Hp),
    have Hp : p, from Hnpp Hnp,
    show false, from Hnp Hp