(Under propositional modal logic, system K)
There's seems to be an obvious counterexample: A model with one world w s.t. $\phi$ is not true in $\phi$ and $\lnot R(w,w)$.
But consider this argument:
Assuming $\vDash\square\phi$, take an arbitrary model $M$ and construct a new model $M^*$ s.t. for any $w$ in $M$, add a world x s.t. $R(z,x)$. Since $M^*,x \vDash \square\phi$, $M^*,w \vDash\phi$. And since $\langle M,w\rangle$ and $\langle M^*,w\rangle$ is bisimilar, $M,w \vDash\phi$. Because $M$ and $w$ was arbitrary, $\vDash\phi$.
I don't think this argument is right because we don't know if $\langle M,w\rangle$ and $\langle M^*,w\rangle$ is bisimilar, since we don't know if adding an $x$ would change how $M^*, w$ satisfies sentential variables.
Intuitively, this claim holds when $\phi$ is a modal tautology. But I'm not sure if that's always the case given that $\vDash\square\phi$. I suspect it isn't.
Update:
The counterexample does not work because: since $\phi$ is any wff, we cannot assume that $\phi$ is not true at some world, for $\phi$ could be a tautology (i.e. $P\lor\lnot P$).
The argument that "If ⊨□φ then ⊨φ" is true does work:
Originally, I thought that it begs the question as saying there is a bisimulation between the old $w$ and the new $w$ means that any atomic letter in either $w$ receives the same truth assignment, which implies the conclusion. My professor got me to see that this is not the case.
Consider this:
Before we assume $\vDash\square\phi$, we first extend any model $M=\langle W, R, V\rangle$ (where $w\in W$) to $M^*=\langle W^*, R^*, V^*\rangle$ like so:
- $W^* = W\cup \{x\}$
- $R^* = R\cup\{\langle x, w\rangle\}$
- $V^*(u,p) = V(u,p)$ if $u\neq x$, F otherwise (so, satisfaction of any formulas in $w$ stays the same)
It is trivial that there is a bisimulation between $\langle M,w\rangle$ and $\langle M^*, w\rangle$.
Now we assume $\vDash\square\phi$. So $M^*,x\vDash\square\phi$, hence $M^*, w\vDash\phi$. Since $M$ and $w$ was arbitrary, we have that $\vDash\phi$.
It isn't necessary to do the model extension and bisimulation first, we can assume $\vDash\square\phi$ first. But this way makes it clearer that the argument doesn't beg the question.
Best Answer
We notice that
$$\Box\psi\rightarrow\psi$$
is not a theorem of $\mathbf{K}$, hence
$$\not\vdash_{\mathbf{K}}\Box\psi\rightarrow\psi$$
However,
$$\vdash\Box\psi\implies\vdash\psi$$
equivalently,
$$\Vdash\Box\psi\implies\Vdash\psi$$
is a metatheorem of $\mathbf{K}$. We may intuitively see this noticing that $\Box\psi$ says that $\psi$ holds in all worlds, therefore, the question of reflexivity has already been resolved. Indeed, the proof system presented in James Garson's Modal Logic for Philosophers includes it as an inference rule.
Johan van Benthem gives an interesting proof of it in his Modal Logic for Open Minds. I quote it here for completeness: