Is this proof correct? (natural deduction)

Question

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

Answer 1

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.

Answer 2

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.

Done.

Answer 3

$\def\fitch#1#2{\begin{array}{|l}#1\\\hline#2\end{array}}$

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.

Answer 4

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}