Is my axiomatic proof of $\phi \vdash \neg \neg \phi$ correct?

Question

I have constructed the following proof of $\phi \vdash \neg \neg \phi$ using an axiomatic proof system as well as $(\neg$I) and ex falso quodlibet ($\phi,\neg \phi \vdash \psi$) and ($\rightarrow$I), which I've already proved. I get suspicious whenever I use EFQ, so I'm doubting my proof, but perhaps it's fine:

1. $\phi \hspace{5cm} premise$
2. $\neg \phi \hspace{4.6cm} assumption$
3. $\neg \phi \hspace{4.6cm} EFQ, 1,2$
4. $\phi \rightarrow \neg \phi \hspace{3.55cm} \rightarrow I\hspace{0.3cm}1,3$
5. $\neg \phi \hspace{4.55cm} MP \hspace{0.4cm} 1,4 $
6. $\neg \neg \phi \hspace{4.2cm} \neg$I

So I suppose $\neg \phi$, derive $\neg \phi$ by EFQ, and so I can assert $\phi \rightarrow \neg \phi$ and by modus ponens get to $\neg \phi$, which is obviously a contradiction, so we must have $\neg \neg \phi$, when $\phi$ is a premise. I do think that works, but let me know if you spot a blunder! The line that I have some doubts about is the $\rightarrow$ introduction.

To expand, I now ask myself: why can't I just do the following?

1. $\phi \hspace{5cm} premise$
2. $\neg \phi \hspace{4.6cm} assumption$
3. $\neg \phi \hspace{4.6cm} EFQ, 1,2$
4. $\neg \neg \phi \hspace{4.2cm} \neg$I

NOTE: 'assumption' means something we are going to discharge eventually, whereas 'premise' as an actual premise/assumption.

EDIT: The axioms I can use, along with the derived rules I mentioned above, are:

$$ (A1) \hspace{1cm} \phi \rightarrow (\psi \rightarrow \phi)\ $$

$$ (A2) \hspace{1cm} \phi \rightarrow (\psi \rightarrow \chi) \rightarrow ((\phi \rightarrow \psi) \rightarrow (\phi \rightarrow \chi))\ $$

$$ (A3) \hspace{1cm}(\neg \phi \rightarrow \neg \psi) \rightarrow (\psi \rightarrow \phi) $$

Answer 1

I don't think your proof is correct. It's hard to say anything exact without knowing the proof system you are working in. Some remarks for your first proof:

1. For 3. you don't need EFQ, as you already have $\neg\phi$ available in 2.
2. The introduction of the implication does not work. The assumption is 2., not 1., so the resulting implication is $\neg\phi \to \neg\phi$, which is not very useful.
3. I do not know which form of negation introduction you are using. I don't understand the conclusion 6.

One way to construct the proof, is to use the definition $\neg\psi := \psi \to \bot$. Then we have a proof

1. $\phi$ (premise)
2. $\neg \phi$ (assumption)
3. | $\phi \land \neg \phi$ ($\land$ introduction)
4. | $\bot$ (contradiction)
5. $\neg \phi \to \bot$ (implication introduction)
6. $\neg\neg \phi$ (definition)

(The lines starting with | are subject to the assumption).

Another way to proceed is to use the negation introduction in https://en.wikipedia.org/wiki/Negation_introduction .