Questions about proving $\lnot \lnot a = a$

Question

This is all in the context of a Hilbert system with modus ponens $A, A\to B \vdash B$ and axioms:

Axiom $1$: $A \to (B \to A)$

Axiom $2$: $(A \to (B \to C)) \to ((A \to B) \to (A \to C))$

Axiom $3$: $(\lnot B \to \lnot A) \to (A \to B)$

So I tried to prove double-negation elimination by doing the following:

\begin{array}{ccc} 1 & \{ \lnot \lnot a \} \vdash \lnot \lnot a & \text{Premise}\\ 2 & \{ \lnot \lnot a \} \vdash \lnot \lnot a \to (\lnot \lnot \lnot \lnot a \to \lnot \lnot a) & \text{ Axiom } 1\\ 3 & \{ \lnot \lnot a \} \vdash \lnot \lnot \lnot \lnot a \to \lnot \lnot a & \text{ Modus Ponens } 1, 2\\ 4 & \{ \lnot \lnot a \} \vdash (\lnot \lnot \lnot \lnot a \to \lnot \lnot a) \to (\lnot a \to \lnot \lnot \lnot a) & \text{ Axiom } 3\\ 5 & \{ \lnot \lnot a \} \vdash \lnot a \to \lnot \lnot \lnot a & \text{ Modus Ponens } 3, 4\\ 6 & \{ \lnot \lnot a \} \vdash (\lnot a \to \lnot \lnot \lnot a) \to (\lnot \lnot a \to a) & \text{ Axiom } 3\\ 7 & \{ \lnot \lnot a \} \vdash \lnot \lnot a \to a & \text{ Modus Ponens } 5, 6\\ 8 & \{ \lnot \lnot a \} \vdash a & \text{ Modus Ponens } 1, 7\\ 9 & \vdash \lnot \lnot a \to a & \text{ Deduction Theorem } \\ \end{array}

And then I continued on, to prove double negation introduction:

\begin{array}{ccc} 10 & \vdash \lnot \lnot \lnot a \to \lnot a & \text{Double Negation Elimination}\\ 11 & \vdash (\lnot\lnot \lnot a \to \lnot a) \to (a \to \lnot \lnot a) & \text{ Axiom } 3\\ 12 & \vdash a \to \lnot \lnot a & \text{ Modus Ponens } 10, 11\\ \end{array}

My questions:

1. Am I allowed to invoke the deduction theorem in the middle of a proof like this (step $9$)? Is this considered a context change? Is context-changing allowed?

2. Are the proofs even right/correct?

3. Assuming it's all correct: Are we able to combine them to say that $a \to \lnot \lnot a$ and $\lnot \lnot a \to a$, therefore $a \iff \lnot \lnot a$ or is this symbol not allowed?

4. What ultimately let us say $\lnot \lnot a = a$, the use of the equal sign here?

Answer 1

1. The sequence 1-8 is a derivation (in the Hilbert system for implicative propositional classical logic) of $\lnot \lnot a \vdash a$. Step 9 does not correspond to an inference rule in such Hilbert system, thus the sequence 1-9 is not a derivation of $\vdash \lnot \lnot a \to a$ in such Hilbert system. The deduction theorem says that, since there is a derivation of $\lnot \lnot a \vdash a$, then there exists another derivation (which you didn't construct, but there exists) of $\vdash \lnot \lnot a \to a$. So, if the question is "Show a derivation of $\vdash \lnot \lnot a \to a$ in such Hilbert system", you didn't answer it; but if the question is "Show that $\vdash \lnot \lnot a \to a$ is derivable in such Hilbert system", your answer is fine (except that step 9 is not allowed as an inference rule in the Hilbert system, i.e. you should consider the sequence 1-8 and then apply the deduction theorem to conclude). See also here.

2. Concerning the proof of $\vdash \lnot \lnot a \to a$, see point 1. Your derivation for $\vdash a \to \lnot \lnot a$ (which is completely independent and separated from the derivation 1-8) is correct, on the proviso that you have already proved that $\vdash \lnot \lnot \lnot a \to \lnot a$ is derivable in the Hilbert system.

3. If you want to consider $\leftrightarrow$ as a connective in the formal language, then you need to add some axioms concerning it in the Hilbert system. Without these axioms, the formula $a \leftrightarrow \lnot \lnot a$ makes no sense in the Hilbert system and hence it is not allowed. The list of axioms that you have to add to the Hilbert system for the connective $\leftrightarrow$ is here.
4. The notation $a = \lnot \lnot a$ (I prefer to write $a\equiv \lnot \lnot a$ or $a\dashv\vdash \lnot \lnot a$) means that both $\vdash \lnot \lnot a \to a$ and $\vdash a \to \lnot \lnot a$ are derivable in the Hilbert system, which is essentially what you have proved (or want to prove). Note that $a = \lnot \lnot a$ and $a\equiv \lnot \lnot a$ and $a\dashv\vdash \lnot \lnot a$ are not formulas in the language, they are just notations in the meta-language. See also point 3.