Understanding $F\phi \to FF\phi$ as density of time

42 Views Asked by At

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?

1

There are 1 best solutions below

1
On BEST ANSWER

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