One of the reasons is that the Generalization Theorem [see page 117] used in the last step of the proof is not a rule of the calculus, but a so-called meta-theorem.
It is a theorem about $\vdash$, i.e. the derivability relation, and $\vdash$ is not part of the syntax of the calculus [see page 69].
The theorem asserts that (under certain circumstances) a derivation in the calculus exists, but it is not itself a derivation in the calculus.
We can convert the proof provided at page 122 into a "fully formal" derivation following the steps in the proof of the Gen Th, inserting the "missing" steps.
Example : how to remove the first use of Gen Th in step 4 ? We have to use the Case 3 of the proof of the meta-theorem.
In your expanded proof we have to use the universal closure of step 3) :
3a) $\forall x (x=x → (x=y → y=x))$
as well as that of Ax.5 :
4a) $\forall x (x=x).$
Thus :
4b) $\forall x (x=x → (x=y → y=x)) \to (\forall x (x=x) → \forall x (x=y → y=x))$ --- Ax.3
4c) $\forall x (x=x) → \forall x (x=y → y=x))$ --- from 3a) and 4b) by MP
4d) $\forall x (x=y → y=x)$ --- from 4a) and 4c) by MP.
The same procedure must then be used to derive 3a) above from Ax.6 and the universal closure of step 2 (see page 112 : "The logical axioms are then all generalizations of wffs of the following forms [...] : 1. Tautologies; [...]").
In the same way, for the 2nd use of Gen Th.
The same for Rule T [page 118] used in step 3: you have already provided the "elimination" of it inserting into the proof the corresponding elementary propositional steps.
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:
- The systematic transformation algorithm will always work .. but often it will end up doing work that isn't really necessary. For example, we did a lot of work to get to line $11$, but that line is identical to line $6$. So, we can simplify the proof to:
\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}
- These formal proofs are nuts! ... even with possible simplifications .. So this is exactly why in practice we use the Deduction Theorem. Again, not as a rule of inference in an actual formal proof, but rather as theorem to mathematical prove that something is formally provable.
Best Answer
A different derivation ...
1) $∀x(Px → Qx)$ --- premise
2) $∀zPz$ --- premise
3) $∀x(Px → Qx) \to (Pc → Qc)$ --- Axiom 2
4) $∀zPz \to Pc$ --- Axiom 2
5) $Pc → Qc$ --- 1) and 3) by MP
6) $Pc$ --- 2) and 4) by MP