6
$\begingroup$

How do you prove $\neg\neg(\neg\neg P \rightarrow P)$ in intuitionistic logic?

I know this statement to be intuitionistically provable because of Glivenko's theorem. However, I wish to prove it intuitionistically.

The relevant axioms I happen to be using are: (1) $\neg P = P\rightarrow\bot$ and (2) $\bot \rightarrow P$.

$\endgroup$
3
  • $\begingroup$ @avid19 Better? Btw, this question is not a duplicate of the one linked, as my edit shows. $\endgroup$ Dec 21, 2015 at 3:50
  • 1
    $\begingroup$ There is a proof outline in the comments of the linked answer, but with the edit, I agree that this is no longer a duplicate, and I've voted to reopen. $\endgroup$
    – Slade
    Dec 21, 2015 at 3:58
  • 1
    $\begingroup$ I also voted to reopen. $\endgroup$
    – user223391
    Dec 21, 2015 at 4:04

1 Answer 1

8
$\begingroup$

The first thing to notice is that $$(\lnot(\lnot\lnot P \to P)) \to \lnot P\qquad(\star)$$ Indeed, suppose $\lnot(\lnot\lnot P \to P)$ and $P$ ; we want to show $\bot$.

By modus ponens, it suffices to prove $\lnot\lnot P \to P$, but as you supposed $P$, the implication is clearly true.

Now, for the main result, suppose $\lnot(\lnot\lnot P \to P)$ ; you want to show $\bot$. By modus ponens, it suffices to show $\lnot\lnot P \to P$. Suppose now $\lnot\lnot P$. By $(\star)$, you also have $\lnot P$, and you know that $\lnot\lnot P \land \lnot P \to \bot$. Thus you have $\bot$, thus $P$, and the result is proved.

Edit : This proof is, on some points, similar to the proof of $\lnot\lnot(P\lor\lnot P)$, delightly explained by Phil Wadler in section 4 of http://homepages.inf.ed.ac.uk/wadler/papers/dual/dual.pdf

$\endgroup$
0

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.