Understanding $F\phi \to FF\phi$ as density of time I'm talking about the basic temporal language in modal logic.
Suppose we insist that the following is always true:
$$F\phi \to FF\phi$$
It is supposed to be interpreted as between any 2 time instants, there is always a third, i.e. density of time. I'm not able to understand how.
$F\phi$ means $\phi$ will be the case in the future, and $FF\phi$ means $F\phi$ will be the case in the future. How do I understand this as density?
 A: See Temporal Logic for the basic definition and the condition expressing "dense" in term of the precedence operator: $<$.
Suppose that the temporal model $\mathcal M$ is dense.
Consider a valuation $v$ such that   $\mathcal M, t \vDash \text F p[v]$. By the clause for $\text F$ operator we have that $\mathcal M, t' \vDash p[v]$ for some $t' > t$ [a valuation is a function assigning to each atomic proposition $p$ the set of time instants $v(p)$ at which $p$ is true.]
By density, there is some $t''$ such that: $t < t'' < t'$ and the fact above implies that $\mathcal M, t'' \vDash \text F p[v]$.
But this in turn implies: $\mathcal M, t \vDash \text F \text F p[v]$.
Thus, if the temporal model is dense, we have that: $\mathcal M, t \vDash \text F p \to \text F \text F p$.
Conversely, we show that the formula $\text F \text F p$ is not valid on a discrete ordering of time.
Consider two successive points $t_0$ and $t_1$ and consider the valuation $v^*$ that makes $p$ true only at $t_1$ [i.e. $v^*(p) = \{ t_1 \}$].
Obviously, $\text F p$ holds at $t_0$; but since there is no point in time between $t_0$ and $t_1$, the formula $\text F \text F p$ cannot be true at $t_0$.
Thus, in a discrete model of time, the formula $\text F p \to \text F \text F p$ is not satisfied by valuation $v^*$.
