# Axiomatic Proof of Double Negation Elimination Schema

I need to prove that $\vdash \neg\neg\phi \rightarrow \phi$

Here are my tools aside from modus ponies, Cut Elimination, Deduction Theorem and the three axioms called PL1, PL2 and PL3.
Weakening: $\phi \vdash \psi\rightarrow\phi$
The MP Technique: $\phi \rightarrow (\psi \rightarrow \chi), \phi \rightarrow \psi \vdash \phi\rightarrow\chi$
Transitivity: $\phi \rightarrow \psi, \psi\rightarrow\chi \vdash \phi\rightarrow\chi$
Contraposition (usual)
Principle of Explosion (usual)
Negated Conditional: $\neg(\phi\rightarrow\psi) \vdash Q;$ and $\neg(\phi\rightarrow\psi) \vdash \neg\psi$
Excluded Middle MP: $\phi\rightarrow\psi, \neg\phi\rightarrow\psi \vdash\psi$

I know that by DT and my goal that there is an axiomatic proof from $\neg\neg\phi$ to $\phi$. In other words, by DT and my goal I know that $\neg\neg\phi\vdash\phi.$

From here, though, I am a bit stuck beyond knowing that I need to use PL3 at some point. Does anyone have any $\textit{tips or suggestions}$ on how to proceed?

• Did your instructor do any proofs? Do you have any other results you can use? And by the way, you cannot say that you know that $\neg \neg \phi \vdash \phi$ ... you should merely say to yourself: "I could prove that $\vdash \neg \neg \phi \rightarrow \phi$ if I could prove that $\neg \neg \phi \vdash \phi$, for then I just have to apply DT to the latter to get the former. So, let me try to prove the latter". – Bram28 Oct 14 '17 at 13:56
• Right. I meant to say that my goal had merely changed. I've done proofs for all of these tools but so far I cannot recall my proving any other results that I may use besides $\phi \rightarrow \phi$ – Rusty Oct 14 '17 at 14:05
• OK, but if you have proven some other results, then even if you are not allowed to use them as givens, at least you have the proofs for them, and build on top of them to try and get this partiuclar result. Also, as you noticed, proofs in these kinds of axiomatic systems are extremely frustrating, especially at the beginning. This $\neg \neg \phi \vdash \phi$ is no exception: there is no easy proof of this, and I have no idea why you would be expedted to find a proof if you are just beginning with proofs (which is what it seems like). Did your instructor give no poinrs at all? – Bram28 Oct 14 '17 at 14:13
• I also feel as though my proof of $\neg\neg P \vdash P$ should be useful somehow but I feel as though my final proof needs involve metavariables only. – Rusty Oct 14 '17 at 14:13
• In terms of pointers all I have heard is that axiomatic proof systems are almost completely bereft of strategy unlike other proof systems (tableaux, natural deductions, etc). – Rusty Oct 14 '17 at 14:15