Temporal and polymodal logics

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

Related posts

• Modal axiom cube
• Simplifying Boolean expressions
• Intuitionistic logic in The Gondoliers

The post Temporal and polymodal logics first appeared on John D. Cook.