How to prove $(\Box (p\supset q)\land\Box( q\supset r))\supset\Box(p\supset r)$ in K

Question

$(\Box (p\supset q)\land\Box( q\supset r))\supset\Box(p\supset r)$

This is problem 2.1a in Hughes/Cresswell pg. 48.

So far I have this:

1. $(p \supset q)\supset((q\supset r)\supset(p\supset r)$, PC6
2. $[(p\supset q)\supset((q\supset r)\supset(p \supset r)]\supset[((p\supset q)\land(q\supset r))\supset(p\supset r)]$, PC7 [$(p\supset q)/p,(q\supset r)/q,(p\supset r)/r]$
3. $((p\supset q)\land(q\supset r))\supset(p\supset r)$, MP 1,2
4. $\Box[((p\supset q)\land(q\supset r))\supset(p\supset r)]$, N 3
5. $\Box((p\supset q)\land(q\supset r))\supset\Box(p\supset r)$, K 4

And here is where I'm stuck. I know that $\Box$ distributes over $\land$ in K. So I feel like a substitution instance of K3 needs to show up. Something like this:

$\Box((p\supset q)\land(q\supset r))\equiv(\Box(p\supset q)\land\Box(q\supset r))$

But I am not super comfortable with substitution of equivalents. If this were line 6, can I then infer a line 7 identical with 5, except 6 swaps for $\Box((p\supset q)\land(q\supset r))$?

Thanks for any and all help!

Answer 1

To summarize, you know how to prove

$$\Box((p\supset q)\land(q\supset r))\supset\Box(p\supset r)$$ and $$\Box((p\supset q)\land(q\supset r))\equiv(\Box(p\supset q)\land\Box(q\supset r))$$ and you want to eventually conclude $$(\Box (p\supset q)\land\Box( q\supset r))\supset\Box(p\supset r)$$

---

Let's introduce some abbreviations, to combine some of the trees into forests: $$A := \Box((p\supset q)\land(q\supset r)) \qquad B := \Box(p\supset r) \qquad C:= \Box(p\supset q)\land\Box(q\supset r) $$ Then what you want is $$ \text{from } A \supset B \text{ and } A \equiv C \text{ conclude } C \supset B $$ All of the modal boxes have disappeared into the abbreviations, so what is left is a purely propositional task. In fact, $$ \tag{*} (A\equiv C) \supset((A\supset B)\supset (C\supset B)) $$ is a propositional tautology, so if you trust that your proof system can derive all of those, all you need now is two steps of MP.

Alternatively, it sounds like you might already have a "substitution of equivalents" meta-theorem that tells you that $(\text{*})$ can be derived.

If neither of those plans are available to you, I'd suggest doing it from scratch in two steps. First prove $C\supset A$ from $A\equiv C$. This ought to be very simple; the fine details depend on which axioms for $\equiv$ you have to start from. Second, it looks like $(C\supset A)\supset((A\supset B)\supset(C\supset B))$ is actually an instance of a logical axiom for you ("PC6"). You then have exactly the ingredients to get to $C\supset B$ in two MP steps.