6
$\begingroup$

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.

  • 0
    A general tip: It would be easier to navigate if you presented your eventual solution by posting it as an _answer_ rather than editing it into the _question_ (you should see an "Answer Your Question" button at the bottom of the page). Then it would be clearer to readers what the original question that I and the other answers responded to was.2012-11-12

5 Answers 5

5

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.

  • 0
    I think I found a way to avoid using the meta rule $ \varnothing \vdash p $ implies $ \Gamma \vdash p $. I added it to my original posting. Thank you again for your help.2012-11-12
2

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

1

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.

0

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

0

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