3
$\begingroup$

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.

$\endgroup$

2 Answers 2

3
$\begingroup$

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

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

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
$\endgroup$
8
  • 1
    $\begingroup$ 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) $\endgroup$ Jan 16, 2017 at 18:57
  • 2
    $\begingroup$ 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$. $\endgroup$
    – Rob Arthan
    Jan 16, 2017 at 20:26
  • 1
    $\begingroup$ 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. $\endgroup$ Jan 16, 2017 at 20:31
  • $\begingroup$ 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 :) $\endgroup$ Jan 16, 2017 at 22:10
  • $\begingroup$ @RobArthan are you referring to principle of explosion en.wikipedia.org/wiki/Principle_of_explosion $\endgroup$ Jan 16, 2017 at 22:11

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.