Prove $(\Diamond p \to \Box q) \to (\Diamond p \to \Diamond q)$ in K

Question

Modal logic, axiomatic proofs in K

I started with the tautology $(p \to q) \to (p \to q)$ but i'm a bit stuck.

$1. (p \to q) \to (p \to q)$

$2.\Box(p \to q) \to \Box(p \to q)$

$3. (\Box p \to \Box q) \to (\Box p \to \Box q)$

$4. (\neg \Diamond\neg p \to \Box q) \to (\neg \Diamond\neg p \to \neg \Diamond\neg q)$

But im not sure what to do from here. Did i pick a bad starting tautology.

Answer 1

The key here is to assume $\Diamond P$ to prove $\Diamond Q$ after already assuming $\Diamond P \to \Box Q$. Since we know that $\bot \to Q$, by Necessitation and K we get $\Box \bot \to \Box \sim Q$. By similar reasoning we get $\Box \bot \to \Box \sim P$. Since $\sim \Box \sim$ is equivalent to $\Diamond$, we have $\Diamond P \to \Diamond \top$. By Necessitation and K we have $\Box Q \to (\Box \sim Q \to \Box \bot)$. Since we have assumed both $\Diamond P$ and $\Diamond P \to \Box Q$, by Modus Ponens we have $\Box Q$, which in turn gives us $\Box \sim Q \to \Box \bot$. By contrapositive identity, we have $\Diamond \top \to \Diamond Q$. Since we have $\Diamond P \to \Diamond \top$, by Hypothetical Syllogism and Modus Ponens we have $\Diamond Q$. Thus, discharging our assumptions, we conclude $(\Diamond P \to \Box Q) \to(\Diamond P \to \Diamond Q)$.

Answer 2

I give a proof employing basic definitions/equivalences; one can supply the terms in the annotations and add or delete several lines according to one's system and context:

1. $\Diamond P\rightarrow\Box Q\tag{Assumption}$
2. $\neg\Box\neg P\rightarrow\Box Q\tag{Definition}$
3. $\Box\neg P\vee\Box Q\tag{Definition}$
4. $\Box(\neg P\vee Q)\tag{Distribution}$
5. $\Box(P\rightarrow Q)\tag{Definition}$
6. $\Box(P\rightarrow Q)\rightarrow(\Box P\rightarrow\Box Q)\tag{Axiom}$
7. $\Box P\rightarrow\Box Q\tag{Modus Ponens 5, 6}$
8. $(P\rightarrow Q)\rightarrow(\neg Q\rightarrow\neg P)\tag{Contraposition}$
9. $\Box((P\rightarrow Q)\rightarrow(\neg Q\rightarrow\neg P))\tag{Necessitation 8}$
10. $\Box(P\rightarrow Q)\rightarrow\Box(\neg Q\rightarrow\neg P)\tag{Axiom, Modus ponens 9}$
11. $\Box(\neg Q\rightarrow\neg P)\tag{Modus ponens 7, 10}$
12. $\Box(\neg Q\rightarrow\neg P)\rightarrow(\Box\neg Q\rightarrow\Box\neg P)\tag{Axiom}$
13. $\Box\neg Q\rightarrow\Box\neg P\tag{Modus ponens 11, 12}$
14. $\neg\Diamond\neg\neg Q\rightarrow\neg\Diamond\neg\neg P\tag{Definition}$
15. $\neg\Diamond Q\rightarrow\neg\Diamond P\tag{Double negation elimination 14}$
16. $\Diamond P\rightarrow\Diamond Q\tag{Contraposition 15}$
17. $(\Diamond P\rightarrow\Box Q)\rightarrow(\Diamond P\rightarrow\Diamond Q)\tag{Implication introduction 1, 17}$