# 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?

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^*$$.