temporal logic



Temporal logics, as their name suggests, are logics that involve time. They form a very large and important class of modal logics, but here we will, to start with, only look at some simple cases. Temporal logics are very closely related to tense logic?s.

Basic temporal language, (BTL)

First the basic temporal language is built with two binary model operators, which instead of being denoted ‘box’ and ‘diamond’, are written FF and PP. The intended interpretation of these are:

  • FϕF\phi is ϕ\phi will be true at some future time;

  • PϕP\phi is ϕ\phi was true at some past time.

The reason for the notation FF and PP should be clear.

  • The dual of FF is GG, so Gϕ=¬F¬ϕG\phi = \neg F\neg \phi. This means that we read GϕG\phi as ‘at no future time is ϕ\phi not true’, i.e., ϕ\phi is always going to be true. (GG for ‘going’.)

  • The dual of PP is written HH, whence Hϕ=¬P¬ϕH\phi = \neg P\neg \phi and HϕH\phi interprets as ‘ϕ\phi has always been true’. (HH is for ‘has’ - which is a bit weak, but that is life!)

  • If for all ϕ\phi we have PϕGPϕP\phi \to G P\phi, then whatever has happened will always have happened, which seems reasonable so this might be a suitable ‘general truth’ we might want a temporal logic to contain.

  • If we had in our logic that FϕFFϕF\phi \to F F\phi, then this would means that if ϕ\phi is true at some future time, then at some future time it will be true that ϕ\phi will be true at some future time, so between any two instants there must be a third, and the general truth of this would say something about the ‘internal structure’ of time as modelled by such a logic.

This basic temporal language does not yet really constitute a sensible logic that could model important features of ‘time’. but we can still look at models so as to see what properties of the models can be identified as corresponding to seemingly feasible formulae in the language.

Frames and Models for BTL

A frame for BTL will be a set, TT, with two binary relations R FR_F and R PR_P. We have R FxyR_F x y reads that ‘at xx, yy is in the future’ - but, in the ordinary common sense meaning of words, this should mean R PyxR_P y x and conversely. In other words R PR_P should be the converse or opposite relation of R FR_F.

(In general, if RR is a binary relation on a set XX, then its opposite relation is defined by

(y,x)R op(x,y)R.)(y,x) \in R^{op} \Leftrightarrow (x,y)\in R.)

A frame of the form (T,R,R op)(T,R,R^{op}) is called a bidirectional frame.

If we have any model 𝔐=(T,R,V)\mathfrak{M} = (T,R,V) with a valuation, VV, then we can interpret BTL in terms of it by specifying the interpretation of PP in terms that of RR. explicitly we define

  • 𝔐,tFϕ\mathfrak{M}, t\models F\phi if and only if s(Rts𝔐,sϕ);\exists s (R t s \wedge \mathfrak{M}, s\models \phi);

  • 𝔐,tPϕ\mathfrak{M}, t\models P\phi if and only if s(Rst𝔐,sϕ)\exists s (R s t \wedge \mathfrak{M}, s\models \phi),

but, of course, this is still a long way from having a logic that looks as if it captures ‘time-like’ behaviour. We could have models with ‘circular time’, and ‘branching time’. Both of these correspond to various situations in computational applications so should be kept in mind, both to be able to identify their occurrence and to build them in or to avoid them in the logics.


One condition it would be natural to impose is transitivity of R FR_F, since if FϕF\phi is true at some future time, then clearly, ϕ\phi itself must also be true at some future time, i.e., later on still! This leads one to ask that

(4)FFϕFϕ(4) \quad\quad F F\phi \to F\phi

should be in our logic, (and similarly for PP, but that will hold in the bidirectional models since if RR is transitive then so will be R opR^{op}).

Temporal Logic in Terms of Adjoints

Consider a category 𝒞\mathcal{C}, and an internal category given by b,e:Time 1Time 0b, e: Time_1 \rightrightarrows Time_0. Here we understand elements of Time 1Time_1 as time intervals, and bb and ee as marking their beginning and end points. We may choose to impose additional structure on TimeTime, e.g., that it be an internal poset, or a linear order.

