Questions about proving $\lnot \lnot a = a$ 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:


*

*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?

*Are the proofs even right/correct?

*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?

*What ultimately let us say $\lnot \lnot a = a$, the use of the equal sign here?
 A: *

*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.

*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. 

*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.

*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. 

