How to prove ~~A,A→B⊢B without double negation elimination

Question

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.

Answer 1

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.

Answer 2

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

1. [[A -> Q] -> Q]. Then assume
2. [B -> Q]. Then assume
3. [A -> B]

Now, can you deduce Q?