I have come across literature comparing modal logic to forcing (by Hamkins et al). Has anything similar been done showing equivalences between temporal logic and forcing? This would be interesting to me, since forcing is sometimes explained in a way that seems to imply the passage of time (i.e. a "before" using a generic filter and "after").
Temporal logic is just a particular flavor of modal logic, so the same S4 models (trees, really; finite trees in the propositional case) that give natural "forcing semantics" for intuitionistic logic can be understood as branching temporal S4 flows with the additional heredity condition, which says that: what is forced at any instant t is forced at all instants t' > t.
Another natural way of thinking of those models is in epistemic logical terms, which again, is just another flavor of modal logic. So just take the epistemic logic corresponding to S4, add the heredity condition, and you've got epistemic forcing models for intuitionistic logic.
Of course none of this is precise, so check out CSLI Lecture Notes #199, Ch. 20 for the basic details.
I just noticed this question. There are certain affinities between the modal logic of forcing and temporal logic, particularly when one has the upward modality expressing that something is true in some forcing extension (like the future), but also the dual modality for when something is true in some ground model (like the past). In joint work, Benedikt Loewe and I have studied this mixed modal logic of forcing in our paper
- J. D. Hamkins, B. Loewe, Moving up and down in the generic multiverse Logic and its applications, ICLA 2013 LNCS, vol. 7750, pp. 139-147, 2013.
It is easy to see (see footnote $7$ in our paper) for the mixed modal logic of forcing that any statement $p$ implies that $p$ is upwards necessarily downwards possible. This is also a basic fact in most temporal logics, asserting that $p$ implies that from now on in the future, $p$ was true at some point in the past. Similarly, it is easy to prove for forcing that $p$ implies that in all ground models, $p$ is forceable. And in temporal logic, if $p$ is true, then at every point in the past, it is possible that $p$ holds in the future.