I’ve been doing some proofs in S4 recently and noticed that the following holds:
If $\phi$ is a wff and all positive literals $A$ that occur in $\phi$ are prefixed by either $\Diamond$ or $\Box$, then $\vDash_{S4} \Box \Diamond \phi \to \Diamond \Box \phi$.
I’m trying to prove this by induction on the complexity of formulas, but I am having trouble with the inductive step. Here is what I have for the base case, and any help for how to proceed would be appreciated:
If $\phi$ is an atomic formula with $\Box$ as the main operator, then because $\vDash_{S4} \Box \varphi \leftrightarrow \Box \Box \varphi$, it follows that $\vDash_{S4} \Box \Diamond \phi \to \Diamond \Box \phi$.
If $\phi$ is an atomic formula with $\Diamond$ as the main operator, since $\vDash_{S4} \Box \Diamond \Diamond \varphi \to \Diamond \Box \Diamond \varphi$, it follows that $\vDash_{S4} \Box \Diamond \phi \to \Diamond \Box \phi$.