Help proving $ \sim \sim (p \to q),\sim \sim p \vdash \sim \sim q $ with intuitionistic axioms Rule
modus ponens: $ p, p \to q \vdash q $
Axioms
A1  $ p \to (q \to p) $
A2  $ (p \to (q \to r)) \to ((p \to q) \to (p \to r)) $
A3  $ (p \land q) \to p $
A4  $ (p \land q) \to q $
A5  $ p \to (q \to (p \land q)) $
A6  $ p \to (p \lor q) $
A7  $ q \to (p \lor q) $
A8  $ (p \to r) \to ((q \to r) \to ((p \lor q) \to r)) $
A9  $ (p \to q) \to ((p \to \sim q) \to \sim p) $
A10 $ \sim p \to (p \to q) $
Rule I have derived: $ p \to q, q \to r \vdash p \to r $
Derived meta-rule (deduction theorem): $ \Gamma,p \vdash q $ implies $ \Gamma \vdash p \to q $
Theorems I have proven
T1  $ p \to \sim \sim p $
T2  $ (p \to q) \to (\sim q \to \sim p) $
T3  $ p \to (\sim p \to q) $
T4  $ \sim \sim (\sim \sim p \to p) $
T5  $ \sim \sim \sim p \to \sim p $
I am guessing axioms 3,4,5,6,7 and 8 are not needed for the proof.
On the other hand I believe A10 and T3 are critical.
Thanks for any help on this.
 A: Since we have the deduction theorem, the Curry-Howard isomorphism comes to the rescue.
Intuitionistic negation $\neg \phi$ is morally equivalent to $\phi\to\bot$, where $\bot$ is a contradiction. And double-negation corresponds via Curry-Howard to programming in continuation-passing style. So if we have the assumptions
$$ F: \neg\neg(p\to q) \qquad X:\neg\neg p $$
and want to generate $\neg\neg q$, it is natural to try to write down a CPS transform of the application $f\;x$, which gives
$$ \lambda c. F\;(\lambda f. X\;(\lambda x. c(f\; x))) : \neg\neg q$$
The typing tree for this expression can be unfolded to a proof using the deduction theorem several times:


*

*Assume $\neg q$ (this corresponds to $\lambda c$).

*Assume $p\to q$ (this corresponds to $\lambda f$).

*Assume $p$ (this corresponds to $\lambda x$).

*Prove $q$ (easily by assumptions 2 and 3 -- this corresponds to the expression $f\; x$).

*Discharge assumption 3 to get $p\to q$. We also have $p\to \neg q$ (via A1 and assumption 1). Then apply A9 to conclude $\neg p$.
(This corresponds to $\lambda x.c(f\; x)$ of type $p\to\bot\equiv \neg p$. Because your proof system doesn't have an explicit $\bot$ it was necessary to get the contradiction $q$, $\neg q$ out of the deduction theorem in two pieces, and the application of $c$ to $f\;x$ gets hoisted out to happen "outside the lambdas". A more C-H-friendly but less minimal proof strategy would have been to prove $(x\to(y\land \neg y))\to\neg x$ as a general theorem first).

*Discharge assumption 2 to get $(p\to q)\to \neg p$. We also have $(p\to q)\to\neg\neg p$ since $\neg\neg p$ is generally assumed. Therefore A9 concludes $\neg(p\to q)$.
(This corresponds to $\lambda f.x\;(\lambda x.c(f\; x))$ of type $(p\to q)\to \bot\equiv \neg(p\to q)$, just as the previous step).

*Finally, discharge assumption 1 to get $\neg q\to\neg(p\to q)$. We also have $\neg q\to\neg\neg(p\to q)$ since $\neg\neg (p\to q)$ is generally assumed. Therefore A9 concludes $\neg\neg q$. Q.E.D.


After a bit of squinting at this construction it should now be clear how we can systematically lift any proof of $\phi_1,\ldots,\phi_k\vdash \psi$ to a proof of $\neg\neg\phi_1,\ldots,\neg\neg\phi_k\vdash\neg\neg\psi$. There will be $k+1$ nested invocations of the deduction theorem, and the original proof is inserted in place of step (4) in the above sketch.
A: The about 40 lines long derivation seems to me a little bit longer than needed ...
1) $\lnot \lnot (p→q)$ --- premise
2) $\lnot \lnot p$ --- premise
3) $\vdash \lnot \lnot (p→q) → [\lnot q \rightarrow \lnot \lnot (p→q)]$ --- Axiom 1
4) $\lnot q \rightarrow \lnot \lnot (p→q)$ --- from 1) and 3) by modus ponens
5) $\vdash \lnot \lnot p → [(p \rightarrow q) \rightarrow \lnot \lnot p]$ --- Axiom 1
6) $(p \rightarrow q) \rightarrow \lnot \lnot p$ --- from 2) and 5) by modus ponens
7) $\lnot q$ ---- assumed [a]
8) $p→q$ --- assumed [b]
9) $\lnot q \rightarrow \lnot p$ --- from 8) by T2 and modus ponens
10) $\lnot p$ --- from 7) and 9) by modus ponens
11) $(p \rightarrow q) \rightarrow \lnot p$ --- from 8) and 10) by Deduction Th, discharging [b]
12) $\lnot (p \rightarrow q)$ --- from 11) and 6) and Axiom 9 by modus ponens twice
13) $\lnot q \rightarrow \lnot (p \rightarrow q)$ --- from 7) and 12) and Deduction Th, discharging [a]
14) $\lnot \lnot q$ --- from 4) and 13) and Axiom 9 by modus ponens twice.
Thus, form 1), 2) and 14) :


$\lnot \lnot (p→q), \lnot \lnot p \vdash \lnot \lnot q$.


A: Try proving the very useful metatheorem: $\Gamma, p \vdash \sim q$ iff $\Gamma, \sim\sim p \vdash \sim q$.
You can use this to turn the easily proven $ p \to q, p \vdash q $ into something that can be composed with your theorem T1 to get your goal.
A: Using T2 twice we have $ (p\to q) \to (\sim\sim p \to \sim\sim q)$. Use this for 'itself' ($p':=p\to q$ and $q':=(\sim\sim p\to \sim\sim q)$, we get
$$ \sim\sim(p\to q)\to\sim\sim(\sim\sim p\to \sim\sim q) $$
then use something like T4 to get: $\sim\sim(p\to q) \to (\sim\sim p\to\sim\sim q)$.
A: Thank you for all the reponses.
I have focused on Mr. Makholm's helpful workup. Although it is true that I don't have access to $ \bot $ It seems to me that his steps 3-5 are not necessary:
Derive rule A: $ \sim q \vdash (p \to q) \to \sim p $
1 $ \sim q $ hypothesis
2 $ p \to q $ hypothesis
3 $ \sim q \to (p \to \sim q) $ A1
4 $ p \to \sim q $ 1,3 modus ponens
5 $ (p \to q) \to ((p \to \sim q) \to \sim p) $ A9
6 $ (p \to q) \to ~p $ 2,5 modus ponens
7 $ \sim p $ 4,6 modus ponens
8 $ \sim q, p \to q \vdash \sim p $ 1-7
9 $ \sim q \vdash (p \to q) \to \sim p $ 8 deduction theorem
Derive $ \sim \sim (p \to q),\sim \sim p \vdash \sim \sim q $
1 $ \sim \sim (p \to q) $ hypothesis
2 $ \sim \sim p $ hypothesis
3 $ \sim q $ hypothesis
4 $ \sim q \vdash \sim \sim (p \to q) $ 1
5 $ p \to q \vdash \sim \sim p $ 2
6 $ \sim q \to \sim \sim (p \to q) $ 4 deduction theorem
7 $ (p \to q) \to \sim \sim p $ 5 deduction theorem
8 $ (p \to q) \to \sim p $ 3 rule A
9 $ ((p \to q) \to \sim p) \to ((p \to q) \to \sim \sim p) \to \sim (p \to q)) $ A9
10 $ (p \to q) \to \sim \sim p) \to \sim (p \to q) $ 8,9 modus ponens
11 $ \sim (p \to q) $ 7,10 modus ponens
12 $ \sim q \vdash \sim (p \to q) $ 3-11
13 $ \sim q \to \sim (p \to q) $ 12 deduction theorem
14 $ ( \sim q \to \sim (p \to q)) \to (( \sim q \to \sim \sim (p \to q)) \to \sim \sim q) $ A9
15 $ ( \sim q \to \sim \sim (p \to q)) \to \sim \sim q $ 13,14 modus ponens
16 $ \sim \sim q $ 6,15 modus ponens
17 $ \sim \sim (p \to q),\sim \sim p \vdash \sim \sim q $ 1-16
My only points of discomfort are steps 4 and 5 of my second derivation (Mr. Makholm's "general assumptions" of his steps 6 and 7). They presume the meta-rule $ \varnothing  \vdash p $ implies $ \Gamma \vdash p $. I suppose this should be easy enough to prove however.
I think I found a way to avoid using the meta rule $ \varnothing \vdash p $ implies $ \Gamma \vdash p $ 
To obtain step 6 of my second derivation without using step 4:
Prove $ \sim q \to \sim \sim (p \to q) $
1 $ \sim \sim (p \to q) $ hypothesis
2 $ \sim \sim (p \to q) \to ( \sim (p \to q) \to q) $ A10
3 $  \sim (p \to q) \to q $ 1,2 modus ponens
4 $ (\sim (p \to q) \to q) \to ( \sim q \to \sim \sim (p \to q)) $ T2
5 $ \sim q \to \sim \sim (p \to q) $ 3,4 modus ponens
To obtain step 7 of my second derivation without using step 5:
Prove $ (p \to q) \to \sim \sim p $
1 $ \sim \sim (p \to q) $ hypothesis
2 $ \sim \sim p $ hypothesis
3 $ p \to q $ hypothesis
4 $ \sim \sim p \to ( \sim p \to \sim (p \to q)) $ A10
5 $ \sim p \to \sim (p \to q) $ 2,4 modus ponens
6 $ (\sim p \to \sim (p \to q)) \to ( \sim \sim (p \to q) \to \sim \sim p) $ T2
7 $ \sim \sim (p \to q) \to \sim \sim p $ 5,6 modus ponens
8 $ \sim \sim p $ 1,7 modus ponens
9 $ p \to q \vdash \sim \sim p $ 3-8
10 $ (p \to q) \to \sim \sim p $ 9 deduction theorem