Now each arrow, bb and ee, generates an adjoint triple, e.g., bb * b\sum_b \dashv b^{\ast} \dashv \prod_b, formed of dependent sum, base change, dependent product, going between the slices 𝒞/Time 0\mathcal{C}/Time_0 and 𝒞/Time 1\mathcal{C}/Time_1.

Then we find two adjunctions be * eb *\sum_b e^{\ast} \dashv \prod_e b^{\ast} and eb * be *\sum_e b^{\ast} \dashv \prod_b e^{\ast}, e.g.,

Hom( be *C(t),D(t))=Hom(e *C(t),b *D(t))=Hom(C(t), eb *D(t)). Hom(\sum_b e^{\ast} C(t), D(t)) = Hom(e^{\ast} C(t), b^{\ast} D(t)) = Hom(C(t), \prod_e b^{\ast} D(t)).

Now consider for the moment that CC and DD are propositions. Then be *C\sum_b e^*C means “there is some interval beginning now and such that CC is true at its end”, i.e. FCF C; while eb *D\prod_e b^*D means “for all intervals ending now, DD is true at their beginning”, i.e. HDH D. Hence our adjunction is FHF \dashv H. Similarly, interchanging bb and ee, we find PGP \dashv G. Note that we don’t have to assume the classical principle Gϕ=¬F¬ϕG\phi = \neg F\neg \phi and Hϕ=¬P¬ϕH\phi = \neg P\neg \phi.

In the setting of dependent type theory, we do not need to restrict to propositions, but can treat the temporal operators on general time-dependent types. So if People(t)People(t) is the type of people alive at tt, FPeople(t)F People(t) is the type of people alive at a point in the future of tt, and GPeople(t)G People(t) is a function from future times to people alive at that time, e.g., an element of this is ‘The oldest person alive(t)’.

Since TimeTime is a category, we have in addition to the two projections p,q:Time 1× Time 0Time 1Time 1p,q:Time_1\times_{Time_0} Time_1 \to Time_1, composition c:Time 1× Time 0Time 1Time 1c:Time_1\times_{Time_0} Time_1 \to Time_1. This allows us to express more subtle temporal expressions, such as ‘ϕ\phi has been true since a time when ψ\psi was true’, denoted ϕSψ\phi S \psi.

ϕSψ:=Σ e(b *ψ×Π c(ep) *ϕ)\phi S \psi := \Sigma_e (b^* \psi \times \Pi_c (e p)^* \phi)

(note ep=bqe p = b q). That is, there is a subinterval ending now such that ψ\psi was true at its beginning and ϕ\phi was true at all points inside it. Similarly, ‘ϕ\phi will be true until a time when ψ\psi is true’ is

ϕUψ:=Σ b(e *ψ×Π c(ep) *ϕ).\phi U \psi := \Sigma_b (e^* \psi \times \Pi_c (e p)^* \phi).

Temporal logicians have debated the relevant advantages of instant-based and interval-based approaches. Some have also considered hybrid approaches (Balb11). The analysis of this section suggests that working with intervals and instants together in the form of an internal category allows for a natural treatment via adjoint logic.


Generally this entry is based on

  • P. Blackburn, M. de Rijke and Y. Vedema, Modal Logic, Cambridge Tracts in Theoretical Computer Science, vol. 53, 2001,

but see also:

  • A. Galton, Temporal Logic, (Stanford Encyclopedia of Philosophy)

  • Patrick Blackburn, Tense, Temporal Reference and Tense Logic, Journal of Semantics, 1994,11, pages 83–101, on-line version

  • Balbiani, P., Goranko, V. and Sciavicco, G., 2011, ‘Two-sorted Point-Interval Temporal logics’, in Proc. of the 7th International Workshop on Methods for Modalities (M4M7) (Electronic Notes in Theoretical Computer Science: Volume 278), pp. 31–45.

Revised on October 3, 2015 05:56:35 by David Corfield (