Stanford Encyclopedia of Philosophy
This is a file in the archives of the Stanford Encyclopedia of Philosophy.

Temporal Logic

First published Mon Nov 29, 1999; substantive revision Thu Feb 7, 2008

The term Temporal Logic has been broadly used to cover all approaches to the representation of temporal information within a logical framework, and also more narrowly to refer specifically to the modal-logic type of approach introduced around 1960 by Arthur Prior under the name of Tense Logic and subsequently developed further by logicians and computer scientists.

Applications of Temporal Logic include its use as a formalism for clarifying philosophical issues about time, as a framework within which to define the semantics of temporal expressions in natural language, as a language for encoding temporal knowledge in artificial intelligence, and as a tool for handling the temporal aspects of the execution of computer programs.

1. Modal-logic approaches to temporal logic

1.1 Tense Logic

Tense Logic was introduced by Arthur Prior (1957, 1967, 1969) as a result of an interest in the relationship between tense and modality attributed to the Megarian philosopher Diodorus Cronus (ca. 340-280 BCE). For the historical context leading up to the introduction of Tense Logic, as well as its subsequent developments, see Øhrstrøm and Hasle, 1995.

The logical language of Tense Logic contains, in addition to the usual truth-functional operators, four modal operators with intended meanings as follows:

P “It has at some time been the case that …”
F “It will at some time be the case that …”
H “It has always been the case that …”
G “It will always be the case that …”

P and F are known as the weak tense operators, while H and G are known as the strong tense operators. The two pairs are generally regarded as interdefinable by way of the equivalences

Pp ¬H¬p
Fp ¬G¬p

On the basis of these intended meanings, Prior used the operators to build formulae expressing various philosophical theses about time, which might be taken as axioms of a formal system if so desired. Some examples of such formulae, with Prior's own glosses (from Prior 1967), are:

GpFp “What will always be, will be”
G(pq)→(GpGq) “If p will always imply q, then if p will always be the case, so will q
FpFFp “If it will be the case that p, it will be — in between — that it will be”
¬FpF¬Fp “If it will never be that p then it will be that it will never be that p

Prior (1967) reports on the extensive early work on various systems of Tense Logic obtained by postulating different combination of axioms, and in particular he considered in some detail what light a logical treatment of time can throw on classic problems concerning time, necessity and existence; for example, “deterministic” arguments that have been advanced over the ages to the effect that “what will be, will necessarily be”, corresponding to the modal tense-logical formula Fp→□Fp.

Of particular significance is the system of Minimal Tense Logic Kt, which is generated by the four axioms

pHFp “What is, has always been going to be”
pGPp “What is, will always have been”
H(pq)→(HpHq) “Whatever has always followed from what always has been, always has been”
G(pq)→(GpGq) “Whatever will always follow from what always will be, always will be”

together with the two rules of temporal inference:

RH: From a proof of p, derive a proof of Hp
RG: From a proof of p, derive a proof of Gp

and, of course, all the rules of ordinary Propositional Logic. The theorems of Kt express, essentially, those properties of the tense operators which do not depend on any specific assumptions about the temporal order. This characterisation is made more precise below.

Tense Logic is obtained by adding the tense operators to an existing logic; above this was tacitly assumed to be the classical Propositional Calculus. Other tense-logical systems are obtained by taking different logical bases. Of obvious interest is tensed predicate logic, where the tense operators are added to classical First-order Predicate Calculus. This enables us to express important distinctions concerning the logic of time and existence. For example, the statement A philosopher will be a king can be interpreted in several different ways, such as

x(Philosopher(x) & F King(x)) Someone who is now a philosopher will be a king at some future time
xF(Philosopher(x) & King(x)) There now exists someone who will at some future time be both a philosopher and a king
Fx(Philosopher(x) & F King(x)) There will exist someone who is a philosopher and later will be a king
Fx(Philosopher(x) & King(x)) There will exist someone who is at the same time both a philosopher and a king

The interpretation of such formulae is not unproblematic, however. The problem concerns the domain of quantification. For the second two formulae above to bear the interpretations given to them, it is necessary that the domain of quantification is always relative to a time: thus in the semantics it will be necessary to introduce a domain of quantification D(t) for each time t. But this can lead to problems if we want to establish relations between objects existing at different times, as for example in the statement “One of my friends is descended from a follower of William the Conqueror”.

