1
$\begingroup$

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?

$\endgroup$
2
$\begingroup$

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

$\endgroup$
1

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.