Natural deduction - prove a theorem

Question

I am currently taking a course in "Introduction to Mathematical Logic" and I have been trying to do this proof, but everything I did just lead me to nowhere... Could anyone give me a general idea of how to start these kinds of proofs in the right way? And is there a specific mindset I need to have when approaching these kinds of problems?

$ \vdash((p\lor(p\rightarrow q))\rightarrow((p\rightarrow r)\land(q\rightarrow r)))\rightarrow((p\lor q)\rightarrow r) $

Answer 1

Natural deduction is just formally writing out how we reason in a normal proof. First, let me write out how I would reason about the proof in words.

Proof. We want to prove that "if (p ∨ (p → q)) → ((p → r) ∧ (q → r)), then ((p ∨ q) → r)". Let us assume that (p ∨ (p → q)) → ((p → r) ∧ (q → r)) is true, and call this assumption (1). From assumption (1), we want to prove that "if (p ∨ q) holds, then r holds".

Suppose p is true. Then (p ∨ (p → q)) is true by properties of ∨. So by assumption (1), we obtain ((p → r) ∧ (q → r)). In particular, we have (p → r) by the properties of ∧. Now since we assumed p is true, we conclude that r is true.

On the other hand, suppose q is true. Then p → q is true, because q is already assumed to be true. So (p ∨ (p → q)) holds. Thus by assumption (1), we obtain ((p → r) ∧ (q → r)). In particular, we have (q → r). Now since we assumed q is true, we conclude that r is true.

We have proven that, under assumption (1), if p holds then r holds. We have also proven that, under assumption (1), if q holds then r holds. Therefore, under assumption (1), if (p ∨ q) holds then r must also hold. $\square$

This proof is then formalised using the natural deduction rules. If you read the following proof line by line and compared it with the informal word-y proof above, you will see parallels in the line-of-thinking.

1. (p ∨ (p → q)) → ((p → r) ∧ (q → r)) $\quad$ Assumption

$\quad$ 2. p ∨ q $\quad$ Assumption

$\quad$ $\quad$ 3. p $\quad$ Assumption

$\quad$ $\quad$ $\quad$ 4. p ∨ (p → q) $\quad$ ∨ Intro (3)

$\quad$ $\quad$ $\quad$ 5. (p → r) ∧ (q → r) $\quad$ → Elim (1, 4)

$\quad$ $\quad$ $\quad$ 6. p → r $\quad$ ∧ Elim (5)

$\quad$ $\quad$ $\quad$ 7. r $\quad$ → Elim (3, 6)

$\quad$ $\quad$ 8. q $\quad$ Assumption

$\quad$ $\quad$ $\quad$ 9. p $\quad$ Assumption

$\quad$ $\quad$ $\quad$ $\quad$ 10. p → q $\quad$ → Intro (8, 9)

$\quad$ $\quad$ $\quad$ $\quad$ 11. q $\quad$ → Elim (9, 10)

$\quad$ $\quad$ $\quad$ 12. p → q $\quad$ → Intro (9, 10, 11)

$\quad$ $\quad$ $\quad$ 13. p ∨ (p → q) $\quad$ ∨ Intro (12)

$\quad$ $\quad$ $\quad$ 14. (p → r) ∧ (q → r) $\quad$ → Elim (1, 13)

$\quad$ $\quad$ $\quad$ 15. q → r $\quad$ ∧ Elim (14)

$\quad$ $\quad$ $\quad$ 16. r $\quad$ → Elim (8, 15)

$\quad$ $\quad$ 17. r $\quad$ ∨ Elim (2, 3–7, 8–16)

$\quad$ 18. (p ∨ q) → r $\quad$ → Intro (2–17)

19. ((p ∨ (p → q)) → ((p → r) ∧ (q → r))) → ((p ∨ q) → r) $\quad$ → Intro (1–18)

It is worth noting that some people suggest using a bottom-up approach when writing out these natural deduction proofs, because you can always see what you should be aiming for. For example, if you're trying to prove A → B, then you know that your very last step must be an → Intro.

Answer 2

The formula you have to prove has the form $A \to (B \to C)$, where

$$ A = (p \lor (p \to q)) \to ((p \to r) \land (q \to r)) , \qquad B = p \lor q, \qquad C = r $$

To write a derivation of the formulas of the form $A \to (B \to C)$, the idea is to suppose $A$ and $B$, and to find a way to derive $C$ from these two assumptions. There is no reasonable mechanical procedure that helps you find such a way, only intuition and experience can help you.

I suggest that to derive $C = r$, you can apply the rule $\lor_\text{elim}$ to the assumption $B = p \lor q$. Why? Because to apply the rule $\lor_\text{elim}$, which amounts to do a proof by cases, you can suppose $p$ and $q$ separately as a further assumption: in either case, by exploiting the assumption $A = (p \lor (p \to q)) \to ((p \to r) \land (q \to r))$, you can derive $r$.

Below, the derivation in natural deduction that formalizes my intuitive explanation above.

\begin{align}\small \dfrac {[p \lor q]^* \ \ \dfrac {\dfrac {\displaystyle{\atop [A]^\bullet} \ \ \dfrac{[p]^\circ}{p \lor (p \to q)}\lor_{\text{intro}_1}} {\dfrac{(p \to r) \land (q \to r)}{p \to r}\land_{\text{elim}_1}} \!\to_\text{elim} { \atop \displaystyle{ \atop \displaystyle{ \atop [p]^\circ}}\!\!\!} } {r} \!\to_\text{elim} \ \ \dfrac {\dfrac {\displaystyle{ \atop [A]^\bullet} \ \ \dfrac {\dfrac{[q]^\circ}{p \to q}\to_\text{intro}} {p \lor (p \to q)}\lor_{\text{intro}_2}} {\dfrac{(p \to r) \land (q \to r)}{q \to r}\land_{\text{elim}_2}} \!\to_{\text{elim}} \displaystyle{ \atop \displaystyle{\atop \displaystyle{\atop [q]^\circ}}}\!\! } {r} \!\to_\text{elim} } {\dfrac {r} {\dfrac{(p \lor q) \to r}{A \to ((p \lor q) \to r)}\to_\text{intro}^\bullet} \to_\text{intro}^* } \lor_\text{elim}^\circ \end{align}