Equivalence between temporal logic and notions of forcing

Question

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").

Answer 1

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.