# Are there any invalid $S5$-formulas $\psi$ such that $\diamond\psi$ is valid?

I cannot find an example for an invalid $S5$ formula $\psi$ (i.e. $\nvDash\psi$), such that $\diamond\psi$ is valid (i.e. $\vDash\diamond\psi$).
If there is none, then $\vDash\diamond\psi\Rightarrow\,\vDash\psi$ is the case, but I cannot find a proof for that.
So far, I only managed to prove it for propositional $\psi$ (i.e. $\psi$ that contain no $\diamond$ or $\square$), based on the idea that when $\psi$ is propositional and $S5$-valid, then for a set of worlds that contains only one element, $\psi$ is true, and since it is independent of other worlds (because it is propositional), it is also true for every set of worlds.

Do you know an example or can you prove that no such example exists in the general case?

Consider $\psi = (P \lor \square \lnot P)$.
$\psi$ is not valid in $S5$, since it's possible to have a world satisfying both $\lnot P$ and $\lozenge P$.
But $\lozenge \psi$ is valid in $S5$. Indeed, consider any world $w$ in a Kripke model of $S5$ (actually, all we need is that the accessibility relation $R$ is reflexive). Case 1: $P$ holds at some world $v$ accessible from $w$. Then $\lozenge \psi$ holds at $w$, since $\psi$ holds at $v$. Case 2: $\lnot P$ holds at every world accessible from $w$, i.e. $\square \lnot P$ holds at $w$. Then $\lozenge \psi$ holds at $w$, since $\psi$ holds at $w$ and $R$ is reflexive.