Derive $P \to \neg \neg P$ in a structure with not and implies
Yes, this is possible, but the proof is not short and simple. From a birds-eye view, the trick is to start by proving double-negation elimination: $$ \neg\neg Q \to Q $$ This requires two instances of axiom 2: $$ (\neg\neg\neg\neg Q \to \neg\neg Q) \to (\neg Q \to \neg\neg\neg Q) \\ (\neg Q \to \neg\neg\neg Q) \to (\neg\neg Q \to Q) $$ If we temporarily assume $\neg\neg Q$, then by axiom 1 we have $\neg\neg\neg\neg Q\to\neg\neg Q$, and by the two implications above get get $\neg\neg Q\to Q$. Since we're still assuming $\neg\neg Q$, we can get $Q$. Now the deduction theorem applied to this reasoning then gives a proof of $\neg\neg Q\to Q$ without any additional assumptions.
To arrive at double-negation introduction, set $Q := \neg P$. The elimination formula we have just proved is then $$ \neg\neg\neg P \to \neg P $$ and a final appeal to axiom 2 converts this into the desired $$ P \to \neg\neg P $$
Unfolding the deduction theorem (and optimising a bit by hand) gives us this somewhat formidable proof, where several internal application of modus ponens have been omitted:
$$ \begin{array}{rll} \\ 1. & \neg^3P \to (\neg^5 P \to \neg^3 P) & \mathrm{Ax.}1 \\ 2. & (\neg^5P \to \neg^3P) \to (\neg^2P\to\neg^4P) & \mathrm{Ax.}2 \\ 3. & \neg^3P \to (\neg^5P \to \neg^3P) \to (\neg^2P\to\neg^4P) & \mathrm{Ax.}1, (2) \\ 4. & \neg^3P \to (\neg^2P \to \neg^4P) & \mathrm{Ax.}3, (3), (1) \\ 5. & (\neg^2P \to \neg^4P) \to (\neg^3P\to\neg P) & \mathrm{Ax.}2 \\ 6. & \neg^3P \to (\neg^2P \to \neg^4P) \to (\neg^3 P\to\neg P) & \mathrm{Ax.}1, (5) \\ 7. & \neg^3P \to (\neg^3P \to \neg P) & \mathrm{Ax.}3, (6), (4) \\ 8. & \neg^3P \to \neg^3P & \mathrm{Ax.}1, \mathrm{Ax.}3 \\ 9. & \neg^3P \to \neg P & \mathrm{Ax.3}, (7), (8) \\ 10. & P\to \neg\neg P & \mathrm{Ax.2}, (9) \end{array} $$
Is it possible to prove this? :--
$$P\to \lnot\lnot P$$
The person who gave me this problem insists it is provable, although it seems to me that such a proof is impossible, as none of the axioms increase the depth of $\lnot$s across the $\to$ (i.e. none of them have a more knotty right-hand-side than left-hand-side).
The mistake in your reasoning is that with the axioms, you can get more $\neg$'s ... for example, if you have $P$, then with axiom $1$, you can get $Q \rightarrow P$ for any $Q$ ... so this $Q$ could have many more $\neg$'s than the $P$, and using Axiom 2, you can get those to the other aside of the conditional.
Now, the actual proof of $P \rightarrow \neg \neg P$ is pretty nasty. In fact, below I'll assume that you can use the Deduction Theorem, which states that for any $\Gamma$, $\varphi$, and $\psi$:
If $\Gamma \cup \{ \varphi \} \vdash \psi$, then $\Gamma \vdash \varphi \rightarrow \psi$
Now for the proof. First, let's prove: $\phi \to \psi, \psi \to \chi, \phi \vdash \chi$:
$\phi \to \psi$ Premise
$\psi \to \chi$ Premise
$\phi$ Premise
$\psi$ MP 1,3
$\chi$ MP 2,4
By the Deduction Theorem, this gives us Hypothetical Syllogism (HS): $\phi \to \psi, \psi \to \chi \vdash \phi \to \chi$
Now let's prove the general principle that $\neg \phi \vdash (\phi \to \psi)$:
$\neg \phi$ Premise
$\neg \phi \to (\neg \psi \to \neg \phi)$ Axiom1
$\neg \psi \to \neg \phi$ MP 1,2
$(\neg \psi \to \neg \phi) \to (\phi \to \psi)$ Axiom2
$\phi \to \psi$ MP 3,4
With the Deduction Theorem, this means $\vdash \neg \phi \to (\phi \to \psi)$ (Duns Scotus Law)
Let's use Duns Scotus to show that $\neg \phi \to \phi \vdash \phi$
$\neg \phi \to \phi$ Premise
$\neg \phi \to (\phi \to \neg (\neg \phi \to \phi))$ (Duns Scotus Law)
$(\neg \phi \to (\phi \to \neg (\neg \phi \to \phi))) \to ((\neg \phi \to \phi) \to (\neg \phi \to \neg (\neg \phi \to \phi)))$ Axiom3
$(\neg \phi \to \phi) \to (\neg \phi \to \neg (\neg \phi \to \phi))$ MP 2,3
$\neg \phi \to \neg (\neg \phi \to \phi)$ MP 1,4
$(\neg \phi \to \neg (\neg \phi \to \phi)) \to ((\neg \phi \to \phi) \to \phi)$ Axiom2
$(\neg \phi \to \phi) \to \phi$ MP 5,6
$\phi$ MP 1,7
By the Deduction Theorem, this means $\vdash (\neg \phi \to \phi) \to \phi$ (Law of Clavius)
Using Duns Scotus and the Law of Clavius, we can now show that $ \neg \neg \phi \vdash \phi$:
$\neg \neg \phi$ Premise
$\neg \neg \phi \to (\neg \phi \to \phi)$ Duns Scotus
$\neg \phi \to \phi$ MP 1,2
$(\neg \phi \to \phi) \to \phi$ Law of Clavius
$\phi$ MP 3,4
By the Deduction Theorem, this also means that $\vdash \neg \neg \phi \to \phi$ (DN Elim)
Now we can prove $\vdash \phi \to \neg \neg \phi$ (DN Intro) as well:
$\neg \neg \neg \phi \to \neg \phi$ (DN Elim)
$(\neg \neg \neg \phi \to \neg \phi) \to (\phi \to \neg \neg \phi)$ Axiom 2
$\phi \to \neg \neg \phi$ MP 1,2