Axiomatic Proofs in K

Question

I have an exercise from Sider's logic book wherein I need to give an axiomatic proof that the following holds in K:
$(\Box(P\rightarrow Q) \land \Box (P \rightarrow\neg Q))\rightarrow \neg\Diamond P.$

I have three basic steps done already, and my tools are, MP (duh), the K axiom, $\Diamond K$ axiom, the modal negation theorems and all of the the rules and theorems of PL.

1. $((P\rightarrow Q) \land (P\rightarrow \neg Q))\rightarrow\neg P$ (PL)
2. $\Box (((P \rightarrow Q)\land (P\rightarrow \neg Q))\rightarrow \neg P)$ (NEC)
3. $\Box ((P\rightarrow Q) \land (P \rightarrow \neg Q)) \rightarrow \Box \neg P.$ (K + MP)

This is where I'm stuck. Does anyone have tips on how to proceed? Or any suggestions about strategies, how to start different, etc.? Any $\textit{help, hints, suggestions, tips}$ would be great. Please, if you can, do not post solutions; I'm trying to learn!

PS: I'm not thinking that I can go from ....
4. $(P\rightarrow (Q\land \neg Q)) \rightarrow \neg P$ (PL)
5. $\Box (((P\rightarrow (Q \land \neg Q))\rightarrow \neg P)$ (NEC)
6. $\Box (P \rightarrow(Q \land \neg Q)) \rightarrow \Box \neg P$ (K)

And (6) is equivalent to what I'm trying to show, yeah? Is it plausible to just state the conclusion and say "equivalence" or something?

I'm having a hard time with this (and every other) axiomatic proof

Answer 1

You have $(A\wedge B)\to \neg P$ as a theorem, where $A$ is $P\to Q$, and $B$ is $P\to \neg Q$.

Then use exportation $(A\wedge B)\to C \iff A\to (B\to C)$

$\begin{array}{llll} 1. & (A\wedge B)\to \neg P&\text{a theorem} &{\sf PL}\\ 2. & A\to(B\to \neg P)&\text{by exportation}&\sf PL\\ 3. & \Box(A\to(B\to\neg P)) & \text{by necessitation}&\sf N\\ 4. & (\Box A\to \Box(B\to \neg P)) &\text{by distribution}&\sf K\\ \vdots & \vdots & \vdots & \vdots \\ \vdots & \Box A\to(\Box B\to \neg\Diamond P) & \vdots & \vdots \\ \vdots & (\Box A\wedge \Box B)\to\neg\Diamond P & \text{by exportation} & \sf PL \end{array}$