# Constructive proof of Barber Paradox

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)

(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.

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))$.

• Ah, I see, it's a double contradiction! That's very helpful, thank you! I'll see how to write it in lean now. Jan 16, 2017 at 13:23

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

• A proof of a negation is not a proof by contradiction. Henning's proof does not use proof by contradiction. His proof corresponds to the Agda term: example : {P : Set} → ¬ ((P → ¬ P) ∧ (¬ P → P)); example (p-to-not-p , not-p-to-p) = p-to-not-p p p where p = not-p-to-p (λ h → p-to-not-p h h) Jan 16, 2017 at 18:57
• Note that when you read $\lnot p$ as $p \to \bot$ (as you can in intutionistic logic), then Henning's proof works (with slight modifications to the wording), even if you replace $\bot$ by some unspecified $q$. It shows that $((p \to p \to q) \land ((p \to q) \to p)) \to q$ is intuitionistically valid for any $q$ not just $\bot$. Jan 16, 2017 at 20:26
• Unless I'm completely misunderstanding the syntax of your proof assitant, the proof you quote is exactly the one I'm suggesting in my answer. Jan 16, 2017 at 20:31
• Yes it is. As others are pointing out, I just misunderstood your first bullet point. But @RobArthan 's suggestion is very good -- and exactly what I thought was missing from your proof. What's happening there is that we create a lambda expression which takes a term of type p (proof of p), and produces false, i.e. p -> false, i.e. ¬p. But I get it now, so big thanks to both :) Jan 16, 2017 at 22:10
• @RobArthan are you referring to principle of explosion en.wikipedia.org/wiki/Principle_of_explosion Jan 16, 2017 at 22:11