2
$\begingroup$

I'm self-studying the textbook Theorem Proving in Lean, and there's one exercise from Section 3.7 that I'm stuck on. The exercise asks for a proof of the proposition ¬(p ↔ ¬p) that does not use classical logic. I've been able to prove the the proposition using classical logic by using proof by cases applied to p ∨ ¬p, but I don't know how to prove the proposition without the Law of Excluded Middle. Here is my classical proof:

open classical
example : ¬(p ↔ ¬p) :=
  or.elim
    (em (p))
    (λ h1 : p,
      λ h2 : p ↔ ¬p,
        iff.elim_left (h2) (h1) (h1))
    (λ h1 : ¬p,
      λ h2 : p ↔ ¬p,
        h1 (iff.elim_right (h2) (h1)))

For reference, a non-classical proof can use the following rules:

  1. and.intro
  2. and.elim_left
  3. and.elim_right
  4. or.intro_left
  5. or.intro_right
  6. or.elim
  7. false.elim
  8. true.intro
  9. iff.intro
  10. iff.elim_left
  11. iff.elim_right

and a classical proof gets the additional extra rule:

  1. em

Any help proving this proposition non-classically would be much appreciated!

$\endgroup$
5
  • $\begingroup$ A search on google finds this third-party solutions repository, which contains the proof you seek (and proofs for various other exercises). Of course there's no guarantee those proofs work until you ask Lean to check them! $\endgroup$
    – Eric
    Jun 26, 2022 at 17:37
  • $\begingroup$ This question already has an answer on Stack Overflow $\endgroup$
    – Eric
    Jun 26, 2022 at 17:41
  • $\begingroup$ That's very helpful! Thanks @Eric $\endgroup$ Jun 26, 2022 at 17:51
  • 2
    $\begingroup$ This is one of my favorite logic puzzles for students learning logic. It seems very difficult as written, but much more intuitive when negation is written as -> false and false is replaced with an arbitrary propositional constant q. This only works because it is actually a theorem of minimal logic. $\endgroup$
    – Jason Rute
    Jun 26, 2022 at 19:18
  • $\begingroup$ I didn't know about the generalisation, Jason, that's very cool! $\endgroup$ Jun 26, 2022 at 20:00

0

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Browse other questions tagged or ask your own question.