Logical deduction to show that the following proposition is unconditionally true

Question

(P → (Q → R)) → ( P /\ Q → R)

I have to show proof that this is true.

If anyone could do it and fully explain the steps so I can understand it and continue with further questions, that'd be much appreciated.

Answer 1

Build up from the bottom.

You have a nested conditional on the right, so use two $\to$ Right rules to get there.

$$\dfrac{?}{\dfrac{P\to(Q\to R), P\wedge Q~\vdash~R}{\dfrac{P\to (Q\to R)~\vdash~ (P\wedge Q)\to R}{\vdash ~(P\to (Q\to R))\to ((P\wedge Q))\to R)}{\tiny\to\text{Right}}}{\tiny\to\text{Right}}}$$

To get that conjunction on the left, we use the $\wedge$ Left rule .

$$\dfrac{?}{\dfrac{P\to (Q\to R), P, Q ~\vdash~ R}{\dfrac{ P\to (Q\to R), P\wedge Q ~\vdash~ R}{\dfrac{P\to Q\to R~\vdash~ (P\wedge Q)\to R}{\vdash ~(P\to (Q\to R))\to ((P\wedge Q))\to R)}{\tiny\to\text{Right}}}{\tiny\to\text{Right}}}{\tiny \wedge\text{Left}}}$$

Now you have a conditional on the left so, perhaps, looking for a $\to$ left rule is an idea?

$$\dfrac{\dfrac{?}{P, Q\vdash P,R} \qquad \dfrac{?}{Q\to R, P, Q\vdash R}}{\dfrac{P\to (Q\to R), P, Q ~\vdash~ R}{\dfrac{ P\to (Q\to R), P\wedge Q ~\vdash~ R}{\dfrac{P\to Q\to R~\vdash~ (P\wedge Q)\to R}{\vdash ~(P\to (Q\to R))\to ((P\wedge Q))\to R)}{\tiny\to\text{Right}}}{\tiny\to\text{Right}}}{\tiny \wedge\text{Left}}}{\tiny\to\text{Left}}$$

For that first branch we just have literals, so can an assumption make it? Well $\{P,Q\}\cap\{P, R\}=\{P\}$ so, yes, it passes the non-empty test.

$$\dfrac{\dfrac{\color{silver}{\{P,Q\}\cap\{P, R\}=\{P\}}}{P, Q\vdash P,R}{\tiny\text{Assume}} \qquad \dfrac{?}{Q\to R, P, Q\vdash R}}{\dfrac{P\to (Q\to R), P, Q ~\vdash~ R}{\dfrac{ P\to (Q\to R), P\wedge Q ~\vdash~ R}{\dfrac{P\to Q\to R~\vdash~ (P\wedge Q)\to R}{\vdash ~(P\to (Q\to R))\to ((P\wedge Q))\to R)}{\tiny\to\text{Right}}}{\tiny\to\text{Right}}}{\tiny \wedge\text{Left}}}{\tiny\to\text{Left}}$$

On the other branch, we have a conditional on the left, so what do we do?

---

We apply the "$\to$ Left" rule, $\tfrac{\color{navy}\Gamma~ \vdash~\color{blue}\varphi,\color{crimson}\Delta\quad\color{navy}\Gamma,\color{purple}\chi~\vdash~\color{crimson}\Delta}{\color{navy}\Gamma,\color{blue}\varphi\to\color{purple}\chi~\vdash~\color{crimson}\Delta}$, making what should be glarringly obvious substitutions.

$$\dfrac{\ldots\qquad\dfrac{\dfrac{}{\color{navy}{P, Q}~\vdash~\color{blue}Q, \color{crimson}R}{\tiny\text{?}}\qquad\dfrac{}{\color{navy}{P, Q},\color{purple}R~\vdash~\color{crimson}R}{\tiny\text{?}}}{\color{blue}Q\to\color{purple}R, \color{navy}{P, Q}~\vdash~\color{crimson}R}{\tiny\to\text{Left}}}{\vdots}$$

Now we can immediately see that these branches can be made by the so called Assumption rule, since in each the antecedant and consequent contain common predicates.