You are right to suspect that your described method does not work to prove the Deduction Theorem: if you simply extend the existing deduction of $B$ from $\Delta \cup \{ A \}$ by adding $B \rightarrow (A \rightarrow B)$ (from axiom 1) and then getting $A \rightarrow B$ through Modus Ponens, then all you have ended up showing is that there is a deduction of $\Delta \cup \{ A\} \vdash A \rightarrow B$, because the original set of premises is still $\Delta \cup \{ A \}$. And you can't just throw out the $A$, since in the extended derivation, you still need to get to $B$ by itself, which may well depend on $A$.
So ... you need to do something else to show $\Delta \vdash A \rightarrow B$
Here is what you need to do. Transform the deduction of $\Delta \cup \{A \} \vdash B$ into a deduction of $\Delta \vdash A \rightarrow B$ by showing how you can get a deduction $\Delta \vdash A \rightarrow \varphi_i$ for $\varphi_i$ of the original deduction. And that you can show by strong induction, where you have to consider that every $\varphi_i$ comes about as one of the three cases: as an element of $\Delta$, an instance of some axiom, or by the use of Modus Ponens.
Here is a simple example:
If we take that $\Delta = \{ A \rightarrow B \}$, then we know that $\Delta \cup \{ A \} \vdash B$, i.e. that $\{ A \rightarrow B, A \} \vdash B$. Indeed, here is a derivation for that:
\begin{array}{ccc}
1 & A \rightarrow B & Given\\
2 & A & Given\\
3 & B & \text{Modus Ponens } 2,3
\end{array}
OK, so now we want to convert this to a derivation of $\Delta \vdash A \rightarrow B$, i.e. of $\{ A \rightarrow B \} \vdash A \rightarrow B$
Now, there is of course a very simple derivation for $\{ A \rightarrow B \} \vdash A \rightarrow B$, but what I want to show below is that we can systematically convert the earlier derivation of $\{ A \rightarrow B, A \} \vdash B$ into a new derivation of $\{ A \rightarrow B \} \vdash A \rightarrow B$
Again, the basic idea is that, since we are 'pulling out' $A$ from the set of assumptions, in the new derivation we want to get a statement of the form $A \rightarrow \varphi_i$ for every line $\varphi_i$ from the original derivation. Think of this as 'conditionalizing' every statement with the condition $A$. So, the basic scheme for the derivation will look like:
\begin{array}{ccc}
..\\
k & A \rightarrow (A \rightarrow B) & ??\\
..\\
l & A \rightarrow A & ??\\
..\\
m & A \rightarrow B & ??
\end{array}
Now, notice that the last line is $A \rightarrow B$, which is exactly what we are trying to get, so that's already good. But of course, we have yet to figure out how to actually get there. In fact, let's first enter the givens, which are all the same givens as in the original derivation, excvept for $A$, since that's the one we're 'pulling out':
\begin{array}{ccc}
1 & A \rightarrow B & Given\\
..\\
k & A \rightarrow (A \rightarrow B) & ??\\
..\\
l & A \rightarrow A & ??\\
..\\
m & A \rightarrow B & ??
\end{array}
OK, now, note that we put down line $k$ exactly because we had line $1$ as a given in the original derivation. That is, for tevery $\varphi_i \in \Delta$, we put down, and are trying to get to, $A \rightarrow \varphi_i$ .. how can we do that? Easy: just exploit axiom $1$:
\begin{array}{ccc}
1 & A \rightarrow B & Given\\
2 & (A \rightarrow B) \rightarrow (A \rightarrow (A \rightarrow B)) & \text{ Axiom } 1\\
3 & A \rightarrow (A \rightarrow B) & \text{ Modus Ponens } 1,2 \\
..\\
l & A \rightarrow A & ??\\
..\\
m & A \rightarrow B & ??
\end{array}
Now, the $A \rightarrow A$ is because the $A$ was in the original set of givens as well, but since in the new derivation we no longer have $A$ as a given, we need to derive $A \rightarrow A$ in a different way. But, as you found, such a derivation can always be done:
\begin{array}{ccc}
1 & A \rightarrow B & Given\\
2 & (A \rightarrow B) \rightarrow (A \rightarrow (A \rightarrow B)) & \text{ Axiom } 1\\
3 & A \rightarrow (A \rightarrow B) & \text{ Modus Ponens } 1,2 \\
4 & (A \rightarrow ((A \rightarrow A) \rightarrow A) \rightarrow ((A \rightarrow (A \rightarrow A)) \rightarrow (A \rightarrow A)) & \text{ Axiom } 2\\
5 & A \rightarrow ((A \rightarrow A) \rightarrow A) & \text{ Axiom } 1\\
6 & (A \rightarrow (A \rightarrow A)) \rightarrow (A \rightarrow A) & \text{ Modus Ponens } 4,5 \\
7 & A \rightarrow (A \rightarrow A) & \text{ Axiom } 1\\
8 & A \rightarrow A & \text{ Modus Ponens } 6,7 \\
..\\
m & A \rightarrow B & ??
\end{array}
OK, almost done. Now we need to show how line $m$ can be derived from the original lines $k$ and $l$, i.e. lines $3$ and $8$. Well, for this you use axiom 2. That is, since in the original derivation we went from $A \rightarrow B$ and $A$ to $B$ via Modus Ponens, in the new derivation we need to do this using the conditionalized statements, i.e. we need to go from $A \rightarrow (A \rightarrow B)$ and $A \rightarrow A$ to $A \rightarrow B$. How do we do this? Well, this is exactly what Axiom 2 is for: Axiom 2 always looks a ittle weird if you first see it, but Axiom 2 is actually the embodiment of this kind of 'conditionalized Modus Ponens'. Here is how it goes:
\begin{array}{ccc}
1 & A \rightarrow B & Given\\
2 & (A \rightarrow B) \rightarrow (A \rightarrow (A \rightarrow B)) & \text{ Axiom } 1\\
3 & A \rightarrow (A \rightarrow B) & \text{ Modus Ponens } 1,2 \\
4 & (A \rightarrow ((A \rightarrow A) \rightarrow A) \rightarrow ((A \rightarrow (A \rightarrow A)) \rightarrow (A \rightarrow A)) & \text{ Axiom } 2\\
5 & A \rightarrow ((A \rightarrow A) \rightarrow A) & \text{ Axiom } 1\\
6 & (A \rightarrow (A \rightarrow A)) \rightarrow (A \rightarrow A) & \text{ Modus Ponens } 4,5 \\
7 & A \rightarrow (A \rightarrow A) & \text{ Axiom } 1\\
8 & A \rightarrow A & \text{ Modus Ponens } 6,7 \\
9 & (A \rightarrow (A \rightarrow B))\rightarrow ((A \rightarrow A) \rightarrow (A \rightarrow B)) & \text{ Axiom } 2\\
10 & (A \rightarrow A) \rightarrow (A \rightarrow B) & \text{ Modus Ponens } 3,9 \\
11 & A \rightarrow B & \text{ Modus Ponens } 8,10
\end{array}
.... and we're done!
OK, so this was just a simple example, but I think you can see how this general technique always works: Your goal is to conditionalize all statements from the original derivation with the '$A$' that you pull out, and you derive those as follows:
Derive $A \rightarrow A$ for that $A$.
Derive $A \rightarrow \varphi_i$ for every $\varphi_i \in \Delta$ using the $\varphi_i$ you still have as a given in the new derivation, and using axiom 1.
Derive any $A \rightarrow \varphi_k$ where in the original derivation $\varphi_k$ was derived using Modus Ponens from earlier $\varphi_i$ and $\varphi_j = \varphi_i \rightarrow \varphi_k$ from the conditionalized $A \rightarrow \varphi_i$ and $A \rightarrow \varphi_j = A \rightarrow (\varphi_i \rightarrow \varphi_k)$ using axiom 2
Best Answer
First, here is proof that shows $\neg \neg P \vdash P$:
\begin{array}{lll} 1&\neg \neg P & Premise\\ 2&\neg \neg P \to (\neg \neg \neg \neg P \to \neg \neg P) & Axiom \ 1\\ 3&\neg \neg \neg \neg P \to \neg \neg P & MP \ 1,2\\ 4&(\neg \neg \neg \neg P \to \neg \neg P) \to (\neg P \to \neg \neg \neg P) & Axiom \ 3\\ 5&\neg P \to \neg \neg \neg P & MP \ 3,4\\ 6&(\neg P \to \neg \neg \neg P) \to (\neg \neg P \to P) & Axiom \ 3\\ 7&\neg \neg P \to P& MP \ 5,6\\ 8&P & MP \ 1,7\\ \end{array}
And so the Deduction Theorem states that this also means that $\vdash \neg \neg P \to P$
OK, but now you ask: Great .. but you used the Deduction Theorem. But is it provable without the Deduction Theorem?
First, the way you phrase your question makes me think that you are mixing up rules of (or within) the logic system with theorems (like the Deduction Theorem) about that system!
To be specific: In the above formal proof, I didn't use the Deduction Theorem as a rule or inference: the Deduction Theorem was never on any line. All lines were instances of either axioms or Modus Ponens, just as it should for any formal proof in this system.
However, in the above mathematical proof I did demonstrate (using a combination of a formal proof followed by a reference to the Deduction Theorem) that $P$ is provable from $\neg \neg P$. That is, I provided a formal proof that $P$ is provable from $\neg \neg P$, and then applied the Deduction Theorem to obtain the result that $\neg \neg P \to P$is provable from no premises at all.
But yes, I did not provide a formal proof that actually goes from no premises at all to $\neg \neg P \to P$. And that is of course what you really mean when you say that you want a proof without the use of the Deduction Theorem. OK, so thanks to the Deduction Theorem we already know it is possible .. but how would we actually do this?
Well, a typical proof of the Deduction Theorem will provide you with the recipe for transforming the proof above into the one you want. The basic idea is to put $\neg \neg P$ in front of all the statements of the original proof. That is, we conditionalize all statements with the premise that we want to discharge. Here is what it looks like:
\begin{array}{lll} ...\\ &\neg \neg P \to \neg \neg P &\\ ...\\ &\neg \neg P \to (\neg \neg P \to (\neg \neg \neg \neg P \to \neg \neg P)) & \\ ...\\ &\neg \neg P \to (\neg \neg \neg \neg P \to \neg \neg P) & \\ ...\\ &\neg \neg P \to ((\neg \neg \neg \neg P \to \neg \neg P) \to (\neg P \to \neg \neg \neg P)) & \\ ...\\ &\neg \neg P \to (\neg P \to \neg \neg \neg P) & \\ ...\\ &\neg \neg P \to ((\neg P \to \neg \neg \neg P) \to (\neg \neg P \to P)) & \\ ...\\ &\neg \neg P \to (\neg \neg P \to P)& \\ ...\\ &\neg \neg P \to P & \\ \end{array}
Interestingly, I can already tell you what the line numbers are going to be, because the transformation algorithm I am going to describe below is completely systematic:
\begin{array}{lll} ...\\ 5&\neg \neg P \to \neg \neg P &\\ ...\\ 8&\neg \neg P \to (\neg \neg P \to (\neg \neg \neg \neg P \to \neg \neg P)) & \\ ...\\ 11&\neg \neg P \to (\neg \neg \neg \neg P \to \neg \neg P) & \\ ...\\ 14&\neg \neg P \to ((\neg \neg \neg \neg P \to \neg \neg P) \to (\neg P \to \neg \neg \neg P)) & \\ ...\\ 17&\neg \neg P \to (\neg P \to \neg \neg \neg P) & \\ ...\\ 20&\neg \neg P \to ((\neg P \to \neg \neg \neg P) \to (\neg \neg P \to P)) & \\ ...\\ 23&\neg \neg P \to (\neg \neg P \to P)& \\ ...\\ 26&\neg \neg P \to P & \\ \end{array}
OK, so how do we fill in the missing lines?
First, the original premise $\neg \neg P$ that we are trying to discharge has become the tautology $\neg \neg P \to \neg \neg P$, and typically $\phi \to \phi$ is one of the first proofs (if not the first proof) you typically do when discussing these axiom systems, and it takes $5$ lines to do it in the new proof:
\begin{array}{lll} 1& (\neg \neg P \to ((P \to \neg \neg P) \to \neg \neg P) \to ((\neg \neg P \to (P \to \neg \neg P)) \to (\neg \neg P \to \neg \neg P)) & Axiom 2\\ 2& \neg \neg P \to ((P \to \neg \neg P & Axiom \ 1\\ 3&(\neg \neg P \to (P \to \neg \neg P)) \to (\neg \neg P \to \neg \neg P) & MP \ 1,2\\ 4&\neg \neg P \to (P \to \neg \neg P) & Axiom \ 1\\ 5&\neg \neg P \to \neg \neg P & MP \ 3,4\\ ...\\ 8&\neg \neg P \to (\neg \neg P \to (\neg \neg \neg \neg P \to \neg \neg P)) & \\ ...\\ 11&\neg \neg P \to (\neg \neg \neg \neg P \to \neg \neg P) & \\ ...\\ 14&\neg \neg P \to ((\neg \neg \neg \neg P \to \neg \neg P) \to (\neg P \to \neg \neg \neg P)) & \\ ...\\ 17&\neg \neg P \to (\neg P \to \neg \neg \neg P) & \\ ...\\ 20&\neg \neg P \to ((\neg P \to \neg \neg \neg P) \to (\neg \neg P \to P)) & \\ ...\\ 23&\neg \neg P \to (\neg \neg P \to P)& \\ ...\\ 26&\neg \neg P \to P & \\ \end{array}
Second, any statement in the original proof we obtained as an instance of an axiom, can be obtained in the new proof as well, and that statement can then be conditionalized using Axiom 1 (indeed, Axiom 1 serves exactly that purpose of 'conditionalization'). As an example, let me do that just for line 2 of the original proof, leading to lines 6 through 8::
\begin{array}{lll} 1& (\neg \neg P \to ((P \to \neg \neg P) \to \neg \neg P) \to ((\neg \neg P \to (P \to \neg \neg P)) \to (\neg \neg P \to \neg \neg P)) & Axiom 2\\ 2& \neg \neg P \to ((P \to \neg \neg P & Axiom \ 1\\ 3&(\neg \neg P \to (P \to \neg \neg P)) \to (\neg \neg P \to \neg \neg P) & MP \ 1,2\\ 4&\neg \neg P \to (P \to \neg \neg P) & Axiom \ 1\\ 5&\neg \neg P \to \neg \neg P & MP \ 3,4\\ 6&\neg \neg P \to (\neg \neg \neg \neg P \to \neg \neg P) & Axiom \ 1\\ 7&(\neg \neg P \to (\neg \neg \neg \neg P \to \neg \neg P)) \to (\neg \neg P \to (\neg \neg P \to (\neg \neg \neg \neg P \to \neg \neg P)))& Axiom \ 1\\ 8&\neg \neg P \to (\neg \neg P \to (\neg \neg \neg \neg P \to \neg \neg P)) & MP \ 6,7\\ ...\\ 11&\neg \neg P \to (\neg \neg \neg \neg P \to \neg \neg P) & \\ ...\\ 14&\neg \neg P \to ((\neg \neg \neg \neg P \to \neg \neg P) \to (\neg P \to \neg \neg \neg P)) & \\ ...\\ 17&\neg \neg P \to (\neg P \to \neg \neg \neg P) & \\ ...\\ 20&\neg \neg P \to ((\neg P \to \neg \neg \neg P) \to (\neg \neg P \to P)) & \\ ...\\ 23&\neg \neg P \to (\neg \neg P \to P)& \\ ...\\ 26&\neg \neg P \to P & \\ \end{array}
OK, so let's do this for lines 4 and 6 of the original proof as well:
\begin{array}{lll} 1& (\neg \neg P \to ((P \to \neg \neg P) \to \neg \neg P) \to ((\neg \neg P \to (P \to \neg \neg P)) \to (\neg \neg P \to \neg \neg P)) & Axiom 2\\ 2& \neg \neg P \to ((P \to \neg \neg P & Axiom \ 1\\ 3&(\neg \neg P \to (P \to \neg \neg P)) \to (\neg \neg P \to \neg \neg P) & MP \ 1,2\\ 4&\neg \neg P \to (P \to \neg \neg P) & Axiom \ 1\\ 5&\neg \neg P \to \neg \neg P & MP \ 3,4\\ 6&\neg \neg P \to (\neg \neg \neg \neg P \to \neg \neg P) & Axiom \ 1\\ 7&(\neg \neg P \to (\neg \neg \neg \neg P \to \neg \neg P)) \to (\neg \neg P \to (\neg \neg P \to (\neg \neg \neg \neg P \to \neg \neg P)))& Axiom \ 1\\ 8&\neg \neg P \to (\neg \neg P \to (\neg \neg \neg \neg P \to \neg \neg P)) & MP \ 6,7\\ ...\\ 11&\neg \neg P \to (\neg \neg \neg \neg P \to \neg \neg P) & \\ 12&(\neg \neg \neg \neg P \to \neg \neg P) \to (\neg P \to \neg \neg \neg P) & Axiom \ 3\\ 13&((\neg \neg \neg \neg P \to \neg \neg P) \to (\neg P \to \neg \neg \neg P)) \to (\neg \neg P \to ((\neg \neg \neg \neg P \to \neg \neg P) \to (\neg P \to \neg \neg \neg P)))& Axiom \ 1\\ 14&\neg \neg P \to ((\neg \neg \neg \neg P \to \neg \neg P) \to (\neg P \to \neg \neg \neg P)) & MP \ 12, 13\\ ...\\ 17&\neg \neg P \to (\neg P \to \neg \neg \neg P) & \\ 18&(\neg P \to \neg \neg \neg P) \to (\neg \neg P \to P) & Axiom \ 3\\ 19&((\neg P \to \neg \neg \neg P) \to (\neg \neg P \to P)) \to (\neg \neg P \to ((\neg P \to \neg \neg \neg P) \to (\neg \neg P \to P))) & Axiom \ 1\\ 20&\neg \neg P \to ((\neg P \to \neg \neg \neg P) \to (\neg \neg P \to P)) & MP \ 18, 19\\ ...\\ 23&\neg \neg P \to (\neg \neg P \to P)& \\ ...\\ 26&\neg \neg P \to P & \\ \end{array}
Third, and finally, we need to transform any applications of MP in the original proof to the new p[roof. For this, we use Axiom 2. Indeed, Axiom 2 can be seen as a one-line statement of a 'conditionalized Modus Ponens'. Let's see how this works. In the oerignal proof, line 3 was inferred using MP from lines 1 and 2. So, in the new proof, we want to infer line $11$ from lines $5$ and %8$. Again, for this, we use Axiom 2. Let's just highlight those very statements so you can focus on that:
\begin{array}{lll} 5&\neg \neg P \to \neg \neg P & \\ 8&\neg \neg P \to (\neg \neg P \to (\neg \neg \neg \neg P \to \neg \neg P)) & \\ 9&(\neg \neg P \to (\neg \neg P \to (\neg \neg \neg \neg P \to \neg \neg P))) \to ((\neg \neg P \to \neg \neg P) \to (\neg \neg P \to (\neg \neg \neg \neg P \to \neg \neg P))&Axiom \ 2\\ 10&(\neg \neg P \to \neg \neg P) \to (\neg \neg P \to (\neg \neg \neg \neg P \to \neg \neg P)& MP \ 9,8\\ 11&\neg \neg P \to (\neg \neg \neg \neg P \to \neg \neg P) & MP \ 10,5\\ \end{array}
See how that works? OK, now let's do the same for the other instances of MP, and we get as our final result:
\begin{array}{lll} 1& (\neg \neg P \to ((P \to \neg \neg P) \to \neg \neg P) \to ((\neg \neg P \to (P \to \neg \neg P)) \to (\neg \neg P \to \neg \neg P)) & Axiom 2\\ 2& \neg \neg P \to ((P \to \neg \neg P & Axiom \ 1\\ 3&(\neg \neg P \to (P \to \neg \neg P)) \to (\neg \neg P \to \neg \neg P) & MP \ 1,2\\ 4&\neg \neg P \to (P \to \neg \neg P) & Axiom \ 1\\ 5&\neg \neg P \to \neg \neg P & MP \ 3,4\\ 6&\neg \neg P \to (\neg \neg \neg \neg P \to \neg \neg P) & Axiom \ 1\\ 7&(\neg \neg P \to (\neg \neg \neg \neg P \to \neg \neg P)) \to (\neg \neg P \to (\neg \neg P \to (\neg \neg \neg \neg P \to \neg \neg P)))& Axiom \ 1\\ 8&\neg \neg P \to (\neg \neg P \to (\neg \neg \neg \neg P \to \neg \neg P)) & MP \ 6,7\\ 9&(\neg \neg P \to (\neg \neg P \to (\neg \neg \neg \neg P \to \neg \neg P))) \to ((\neg \neg P \to \neg \neg P) \to (\neg \neg P \to (\neg \neg \neg \neg P \to \neg \neg P))&Axiom \ 2\\ 10&(\neg \neg P \to \neg \neg P) \to (\neg \neg P \to (\neg \neg \neg \neg P \to \neg \neg P)& MP \ 9,8\\ 11&\neg \neg P \to (\neg \neg \neg \neg P \to \neg \neg P) & MP \ 10,5\\ 12&(\neg \neg \neg \neg P \to \neg \neg P) \to (\neg P \to \neg \neg \neg P) & Axiom \ 3\\ 13&((\neg \neg \neg \neg P \to \neg \neg P) \to (\neg P \to \neg \neg \neg P)) \to (\neg \neg P \to ((\neg \neg \neg \neg P \to \neg \neg P) \to (\neg P \to \neg \neg \neg P)))& Axiom \ 1\\ 14&\neg \neg P \to ((\neg \neg \neg \neg P \to \neg \neg P) \to (\neg P \to \neg \neg \neg P)) & MP \ 12, 13\\ 15&(\neg \neg P \to ((\neg \neg \neg \neg P \to \neg \neg P) \to (\neg P \to \neg \neg \neg P))) \to ((\neg \neg P \to (\neg \neg \neg \neg P \to \neg \neg P)) \to (\neg \neg P \to (\neg P \to \neg \neg \neg P))&Axiom \ 2\\ 16&(\neg \neg P \to (\neg \neg \neg \neg P \to \neg \neg P)) \to (\neg \neg P \to (\neg P \to \neg \neg \neg P))&MP \ 15,14\\ 17&\neg \neg P \to (\neg P \to \neg \neg \neg P) & MP \ 16,11\\ 18&(\neg P \to \neg \neg \neg P) \to (\neg \neg P \to P) & Axiom \ 3\\ 19&((\neg P \to \neg \neg \neg P) \to (\neg \neg P \to P)) \to (\neg \neg P \to ((\neg P \to \neg \neg \neg P) \to (\neg \neg P \to P))) & Axiom \ 1\\ 20&\neg \neg P \to ((\neg P \to \neg \neg \neg P) \to (\neg \neg P \to P)) & MP \ 18, 19\\ 21&(\neg \neg P \to ((\neg P \to \neg \neg \neg P) \to (\neg \neg P \to P))) \to ((\neg \neg P \to (\neg P \to \neg \neg \neg P)) \to (\neg \neg P \to (\neg \neg P \to P))) & Axiom \ 2\\ 22&(\neg \neg P \to (\neg P \to \neg \neg \neg P)) \to (\neg \neg P \to (\neg \neg P \to P))& MP \ 21,20\\ 23&\neg \neg P \to (\neg \neg P \to P)& MP \ 22, 17\\ 24&(\neg \neg P \to (\neg \neg P \to P)) \to ((\neg \neg P \to \neg \neg P) \to (\neg \neg P \to P)) & Axiom \ 2\\ 25&(\neg \neg P \to \neg \neg P) \to (\neg \neg P \to P)& MP \ 24, 23\\ 26&\neg \neg P \to P & MP \ 25, 5\\ \end{array}
And there you have it! A completely formal proof!
To end, a couple of notes:
\begin{array}{lll} 1& (\neg \neg P \to ((P \to \neg \neg P) \to \neg \neg P) \to ((\neg \neg P \to (P \to \neg \neg P)) \to (\neg \neg P \to \neg \neg P)) & Axiom 2\\ 2& \neg \neg P \to ((P \to \neg \neg P & Axiom \ 1\\ 3&(\neg \neg P \to (P \to \neg \neg P)) \to (\neg \neg P \to \neg \neg P) & MP \ 1,2\\ 4&\neg \neg P \to (P \to \neg \neg P) & Axiom \ 1\\ 5&\neg \neg P \to \neg \neg P & MP \ 3,4\\ 6&\neg \neg P \to (\neg \neg \neg \neg P \to \neg \neg P) & Axiom \ 1\\ 7&(\neg \neg \neg \neg P \to \neg \neg P) \to (\neg P \to \neg \neg \neg P) & Axiom \ 3\\ 8&((\neg \neg \neg \neg P \to \neg \neg P) \to (\neg P \to \neg \neg \neg P)) \to (\neg \neg P \to ((\neg \neg \neg \neg P \to \neg \neg P) \to (\neg P \to \neg \neg \neg P)))& Axiom \ 1\\ 9&\neg \neg P \to ((\neg \neg \neg \neg P \to \neg \neg P) \to (\neg P \to \neg \neg \neg P)) & MP \ 7, 8\\ 10&(\neg \neg P \to ((\neg \neg \neg \neg P \to \neg \neg P) \to (\neg P \to \neg \neg \neg P))) \to ((\neg \neg P \to (\neg \neg \neg \neg P \to \neg \neg P)) \to (\neg \neg P \to (\neg P \to \neg \neg \neg P))&Axiom \ 2\\ 11&(\neg \neg P \to (\neg \neg \neg \neg P \to \neg \neg P)) \to (\neg \neg P \to (\neg P \to \neg \neg \neg P))&MP \ 10,9\\ 12&\neg \neg P \to (\neg P \to \neg \neg \neg P) & MP \ 11,6\\ 13&(\neg P \to \neg \neg \neg P) \to (\neg \neg P \to P) & Axiom \ 3\\ 14&((\neg P \to \neg \neg \neg P) \to (\neg \neg P \to P)) \to (\neg \neg P \to ((\neg P \to \neg \neg \neg P) \to (\neg \neg P \to P))) & Axiom \ 1\\ 15&\neg \neg P \to ((\neg P \to \neg \neg \neg P) \to (\neg \neg P \to P)) & MP \ 13, 14\\ 16&(\neg \neg P \to ((\neg P \to \neg \neg \neg P) \to (\neg \neg P \to P))) \to ((\neg \neg P \to (\neg P \to \neg \neg \neg P)) \to (\neg \neg P \to (\neg \neg P \to P))) & Axiom \ 2\\ 17&(\neg \neg P \to (\neg P \to \neg \neg \neg P)) \to (\neg \neg P \to (\neg \neg P \to P))& MP \ 16,15\\ 18&\neg \neg P \to (\neg \neg P \to P)& MP \ 17, 12\\ 19&(\neg \neg P \to (\neg \neg P \to P)) \to ((\neg \neg P \to \neg \neg P) \to (\neg \neg P \to P)) & Axiom \ 2\\ 20&(\neg \neg P \to \neg \neg P) \to (\neg \neg P \to P)& MP \ 19, 18\\ 21&\neg \neg P \to P & MP \ 20, 5\\ \end{array}