If $S5 \vdash \alpha$ then $S4 \vdash \diamond \alpha$ I would like to prove that if S5 proves $\alpha$ then S4 proves $\diamond \alpha$. Here S4 is K plus axioms for reflexivity ($\square \alpha \to \alpha$) and transitivity ($\square \alpha \to \square \square \alpha$), and S5 is S4 plus the axiom $\diamond \alpha \to \square \diamond \alpha$.
My attempts:
I tried to prove it semantically, i.e. that if $\alpha$ is true in every reflexive, transitive, symmetric model then $\diamond \alpha$ is true in every reflexive, transitive model (and then use completeness), by using something like a "symmetric closure" of the relation, but I got stuck ($\alpha$ may be "complicated", I'm not sure how to handle all of the cases...).
I also tried to prove it by induction on the proof of $\alpha$ from S5. I think I was able to prove $S4 \vdash \diamond \alpha$ in case that $\alpha$ is an axiom of S5, but that is not enough, I need to take care of MP and NEC ($\vdash \alpha \Rightarrow \vdash \square \alpha$). For example for NEC I would like to prove that if $S4 \vdash \diamond \alpha$ then $S4 \vdash \diamond \square \alpha$, but I am not sure it is even true (if a model satisfies $\diamond \alpha$ it does not have to satisfy $\diamond \square \alpha$, right?).
I even tried by induction on the structure of $\alpha$ but got stuck (the induction step does not really work).
I do not think it is supposed to be a difficult question so I guess I am missing something.
Thanks in advance!
 A: Here is a proof which relies in the fact that S4 has the finite model property.
If $S4 \nvdash \Diamond \alpha$, then you have a finite Kripke model $M$ where the accessibility relation is a preorder and a world $w$ in $M$ where $\Diamond \alpha$ fails. If $\Diamond \alpha$ fails in $w$, then $\alpha$ fails in every world $w'$ accessible from $w$. In particular, $\alpha$ fails in a maximal world $w'$ in the accessibility preorder, i.e. in a world $w'$ such that $w' R v$ implies $v R w'$. The submodel $M'$ generated by $w'$, i.e. the submodel consisting of the worlds which are equivalent to $w'$ in the equivalence relation induced by the accessibility preorder, is then an S5 model which falsifies $\alpha$.
A: We can use the truth of the lozenge-ified version of the axiom $(\lozenge \beta \to \square \lozenge \beta)$ to grab ourselves a new model on the same Kripke frame where all of the $\mathsf{S5}$ axioms hold. This model does not necessarily have a symmetric accessibility relation, even if we prune away now-unreachable worlds; I'm only promising that its set of tautologies is a superset of the set of $\mathsf{S5}$-tautologies.
Lemma 101: $\lozenge (\lozenge \beta \to \square \lozenge \beta)$ is an $\mathsf{S4}$-tautology.
We can prove this using a tableau with a single branch.
My worlds are $0, 1, 2$. It holds that $0R1$, $0R2$, $2R3$. $0R3$ holds implicitly by transitivity of the accessibility relation.

*

*$0 : \square(\lozenge \beta \land \lozenge \square \lnot \beta)$ is our negated goal.

*$0 : \lozenge \beta \land \lozenge \square \lnot \beta$ follows by necessitation.

*$0: \lozenge \beta$

*$0 : \lozenge \square \lnot \beta$

*$1 : \beta$ holds at a fresh world $1$.

*$2 : \square \lnot \beta$ holds at a fresh world $2$.

*$2 : \lozenge \beta \land \lozenge \square \lnot \beta$ follows by necessitation.

*$2 : \lozenge \beta$

*$2 : \lozenge \square \lnot \beta$

*$3 : \beta$ holds at a fresh world $3$.

*$3: \lnot \beta$ follows by necessitation.

*Contradiction

We can also prove it using the topological semantics for $\mathsf{S4}$. Let $c$ be the complement, $i$ be the interior, $e$ be the exterior, and $k$ be the closure.
Note $\lozenge (\lozenge \beta \to \square \lozenge \beta)$ is equivalent to $((B^k)^c \cup (B^k)^i)^c$, with the modal symbols being replaced with their topological equivalents.

*

*$((B^k)^c \cup (B^k)^i)^k$

*$(B^e \cup B^i)^k$

*$B$
Since this holds in an arbitrary topological space, we are done.
Proof
Let $\alpha$ be an arbitrary well-formed formula such that $\mathsf{S5} \vdash \alpha$.
Consider an arbitrary $\mathsf{S4}$-model $(W, R, w)$. By Lemma 101 and the truth conditions of $\lozenge$, there exists a model $(W, R, u)$ such that $\lozenge \beta \to \square \lozenge \beta$ holds at that model and $wRu$
$(W, R, u)$ thus has all of the tautologies of $\mathsf{S5}$.
Therefore $(W, R, u) \models \alpha$.
Therefore $(W, R, w) \models \lozenge \alpha$ as desired.
Since our model was chosen arbitrarily, it holds that $\mathsf{S4} \vdash \lozenge \alpha$.
A: Following @GregNisbet's answer and @AlexKruckman's comment (and a great help from a friend), here is an answer (sketch; not using fmp):
Lemma 1: $S4\models\lozenge M4$ for every $\varphi$. (M4 is the axiom scheme $\lozenge\varphi\to\square\lozenge\varphi$).
Lemma 2: Let M be a model with a reflexive and transitive relation $R$ (preorder). If $M,u\models\lozenge\varphi\to\square\lozenge\varphi$ for some given $\varphi$, then $M,v\models\lozenge\varphi\to\square\lozenge\varphi$ for every $v$ such that $R(u,v)$.
Both lemmas can be proved (semantically) quite easily.
Now let $\{\alpha_i\}_{i=1}^n$ be the instances of M4 that are used in the proof of $\alpha$ from S5. So we observe $S4,\{\alpha_i\}_{i=1}^n\models\alpha$.
Let M be a preordered model and $w_0$ in M. For $i\in\{1...n\}$, let $w_i$ be a world that satisfies $\alpha_i$ such that $R(w_{i-1}, w_i)$ (exists because of Lemma 1). From Lemma 2, the model $M^{w_n}$ (which is M reduced to the worlds that are  seen from $w_n$) satisfies $\{\alpha_i\}_{i=1}^n$ so from the observation above it satisfies $\alpha$, which leads to $M,w_0\models\lozenge\alpha$. $w_0$ was arbitrary and M was an arbitrary preordered model so from the completeness of S4 w.r.t such models we get the result.
Any corrections or improvements? :)