These problems are related to the so-called Barcan formulae of modal logic, a temporal analogue of which is

Fxp(x)→∃xFp(x) (“If there will be something that is p, then there is now something that will be p”)

This formula can only be guaranteed to be true if there is a constant domain that holds for all points in time; under this assumption, bare existence (as expressed by the existential quantifier) will need to be supplemented by a temporally restricted existence predicate (which might be read 'is extant') in order to refer to different objects existing at different times. For more on this and related matters, see van Benthem, 1995, Section 7.

1.2 Extensions to Tense Logic

Soon after its introduction, the basic “PFGH” syntax of Tense Logic was extended in various ways, and such extensions have continued to this day. Some important examples are the following:

The binary temporal operators S and U (“since” and “until”). These were introduced by Kamp (1968). The intended meanings are

Spq q has been true since a time when p was true”
Upq q will be true until a time when p is true”

It is possible to define the one-place tense operators in terms of S and U as follows:

Pp Sp(p∨¬p)
Fp Up(p∨¬p)

The importance of the S and U operators is that they are expressively complete with respect to first-order temporal properties on continuous, strictly linear temporal orders (which is not true for the one-place operators on their own).

Metric tense logic. Prior introduced the notation Fnp to mean “It will be the case the interval n hence that p”. We do not need a separate notation Pnp since we can write F(-n)p for “It was the case the interval n ago that P”. The case n=0 gives us the present tense. We can define the general, non-metric operators by

Pp n(n<0 & Fnp)
Fp n(n>0 & Fnp)
Hp n(n<0→Fnp)
Gp n(n>0→Fnp)

The “next time” operator O. This operator assumes that the time series consists of a discrete sequence of atomic times. The formula Op is then intended to mean that p is true at the immediately succeeding time step. Given that time is discrete, it can be defined in terms of the “until” operator U by


which says that p will be true at some future time, between which and the present time nothing is true. This can only mean the time immediately following the present in a discrete temporal order.

In discrete time, the future-tense operator F is related to the next-time operator by the equivalence


Indeed, F can here be defined as the least fixed point of the transformation which maps an arbitrary propositional operator X onto the operator λp.OpOXp.

One could similarly define a past-time version of O; but since the main usefulness of this particular operator has been in relation to the logic of computer programming, where one is mainly interested in execution sequences of programs extending into the future, this has not so often been done.

1.3 Semantics of Tense Logic

The standard model-theoretic semantics of Tense Logic is closely modelled on that of Modal Logic. A temporal frame consists of a set T of entities called times together with an ordering relation < on T. This defines the “flow of time” over which the meanings of the tense operators are to be defined. An interpretation of the tense-logical language assigns a truth value to each atomic formula at each time in the temporal frame. Given such an interpretation, the meanings of the weak tense operators can be defined using the rules

Pp is true at t if and only if p is true at some time t′ such that t′<t
Fp is true at t if and only if p is true at some time t′ such that t<t

from which it follows that the meanings of the strong operators are given by

Hp is true at t if and only if p is true at all times t′ such that t′<t
Gp is true at t if and only if p is true at all times t′ such that t<t

We can now provide a precise characterisation of system Kt of Minimal Tense Logic. The theorems of Kt are precisely those formulae which are true at all times under all interpretations over all temporal frames.

Many tense-logical axioms have been suggested as expressing this or that property of the flow of time, and the semantics gives us a precise way of defining this correspondence between tense-logical formulae and properties of temporal frames. A formula p is said to characterise a set of frames F if

Thus any theorem of Kt characterises the class of all frames.

A first-order formula in < determines a class of frames, namely those in which the formula is true. A tense-logical formula p corresponds to a first-order formula q just so long as p characterises the class of frames for which q is true. Some well-known examples of such pairs of formulae are:

HpPp tt′(t′<t) (unbounded in the past)
GpFp tt′(t<t′) (unbounded in the future)
FpFFp t, t′(t<t′ → ∃t″(t<t″<t′)) (dense ordering)
FFpFp t, t′(∃t″(t<t″<t′) → t<t′) (transitive ordering)
FPp → Pp∨pFp t, t′, t″((t<t″ & t′<t″) →
    (t<t′ ∨ t=t′ ∨ t′<t))
