I'm working through The Science of Programming by David Gries. This question is #18 in section 3.3.

Prove $((P \land \lnot Q) \to Q) \to (P \to Q)$

Using the natural deduction system here is my proof.

  1. $(P \land \lnot Q) \to Q)$ (premise)

  2. From $P$ infer $Q$ (subproof)

    • 2.1 $P$ (premise)

    • 2.2 From $\lnot Q$ infer $Q$ (subproof)

    • 2.2.1 $\lnot Q$ (premise)

    • 2.2.2 $P \land \lnot Q$ ($\land$-Introduction, 2.1, 2.2.1)

    • 2.2.3 $Q$ ($\to$-E, 1, 2.2.2)

  3. $P \to Q$ ($\to$-I, 2)

Is this correct? I feel like I'm really stretching in trying to prove $P\to Q$ especially with the subproof of $\lnot Q \to Q$.

  • $\begingroup$ Please, use MathJax (i.e. LaTeX commands) for mathematical notations. $\endgroup$ Mar 17, 2018 at 23:19

4 Answers 4


You were right to doubt your proof; it's not quite right.

The main mistake is that you are effectively closing two subproofs at once once you go from 2.2.3 to 3, but you can only close one subproof at a time, in the reverse order in which you opened them.

Also: you need to have line 1 as an assumption of a subproof, and close that subproof once you have reached line 3, so you can infer the whole desired conditional by $\rightarrow$ Intro

So, what to do? Well, that depends on the rules that you have. Let me give you some options:

Option 1:

After 2.2.3 you can get:

2.3 $\neg Q \rightarrow Q$

Then use the Implication equivalence to get $\neg \neg Q \lor Q$ and thus by Double Negation to $Q \lor Q$, and finally by Idempotence to $Q$

Option 2:

First, get $Q \lor \neg Q$ by Law of Excluded Middle. Then again get $\neg Q \rightarrow Q$, but do a second inside subproof where you assume $Q$, reiterate $Q$, close that subproof to get $Q \rightarrow Q$, and then get $Q$ from $\neg Q \rightarrow Q$, $Q \rightarrow Q$, and $Q \lor \neg Q$ by a proof by cases, probably formalized as $\lor $ Elim

Option 3:

Get a contradiction on 2.2.4 between $\neg Q $ and $Q$, and thus conclude $\neg \neg Q$ by a proof by contradiction (probably formalized by $\neg \ Intro$), and thus the $Q$ you really want.

  • $\begingroup$ Thanks, for this chapter's exercises the student is expected to use the natural deduction rules given earlier in the chapter to solve a proof. I'll use contradiction to obtain the proof I really want. $\endgroup$ Mar 17, 2018 at 23:33
  • $\begingroup$ @openingceremony Option 3 then .. yeah, I figured I should have put that one first :) $\endgroup$
    – Bram28
    Mar 17, 2018 at 23:34

I would do it slightly differently, but as always people use somewhat different systems for natural deduction.

  • Begin
    • 1) $(P \land \lnot Q) \rightarrow Q$ (ass.)
      • 2) $P$ (ass.)
        • 3) $\lnot Q$ (ass.)
        • 4) $(P \land \lnot Q)$ introduction $\lnot$ from 2,3.
        • 5) $Q$ (modus ponens from 1. and 4.)
        • 6) $\bot$ from $5$ and $3$.
      • 7) $\lnot \lnot Q$ (from introduction $\lnot$ and 3, 6, we drop 3).
      • 8) $Q$ (double negation rule).
    • 9) $P \rightarrow Q$ (from 2,8 and introduction $\to$); we drop 2.
  • 10) $((P \land \lnot Q) \to Q)\to (P \to Q)$ (intro $\to$ 1, 9) we drop 1.


  • $\begingroup$ I was initially heading down this route but was unsure if it made sense to "break down" the initial assumption (1) into its subsequent parts (2, 3). Doing this seems much more straightforward. $\endgroup$ Mar 17, 2018 at 23:39
  • $\begingroup$ I don't understand your derivation. In lines 4 and 6 you use the assumption $\lnot Q$ (line 3), but who gave you this assumption? $\endgroup$ Mar 17, 2018 at 23:51
  • 1
    $\begingroup$ You can always assume things for the sake of an argument, @Taroccoesbrocco . In this case the subproof by contradiction demonstrates that we must have $\neg\neg Q$ if the prior assumptions hold ($(P\wedge \neg Q)\to Q$ and $P$. $\endgroup$ Mar 18, 2018 at 0:12
  • $\begingroup$ @GrahamKemp - Oh yes, you're right! I completely misread the derivation, skipping line 7. Sorry. The current presentation is much more readable, well done!. $\endgroup$ Mar 18, 2018 at 0:15
  • 2
    $\begingroup$ @Taroccoesbrocco Indentation helps highlight the assumption and discarge for subproofs. $\endgroup$ Mar 18, 2018 at 0:19


Can you use the Law of Excluded Middle?

$$\fitch{}{\fitch{(P\land\lnot Q)\to Q}{\fitch{P}{\left.\raise{5ex}{Q\vee\lnot Q\\\fitch{Q}{Q}\\Q\to Q}\right\}&\text{add this}\\\fitch{\lnot Q}{P\wedge\lnot Q\\ Q}\\\lnot Q \to Q\\Q}\\P\to Q}\\((P\land\lnot Q)\to Q )\to(P\to Q)}$$

