Using Natural Deduction to Prove $(P \land Q) \to R \vdash (P \to R) \lor (Q \to R)$

Question

I'm currently using a sequent calculus and natural deduction to prove this derivation. The book I'm using ("Logic" by Tomassi) claims that this can be completed using only 24 lines. Here is what I have so far:

So far I'm stuck as to how to get $(P \land Q)$ so I can use RAA in the space between lines 12-16. I'm not sure if this is the correct path to take but it's the closest I've gotten to solving this problem so far. There are other answers here, but they either contain rules of inference not mentioned in the book so far (DeMorgan's Law, Law of Excluded Middle, Principle of Explosion, etc) or are far beyond 24 lines. Any hints or help would be appreciated.

Answer 1

Here is a proof from https://proofs.openlogicproject.org/ with the restrictions you mentioned in comments.

(Note that in lines 5 through 10, the assumption of $\lnot R$ is never used. Therefore, if you were allowed to use the principle of explosion, I would remove lines 4 and 11, and simply justify line 12 from line 10 using this principle. I also tend to use the "IP" rule from the linked site instead of a combination of ${\rightarrow}I$ and DNE, which would allow dropping line 16.)

Answer 2

Long story short: Don't take the long round about.

You have assumed $\neg(p\to r)$ in you third line with the aim of deriving a contradiction so that you can discharge that assumption to deduce $p\to r$ so that you can derive a contradiction ... That is a bit of a scenic detour.

Should the conditional statement $p\to r$ be derivable, then a conditional proof will be possible. Just do that thing.

Is there a strategy that you use to determine what type of proof you should do? – Cizox

Yes.   When you seek to prove a disjunction from a premise you will either be introducing a disjunction after proving at least one from the two disjuncts directly, or you will be using an indirect proof (proof by contradiction).

Here neither $(p\to r)$ nor $(q\to r)$ seems to be directly implied by $(p\wedge q)\to r$.   If you assume $p$ you cannot immediately infer $r$ from the premise.

This indicates the non-intuitivist route should be attempted: Aim to prove that the consequent cannot be false. $\def\fitch#1#2{~~\begin{array}{|l}#1\\\hline#2\end{array}}$

$$\fitch{(p\wedge q)\to r}{\fitch{\neg((p\to r)\vee(q\to r))}{~\vdots\\\bot}\\\neg\neg((p\to r)\vee(q\to r))\\(p\to r)\vee(q\to r)}$$

Now to do that we try to do what could not be done directly: prove at least one of the disjuncts can be derived under the assumption.   Either should be derivable if the assumption is indeed contradictable, so try the first.

$p\to r$ is a conditional statement, so a Conditional Proof is indicated. Assume $p$ aiming to derive $r$ so that the conditional may be introduced.

$$\fitch{(p\wedge q)\to r}{\fitch{\neg((p\to r)\vee(q\to r))}{\fitch{p}{~\vdots\\ r}\\p\to r\\(p\to r)\vee(q\to r)\\\bot}\\\neg\neg((p\to r)\vee(q\to r))\\(p\to r)\vee(q\to r)}$$

But how to derive $r$ from those assumptions?   Well, again we might be able to prove by contradiction that $r$ cannot be false.

So now, we are aiming for a another contradiction, so perhaps we should try to derive the other disjunct, $q\to r$?

Indeed; since we have already assumed $p$, we can do that.

$$\fitch{(p\wedge q)\to r}{\fitch{\neg((p\to r)\vee(q\to r))}{\fitch{p}{\fitch{\neg r}{\fitch{q}{p\wedge q\\r}\\q\to r\\(p\to r)\vee(q\to r)\\\bot}\\\neg\neg r\\ r}\\p\to r\\(p\to r)\vee(q\to r)\\\bot}\\\neg\neg((p\to r)\vee(q\to r))\\(p\to r)\vee(q\to r)}$$

Proof done, mostly.   Just add line numbers and justifications for each inference.

---

On further inspection, (as @DanielSchepler notes) as $\neg r$ is never invoked in the subproof, $r$ can be derived using the principle of explosion, if that is considered a fundamental rule of inference in your ND system.

$$\fitch{(p\wedge q)\to r}{\fitch{\neg((p\to r)\vee(q\to r))}{\fitch{p}{\fitch{q}{p\wedge q\\r}\\q\to r\\(p\to r)\vee(q\to r)\\\bot\\ r}\\p\to r\\(p\to r)\vee(q\to r)\\\bot}\\\neg\neg((p\to r)\vee(q\to r))\\(p\to r)\vee(q\to r)}$$