(linear in the past)
PFp → Pp∨pFp t, t′, t″((t″<t & t″<t′) →
    (t<t′ ∨ t=t′ ∨ t′<t))
(linear in the future)

However, there are tense-logical formulae (such as GFpFGp) which do not correspond to any first-order temporal frame properties, and there are first-order temporal frame properties (such as irreflexivity, expressed by ∀t¬(t<t)) which do not correspond to any tense-logical formula. For details, see van Benthem (1983).

2. Predicate-logic approaches to temporal logic

2.1 The method of temporal arguments

In this method, the temporal dimension is captured by augmenting each time-variable proposition or predicate with an extra argument-place, to be filled by an expression designating a time, as for example

Kill(Brutus, Caesar, 44BCE).

If we introduce into the first-order language a binary infix predicate < denoting the temporal ordering relation “earlier than”, and a constant “now” denoting the present moment, then the tense operators can be readily simulated by means of the following correspondences, which not surprisingly bear more than a passing resemblance to the formal semantics for Tense Logic given above. Where p(t) represents the result of introducing an extra temporal argument place to the time-variable predicates occurring in p, we have:

Pp t(t<now & p(t))
Fp t(now<t & p(t))
Hp t(t<now → p(t))
Gp t(now<tp(t))

Before the advent of Tense Logic, the method of temporal arguments was the natural choice of formalism for the logical expression of temporal information.

2.2 Hybrid approaches

The reification of time instants implied by the method of temporal arguments may be regarded as philosophically suspect, instants being rather artificial constructs unsuited to playing a foundational role in temporal discourse. Following a suggestion of Prior (1968, Chapter XI), one might equate an instant with ‘the conjunction of all those propositions which would ordinarily be said to be true at that instant’. Instants are thus replaced by propositions which uniquely characterise them. A statement of the form “True(p, t)”, saying that proposition p is true at instant t, can then be paraphrased as “□ (tp)”, i.e., the instant-proposition t necessarily implies p.

This kind of manoeuvre lies at the heart of hybrid temporal logics in which the standard apparatus of propositions and tense operators is supplemented by propositions which are true at unique instants, thereby effectively naming those instants without invoking philosophically dubious reification. This can give one some of the expressive power of a predicate-logic approach while retaining the modal character of the logic. (See Areces and Ten Cate, 2006)

2.3 State and event-type reification

The method of temporal arguments encounters difficulties if it is desired to model aspectual distinctions between, for example, states, events and processes. Propositions reporting states (such as “Mary is asleep”) have homogeneous temporal incidence, in that they must hold over any subintervals of an interval over which they hold (e.g., if Mary is asleep from 1 o'clock to 6 o'clock then she is asleep from 1 o'clock to 2 o'clock, from 2 o'clock to 3 o'clock, and so on). By contrast, propositions reporting events (such as “John walks to the station”) have inhomogeneous temporal incidence; more precisely, such a proposition is not true of any proper subinterval of an interval of which it is true (e.g., if John walks to the station over the interval from 1 o'clock to a quarter past one, then it is not the case that he walks to the station over the interval from 1 o'clock to five past one — rather, over that interval he walks part of the way to the station).

The method of state and event-type reification was introduced to cater for distinctions of this kind. It is an approach that has been especially popular in Artificial Intelligence, where it is particularly associated with the name of James Allen, whose influential paper (Allen 1984) is often cited in this connection. In this approach, state and event types are denoted by terms in a first-order theory; their temporal incidence is expressed using relational predicates “Holds” and “Occurs”, as for example,

Holds(Asleep(Mary), (1pm, 6pm))
Occurs(Walk-to(John, Station), (1pm, 1.15pm))

where terms of the form (t, t′) denote time intervals in the obvious way.

The homogeneity of states and inhomogeneity of events is secured by axioms such as

s, i, i′(Holds(s, i) & In(i′, i) → Holds(s, i′))
e, i, i′(Occurs(e, i) & In(i′, i) → ¬Occurs(e, i′))