Else there is the double negation path.

$$\fitch{}{\fitch{(P\land\lnot Q)\to Q}{\fitch{P}{\fitch{\lnot Q}{P\wedge\lnot Q\\ Q\\\bot}\\\lnot\lnot Q \\Q }\\P\to Q}\\((P\land\lnot Q)\to Q )\to(P\to Q)}$$

If the falsum symbol is not accepted this can be modified to introduce negation via $X\to\neg Y, X\to Y\vdash \neg X$

$$\fitch{}{\fitch{(P\land\lnot Q)\to Q}{\fitch{P}{\fitch{\lnot Q}{\neg Q}\\\lnot Q\to\lnot Q\\\fitch{\lnot Q}{P\wedge\lnot Q\\ Q}\\\neg Q\to Q\\\lnot\lnot Q \\Q }\\P\to Q}\\((P\land\lnot Q)\to Q )\to(P\to Q)}$$

I'll leave the justifications to you.

  • $\begingroup$ For this specific chapter we are not expected to use laws like excluded middle and de morgan to solve proofs. The laws here are introduction and elimination of operators (and, or, not, implies, equal). That's why my (wrong) answer was structured this way. Thanks for additional clarification though. $\endgroup$ Mar 17, 2018 at 23:46
  • $\begingroup$ Ah, then double negation would get you there. $\endgroup$ Mar 17, 2018 at 23:55
  • $\begingroup$ PS: which negation elimination/introduction rules do you use? Some authors use different versions. $\endgroup$ Mar 18, 2018 at 0:00
  • $\begingroup$ Nice formatting! $\endgroup$
    – Bram28
    Mar 18, 2018 at 0:37

Your attempt of derivation is wrong because in your subproof 2 you can't have the hypothesis $\lnot Q$, you are just assuming that $(P \land \lnot Q) \to Q$.

I think $((P \land \lnot Q) \to Q) \to (P \to Q)$ is provable only in classical logic, not in weaker logics such as the intuitionistic one. For instance, you can use the Law of Excluded Middle (or some equivalent formula provable only in classical logic) in your derivation in natural deduction:

\begin{align} \dfrac{\dfrac{\dfrac{Q \lor \lnot Q \qquad [Q]^1 \qquad \dfrac{[(P \land \lnot Q) \to Q]^3 \qquad \dfrac{[P]^2 \qquad [\lnot Q]^1}{P \land \lnot Q}\land_i}{Q}\to_e}{Q}\lor_e^1}{P\to Q}\to_i^2}{((P \land \lnot Q) \to Q) \to (P \to Q)}\to_i^3 \end{align}

where the Law of Excluded Middle $Q \lor \lnot Q$ is provable in classical natural deduction as follows:

\begin{align} \dfrac{\dfrac{[\lnot (Q \lor \lnot Q)]^2 \qquad \dfrac{\dfrac{\dfrac{[\lnot (Q \lor \lnot Q)]^2 \qquad \dfrac{[Q]^1}{Q \lor \lnot Q}\lor_{i_L}}{\bot}}{\lnot Q}\lnot_i^1}{Q \lor \lnot Q}\lor_{i_R}}{\bot}\lnot_e}{Q \lor \lnot Q}\text{raa}^2 \end{align}

  • $\begingroup$ I gave two other options ... it all depends on what rules the OP has available though $\endgroup$
    – Bram28
    Mar 17, 2018 at 23:41
  • 1
    $\begingroup$ Choose $P=\neg\neg Q$ and you quickly get double negation elimination as a consequence which shows that you are correct that this is only provable in a classical logic. $\endgroup$ Mar 18, 2018 at 0:24
  • $\begingroup$ @Bram28 - Yes, you're right. I think at the beginning of your option 2 (Law of Excluded Middle) there is a typo, a $\lnot$ is missing. $\endgroup$ Mar 18, 2018 at 0:25
  • $\begingroup$ @DerekElkins - Good and illuminating remark. Thank you so much! $\endgroup$ Mar 18, 2018 at 0:29
  • $\begingroup$ @Taroccoesbrocco thanks for pointing out the typo! nice formatting of your proofs! $\endgroup$
    – Bram28
    Mar 18, 2018 at 0:35

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .