# Simple proof of $\phi \rightarrow \neg \neg \phi$

I have constructed a very simple axiomatic proof of $$\phi \rightarrow \neg \neg \phi$$, but it's so simple I doubt it. Here it is:

1. $$\phi$$ Assumption
2. $$\neg \phi$$ Assumption
3. $$\neg \neg \phi$$ ($$\neg$$I)
4. $$\phi \rightarrow \neg \neg \phi$$ ($$\rightarrow$$I) $$\square$$

I have derived $$\neg$$I independently, and $$\rightarrow$$I is just the deduction theorem, which I've derived also. Can anyone spot an error?

• What is the $\neg I$ rule you're using? Commented Nov 17, 2022 at 12:51

This is a valid (and well-known) argument, assuming that the $$\neg I$$ rule you proved is the following or similar:
From $$\Gamma, A \vdash B$$ and $$\Gamma,A \vdash \neg B$$ infer $$\Gamma \vdash \neg A$$.
You're just instantiating it with $$\Gamma$$ set to $$\{ \varphi \}$$, $$A$$ to $$\neg \varphi$$, and $$B$$ to $$\varphi$$. Of course, if you were to go through the proofs of the deduction theorem and the $$\neg I$$ rule and wrote down the actual Hilbert proof starting from the three axioms, it wouldn't look that simple anymore.