where “In” expresses the proper subinterval relation.

2.4 Event-token reification

The method of event-token reification was proposed by Donald Davidson (1967) as a solution to the so-called “variable polyadicity” problem. The problem is to give a formal account of the validity of such inferences as

John saw Mary in London on Tuesday.
Therefore, John saw Mary on Tuesday.

The key idea is that each event-forming predicate is endowed with an extra argument-place to be filled with a variable ranging over event-tokens, that is, particular dated occurrences. The inference above is then cast in logical form as

e(See(John, Mary, e) & Place(e, London) & Time(e, Tuesday)),
Therefore, ∃e(See(John, Mary, e) & Time(e, Tuesday)).

In this form, the inference does not require any additional logical apparatus over and above standard first-order predicate logic; on that basis, the validity of the inference is considered to be explained. This approach has also been used in a computational context in the Event Calculus of Kowalski and Sergot (1986).

3. Philosophical issues

Prior's motivation for inventing Tense Logic was largely philosophical, his idea being that the precision and clarity afforded by a formal logical notation was indispensible for the careful formulation and resolution of philosophical issues concerning time. See the article on Arthur Prior for a discussion of some of these.

3.1 Realist vs reductionist approaches to tense

The rivalry between the modal and first-order approaches to formalising the logic of time reflects an important set of underlying philosophical issues related to the work of McTaggart. This work is especially well-known, in the context of temporal logic, for introducing the distinction between the “A-series” and the “B-series”. By the “A-series” is meant, essentially, the characterisation of events as Past, Present, or Future. By contrast, the “B-series” involves their characterisation as relatively “Earlier” or “Later”. A-series representations of time inescapably single out some particular moment as present; of course, at different times, different moments are present — a circumstance which, followed to what appeared to be its logical conclusion, led McTaggart to assert that time itself was unreal (see Mellor, 1981). B-series representations have no place for a concept of the present, instead taking the form of a synoptic view of all time and the (timeless) interrelations between its parts.

There is a clear affinity between the A-series and the modal approach and between the B-series and the first-order approach. In the terminology of Massey (1969), adherents of the former approach are called “tensers” while adherents of the latter are called “detensers”. This issue is related in turn to the question of how seriously to take the representation of space-time as a single four-dimensional entity in which the four dimensions are at least in some respects on a similar footing. In view of the Theory of Relativity, it might be argued that this issue is not so much a matter for Philosophy as for Physics.

3.2 Determinism vs non-determinism

The choice of flow of time can be of philosophical significance. For example, one way of capturing the distinction between deterministic and non-deterministic theories is to model the former using a strictly linear flow of time, and the latter with a temporal structure which allows branching into the future. If we adopt the latter approach, then it is helpful in describing the semantics of tense and other operators to introduce the idea of a history, which is a maximal linearly-ordered set of instants. The branching future model will then stipulate that for any two histories there is an instant such that both histories share all the times up to and including that instant, but do not share any times after it. For each history containing a given instant, the times in that history which are later than the instant constitute a “possible future” for that instant.

In branching time semantics it is natural to evaluate formulae with respect to an instant and a history, rather than just an instant. With respect to the pair (h, t), we might interpret “Fp” to be true so long as “p” is true at some time in the future of t as determined by the history h. A separate operator ◊ can be introduced to allow, in effect, quantification over histories: “◊p” is true at (h, t) so long as there is some history h’ such that “p” is true at (h’, t). Then “◊Fp” says that “p” holds in some possible future, and “□Fp” (where “□” is the strong modal operator dual to “◊”) says that “p” is inevitable (i.e., holds in all possible futures). Prior calls this kind of interpretation “Ockhamist”.

Another interpretation (called “Peircean” by Prior) takes “Fp” to be equivalent to the Ockhamist “□Fp”, i.e., “p” is true at some time in every possible future. Under this interpretation there is no formula equivalent to the Ockhamist “Fp”; hence Peircean tense logic is a proper fragment of Ockhamist tense logic. It was favoured by Prior on the grounds that future contingent propositions really do lack truth value: only if a future-tense proposition is inevitable (all possible futures) or impossible (no possible futures) can we ascribe a truth value to it now. For Prior's discussion of these issues, see Prior 1967, Chapter VII. Further discussion can be found in Øhrstrøm, and Hasle 1995, chapters 2.6 and 3.2.

