Help proving $ \sim \sim (p \to q),\sim \sim p \vdash \sim \sim q $ with intuitionistic axioms

Question

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.

Answer 1

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:

1. Assume $\neg q$ (this corresponds to $\lambda c$).
2. Assume $p\to q$ (this corresponds to $\lambda f$).
3. Assume $p$ (this corresponds to $\lambda x$).
4. Prove $q$ (easily by assumptions 2 and 3 -- this corresponds to the expression $f\; x$).

5. 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).

6. 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).

7. 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.

Answer 2

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)$.

Answer 3

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.

Answer 4

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