My posts on modal logic have mostly been about monomodal logic, logic with one modal operator. This may not seem accurate because I’ve talked about □ (“box”) and ◇ (“diamond”). But these are really just one mode: you can define either in terms of the other.
◇p = ¬ □ ¬p
□p = ¬ ◇ ¬p
Temporal logic
Temporal logic is an example of a polymodal operator. There are many varieties of temporal logic, but one version defined by Arthur Prior in the 1950s has two basic modes: P (past) and F (future). Prior called his system tense logic but the term temporal logic is more common now.
We can interpret Fp to mean that at some point in the future, p will be the case.
We can interpret Pp to mean at some point in the past p was the case.
In temporal logic we have two analogs of the box operator, and each has its dual counterpart analogous to diamond.
Gp = ¬ F ¬p
Hp = ¬ P ¬p
So Gp can be read as “from now on p will be the case.”
And Hp can be read as “always up until now p has been the case.”
The combination GFp can be interpreted as “eventually p.”
The combination PHp can be interpreted as “up until some point in the past, p.”
I’ve mentioned before how Kripke semantics—models of “accessible worlds”—sounds like science fiction. Temporal logic can have that flavor too when you get into whether you view time as one linear stream or a branching tree, whether time is discrete or continuous, etc.
I mentioned briefly at the bottom of my post on duality that the algorithm given there for monomodal logics extends to polynomial logics.
In that post I said that the shell command
tr '□◇→' '◇□←'
can turn a modal proposition into its dual. We could find the dual of a temporal proposition with the shell command
tr 'FGPH→' 'GFHP←'
In other words, we replace Fs with Gs, Gs with Fs, Ps with Hs, Hs with Ps, and reversing the direction of implication.
More modes
Polymodal logics can have a lot more than two modes. For example, in security applications of modal logic, you might have a modal operator for every user of a system. Here we might model what a user knows rather than what is true: something might be true without a particular agent knowing that it’s true.
Simulation
Obviously monomodal logics are contained inside polymodal logics; if you have several modalities, box could be one of them. But here’s the amazing converse: polymodal logics can be simulated by monomodal logics.
In the abstract to their paper “Normal monomodal logics can simulate all others.” Marcus Kracht6 and Frank Wolter announce
This paper shows … that polymodal normal logics can be simulated by monomodal (normal) logics. Many properties of logics are shown to be reflected and preserved by such simulations … sheding new light on the power of normal monomodal logic.