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$ – Taroccoesbrocco Mar 17 '18 at 23:19

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$ – openingceremony Mar 17 '18 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$ – Taroccoesbrocco Mar 17 '18 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$ – Graham Kemp Mar 18 '18 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$ – Taroccoesbrocco Mar 18 '18 at 0:15
  • 2
    $\begingroup$ @Taroccoesbrocco Indentation helps highlight the assumption and discarge for subproofs. $\endgroup$ – Graham Kemp Mar 18 '18 at 0:19

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$ – openingceremony Mar 17 '18 at 23:33
  • $\begingroup$ @openingceremony Option 3 then .. yeah, I figured I should have put that one first :) $\endgroup$ – Bram28 Mar 17 '18 at 23:34


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$ – openingceremony Mar 17 '18 at 23:46
  • $\begingroup$ Ah, then double negation would get you there. $\endgroup$ – Graham Kemp Mar 17 '18 at 23:55
  • $\begingroup$ PS: which negation elimination/introduction rules do you use? Some authors use different versions. $\endgroup$ – Graham Kemp Mar 18 '18 at 0:00
  • $\begingroup$ Nice formatting! $\endgroup$ – Bram28 Mar 18 '18 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 '18 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$ – Derek Elkins left SE Mar 18 '18 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$ – Taroccoesbrocco Mar 18 '18 at 0:25
  • $\begingroup$ @DerekElkins - Good and illuminating remark. Thank you so much! $\endgroup$ – Taroccoesbrocco Mar 18 '18 at 0:29
  • $\begingroup$ @Taroccoesbrocco thanks for pointing out the typo! nice formatting of your proofs! $\endgroup$ – Bram28 Mar 18 '18 at 0:35

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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