# Proof of a certain proposition not using classical logic

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!

• 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!
– Eric
Jun 26, 2022 at 17:37
• 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. Jun 26, 2022 at 19:18