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

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)$$

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 .

• I am using an axiomatic proof system, the axioms being: $$(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)$$ Commented Nov 4, 2022 at 14:33
• The form of negation introduction I am using is this: if $\Gamma, \phi \vdash \psi$ and $\Gamma, \phi \vdash \neg \phi$, then $\gamma \vdash \neg \phi$ Commented Nov 4, 2022 at 14:39
• So I can't use natural deduction rules such as and-introduction unless I derive them myself. Commented Nov 4, 2022 at 14:53
• I assume you meant: if $\Gamma, \phi \vdash \psi$ and $\Gamma, \phi \vdash \neg \psi$, then $\Gamma \vdash \neg\phi$? Commented Nov 4, 2022 at 14:57
• In which case, you immediately have the derivation $\phi, \neg \phi \vdash \phi$ and $\phi, \neg\phi \vdash \neg \phi$ implies $\phi \vdash \neg\neg \phi$, where $\phi$ plays the role of $\Gamma$ and $\psi$ Commented Nov 4, 2022 at 14:59