Validity of $ F \supset \Box F$

Question

I started to study propositional modal logic and Kripke semantics. I learned that for any Kripke interpration $\mathcal{M}$, we have that, if $\mathcal{M} \models A$ then $\mathcal{M} \models \Box A$. From which also follows that for all frames $\mathcal{F}$, if $\mathcal{F} \models A$, then $\mathcal{F} \models \Box A$, which again makes sense.

But then I read that $F \supset \Box F$ is not valid in general. I didn't understand this part. I mean, if the validy of $F$ implies the validity of $\Box F$, then the formula $F \supset \Box F$ should be valid.

If someone can give me a concrete counter-example to $F \supset \Box F$, I would be glad. I also want to hear whether there is any frame in which $F \supset \Box F$ is valid.

Answer 1

The property :

if $\vDash \varphi$, then $\vDash \square \varphi$

is the ground for the Rule of Necessitation.

It says that $\square \varphi$ is a theorem of a normal modal logic whenever $\varphi$ is a theorem of the logic.

This does not contradict the fact that $\varphi \to \square \varphi$ is not valid.

---

A "tricky" but simple counterexample can be manufactured considering a propositional letter $p$.

Clearly, $\nvDash p$ and thus (vacuously) : if $\vDash p$, then $\vDash \square p$ holds.

But :

$\nvDash p \to \square p$.

Answer 2

For a countermodel consider any 2-element K-model, where the first element accesses the second and where p is true in the first, but not in the second.

$F \rightarrow \Box F$ is valid in every S4-model satisfying the hereditary condition: If $p$ is true in $w$, then $p$ is true in $v$ for all $v$ with $wRv$.