How to prove ~~A,A→B⊢B without double negation elimination This is an exercise from Mathematical Logic: A First Course by Joel W. Robbin.
The formal language PI, is obtained from the formal language P by deleting ⊥ from the set of primitive symbols and deleting rule (W2) (which says that ⊥ is a wff) in the definition of wff. The axiom schemas for PI are A$\rightarrow$[B$\rightarrow$A], [A$\rightarrow$[B$\rightarrow$C]]$\rightarrow$[[A$\rightarrow$B]$\rightarrow$[A$\rightarrow$C]], and [[A$\rightarrow$B]$\rightarrow$A]$\rightarrow$A (Peirce’s law), and the rule of inference of PI is $modus\;
ponens$. The definitions of deduction in PI, deduction from hypotheses in PI,
and theorem of P, are $mutatis\;mutandis$ the same as for P. The notation $\vdash_\mbox I$ A
means A is a theorem of PI, and QA is an abbreviation for [A$\rightarrow$Q], In unabbreviating an expression which uses this abbreviation more than once use
association to the right; that is, QQA stands for QA$\rightarrow$Q rather than A$\rightarrow$QQ. Notice that the wff QA behaves very much like the wff ~A:=A$\rightarrow\bot$.
Show that the deduction theorem holds for P, and prove the following
theorem schemas.
(1) $\vdash_\mbox I[\mbox A\rightarrow \mbox B]\rightarrow[[\mbox B\rightarrow \mbox C]\rightarrow[\mbox A\rightarrow\mbox C]]$
(2) $\vdash_\mbox I[\mbox A\rightarrow\mbox B]\rightarrow[\mbox{QB}\rightarrow\mbox{QA}]$
(3) $\vdash_\mbox I\mbox A\rightarrow\mbox{QQA}$
(4) $\vdash_\mbox I\mbox{QQQA}\rightarrow\mbox{QA}$
(5) $\vdash_\mbox I\mbox{QQB}\rightarrow\mbox{QQ[A}\rightarrow\mbox B]$
(6) $\vdash_\mbox I\mbox{QQA}\rightarrow[\mbox{QB}\rightarrow\mbox{Q[A}\rightarrow\mbox B]]$...
I am now stuck at (6). Using the deduction theorm, I can convert (6) into $\mbox{QQA}\vdash_\mbox I\mbox{QB}\rightarrow\mbox{Q[A}\rightarrow\mbox B]$ and further into $\mbox{QQA}\vdash_\mbox I[\mbox A\rightarrow\mbox B]\rightarrow\mbox B$ by (2) and modus ponens. But I don't know how to proceed without double negation elimination to deal with that QQA.
Any help will be appreciated.
 A: I can show you how to solve (6) using type theory.

(6) $$((A \to Q) \to Q) \to (B \to Q) \to (A \to B) \to Q$$

Proving this is equivalent to finding a lambda expression available with the above type. (You can assume the existance of an expression of the type $(((g \to h) \to g) \to g$, but that is fortunately not necessary in this case).  By trial and error, an expression can be found:
$$\lambda xyz~.~x(\lambda v.y(zv)) \tag{P1a}$$
$$\begin{array} {c|l} \text{variable} & \text{type} \\ \hline
x & ((A \to Q) \to Q \\
y & B \to Q \\
z & A \to B \\
v & A
\end{array} \tag{P1b}$$
This allows you to construct a proof if you have deduction theorem available:
$$\begin{array} {r|ll}
%
(1) & ((A \to Q) \to Q) & \text{Premise} \\
%
(2) & B \to Q & \text{Premise} \\
%
(3) & A \to B & \text{Premise} \\
%
(4) & A & \text{Premise} \\
%
(5) & B & \text{Modus Ponens 3 , 4} \\
%
(6) & Q & \text{Modus Ponens 2 , 5} \\
%
(7) & A \to Q & \text{Deduction theorem on 6 removing premise 4} \\
%
(8) & Q & \text{Modus Ponens 1 , 7} \\
%
(9) & (A \to B) \to Q & \text{Deduction theorem on 8 removing premise 3} \\
%
(10) & (B \to Q) \to (A \to B) \to Q & \text{Deduction theorem on 9 removing premise 2} \\
%
(11) & ((A \to Q) \to Q) \to (B \to Q) \to (A \to B) \to Q & \text{Deduction theorem on 10 removing premise 1} \\
%
\end{array}$$
And if you don't have the deduction theorem immediately available, then the proof is very very long.
A: QQA stands for [QA -> Q].  QA is an abbreviation for [A -> Q].  Thus,
QQA stands for [[A -> Q] -> Q], correct?
So, if you expand out (6), without the meta-logical $\vdash$$_I$, you end up with (and add some points for emphasis) the following
[.[[A -> Q] -> Q]. -> [:[B -> Q]: -> [;[A -> B]; -> Q]]], correct?
Thus, assume 


*

*[[A -> Q] -> Q].  Then assume 

*[B -> Q].  Then assume

*[A -> B]


Now, can you deduce Q?
