Take the 2-minute tour ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

Rule modus ponens: $ p, p \to q \vdash q $


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.

share|improve this question
Ugh, Hilbert system. By the deduction theorem, to prove your proposition it is enough to show that $\lnot \lnot (p \to q), \lnot \lnot p, \lnot q \vdash \bot$. But $\lnot \lnot p, \lnot q \vdash \lnot q \to \lnot p$, so $\lnot \lnot p, \lnot q \vdash \lnot (\lnot q \to \lnot p)$, and $\lnot (\lnot q \to \lnot p) \vdash \lnot (p \to q)$, etc. –  Zhen Lin Nov 10 '12 at 22:56
I'm not sure about the details of your deductive system, but in most Hilbert-style formalizations a formal proof sequence that proves $\varnothing\vdash p$ is also a proof sequence of $\Gamma \vdash p$. Having more stuff to the left of the turnstile makes it strictly easier for a sequence of formulas to be a valid proof. –  Henning Makholm Nov 11 '12 at 20:23
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. –  Henning Makholm Nov 12 '12 at 0:28

5 Answers 5

up vote 5 down vote accepted

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.

share|improve this answer
Thank you for your observations, I have responded more fully to them by adding to my original posting. –  toph Nov 11 '12 at 20:15
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. –  toph Nov 12 '12 at 0:16

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

share|improve this answer

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

share|improve this answer

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.

share|improve this answer

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

share|improve this answer

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.