The non-determinism implicit in branching time frames has led to their being used to support theories of action and choice. An important example is the STIT logics of Belnap and Perloff (1988), with many subsequent variants (see Xu, 1995). The primitive expression of agency in STIT theories is that an agent a “sees to it that” some proposition P holds, written [a stit: P]. The meaning of this construction is specified in relation to a branching time structure, in which the choices made by agents are representated by means of sets of possible futures branching forward from the choice point. The precise interpretation of [a stit: P] varies from one system to another, but typically it is specified to be true at a particular moment if P holds in all histories selected by the agent's choice function at that moment, with the further condition usually added that P fails to hold in at least one history not so selected (this is in order to avoid the unwelcome conclusion that an agent sees to it that some tautology holds).

4. Applications of Temporal Logic

4.1 Applications to natural language

Prior (1967) lists amongst the precursors of Tense Logic Hans Reichenbach's (1947) analysis of the tenses of English, according to which the function of each tense is to specify the temporal relationships amongst a set of three times related to the utterance, namely S, the speech time, R, the reference time, and E, the event time. In this way Reichenbach was neatly able to distinguish between the simple past “I saw John”, for which R=E<S, and the present perfect “I have seen John”, for which E<R=S, the former statement referring to a past time coincident with the event of my seeing John, the latter referring to the present time, relative to which my seeing John is past.

Prior notes that Reichenbach's analysis is inadequate to account for the full range of tense usage in natural language. Subsequently much work has been done to refine the analysis, not only of tenses but also other temporal expressions in language such as the temporal prepositions and connectives (“before”, “after”, “since”, “during”, “until”), using the many varieties of temporal logic. For some examples, see Dowty (1979), Galton (1984), Taylor (1985), Richards et al. (1989). A useful collection of landmark papers in this area is Mani et al. (2005).

4.2 Applications in artificial intelligence

We have already mentioned the work of Allen (1984), which is concerned with finding a general framework adequate for all the temporal representations required by AI programs. The Event Calculus of Kowalski and Sergot (1986) is pursued more specifically within the framework of logic programming, but is otherwise similarly general in character. A useful survey of issues involving time and temporal reasoning in AI is Galton (1995), and a comprehensive recent coverage of the area is Fisher et al. (2005).

Much of the work on temporal reasoning in AI has been closely tied up with the notorious frame problem, which arises from the necessity for any automated reasoner to know, or be able to deduce, not only those properties of the world which do change as the result of any event or action, but also those properties which do not change. In everyday life, we normally handle such facts fluently without consciously adverting to them: we take for granted without thinking about it, for example, that the colour of a car does not normally change when one changes gear. The frame problem is concerned with how to formalise the logic of actions and events in such a way that indefinitely many inferences of this kind are made available without our having to encode them all explicitly. A seminal work in this area is McCarthy and Hayes (1969). A useful recent reference for the frame problem is Shanahan, 1997.

4.3 Applications in computer science

Following Pnueli (1977), the modal style of Temporal Logic has found extensive application in the area of Computer Science concerned with the specification and verification of programs, especially concurrent programs in which the computation is performed by two or more processors working in parallel. In order to ensure correct behaviour of such a program it is necessary to specify the way in which the actions of the various processors are interrelated. The relative timing of the actions must be carefully co-ordinated so as to ensure that integrity of the information shared amongst the processors is maintained. Amongst the key notions here is the distinction between “liveness” properties of the tense-logical form Fp, which ensure that desirable states will obtain in the course of the computation, and “safety” properties of the form Gp, which ensure that undesirable states will never obtain.

Non-determinism is an important issue in computer science applications, and hence much use has been made of branching time models. Two important such systems are CTL (Computation Tree Logic) and a more expressive system CTL*; these correspond very nearly to the Ockhamist and Peircean semantics discussed above.

Further information may be found in Galton (1987), Goldblatt (1987), Kroger (1987), Bolc and Szalas (1995).


Other Internet Resources

Related Entries

artificial intelligence: logic and | frame problem | logic: hybrid | logic: modal | Prior, Arthur | time