Temporal Logic

First published Mon Nov 29, 1999; substantive revision Fri May 3, 2024

Broadly construed,Temporal Logic covers all formalapproaches to representing and reasoning about time and temporalinformation. More narrowly, it usually refers to the modal-logic styleapproach introduced by Arthur Prior in the 1950s under the nameTense Logic and subsequently developed further by manylogicians and computer scientists. Temporal Logic has been widely usedas a formalism for clarifying philosophical issues about time, as aframework for defining the semantics of temporal expressions innatural language, as a language for encoding temporal knowledge inartificial intelligence, and as a tool for specification andverification of computer programs and systems.

Here we provide a broadly representative — yet concise andinevitably incomplete — overview of the rich variety of temporalmodels and logics introduced and studied over the past 70 years orso.

1. Temporal reasoning from antiquity to modern days

Discussions of temporality and reasoning about time go back toantiquity, and examples can even be found in the Bible (Boyd 2014).Zeno’s famous flying arrow paradox refers to the nature of timeand challenges the notion of change. Much of the early temporaldiscussion, however, centered around the problem offuturecontingents, i.e. the question whether statements about futureevents that are neither necessary nor impossible can have definitetruth values. The most widely known and probably most cited example isthe sea-battle scenario discussed by Aristotle inOnInterpretation (Chapter 9). Aristotle argued that statements suchas “There will be a sea-battle tomorrow”, as well as thecontrary prediction “There will not be a sea-battletomorrow”, do not hold of necessity and hence lack definitetruth values at present, while conceding that it is necessary thateither there will be a sea-battle tomorrow or not. Somewhat later, thephilosopher Diodorus Chronus demonstrated the problem of futurecontingents in his famousMaster Argument, which led him todefine the possible as “what is or will be the case”. Adetailed discussion of Diodorus’ argument is provided in e.g.Rescher and Urquhart (1971, Chapter XVII) and the entry onfuture contingents.

Philosophical discussions concerning time and the contingency of thefuture continued in the Middle Ages, where the theme was taken up bywriters such as Peter Aureole, William of Ockham, and Luis Molina. Thecentral question here was how to reconcile God’s foreknowledgewith the idea of human freedom. Ockham, for example, embraced the ideaof a true or actual future, holding that future contingents are eithertrue or false even though only God knows their truth values. Accordingto Ockham, this is not to say, however, that future contingents arenecessary: there are alternative possibilities for humans to choosefrom. Later, several philosophers and logicians engaged in the problemof relating time and modality, proposing various different solutions.C.S. Peirce objected to the idea that future contingents can havedefinite truth values. He advanced the view that only the present andthe past are actual, whereas the future is the realm of possibilityand necessity. In a similar spirit, J. Łukasiewicz devised athree-valued logic, treating the truth values of future contingents asundetermined. For a more recent philosophical discussion on the openfuture, indeterminism, and free will, see e.g. Belnap et al. (2001),Correia and Iacona (2013), and Müller (2014).

The modern era of formal temporal logic was initiated by the seminalwork of Arthur N. Prior, with important precursors such as H.Reichenbach, J. Findlay, J. Łukasiewicz, and J. Łoś.^[1] From the early 1950s, Prior introduced and analyzed in detail overmore than a decade several different versions of Tense Logic, many ofwhich are discussed here. Prior’s invention of Tense Logic waslargely driven by philosophical considerations. In particular, theMaster Argument of Diodorus Chronus and the intricate relationshipbetween time, (in)determinism, God’s foreknowledge, and humanfreedom played a pivotal role in his work. Prior was convinced that aproper logical approach could help to clarify and resolve suchphilosophical problems. He introduced temporal operators, studiedmetric tense logic, was a pioneer in hybrid logic, and devised twoversions of branching time logic, which he took to reflect the viewsof Ockham and Peirce, respectively. His work paved the way for thedevelopment of the vast and diverse field of temporal logic, withnumerous important applications not only in philosophy, but also incomputer science, artificial intelligence, and linguistics. For moreon Prior’s views and work, see the special issue Albretsen etal. (2016), the four volumes of the recent book seriesLogic andPhilosophy of Time (Hasle et al. 2017; Blackburn et al. 2019;Jakobsen et al. 2020; Hasle et al. 2020); and the entry onArthur Prior. A comprehensive overview of the history of temporal reasoning andlogics is provided in Øhrstrøm and Hasle (1995). Seealso Øhrstrøm and Hasle (2006) and Dyke and Bardon(2013, Part I).

2. Formal models of time

Philosophers have extensively discussed the ontological nature andproperties of time. Several aspects of the debate are reflected in therich variety of formal models of time as they have been explored intemporal logics. For example, is time instant-based or interval-based?Is it discrete, dense, or continuous? Does time have a beginning or anend? Is it linear, branching, or circular? Before we turn to theformal languages of temporal logics and their semantics, we brieflyintroduce below the two most basic types of formal models of timetogether with some of their pertinent properties: instant-based andinterval-based models.

2.1 Instant-based models of time

In instant-based models, the primitive temporal entities are points intime, i.e.time instants, and the basic relationship betweenthem istemporal precedence. Accordingly, the flow of time isrepresented by a non-empty set of time instants \(T\) with a binaryrelation \(\prec\) of precedence on it: \(\mathcal{T} = \left\langleT, \prec \right\rangle.\)

There are some basic properties which can naturally be imposed oninstant-based flows of time. The temporal precedence relation\(\prec\) is usually required to be a strict partial ordering, thatis, an irreflexive, transitive, and hence asymmetric relation. Incomputer science, however, one often uses the reflexive closure\(\preceq \) of the precedence relation, and then the asymmetrycondition is replaced by antisymmetry. A list of key properties isprovided below.

One fundamental distinction in the realm of instant-based models oftime is the distinction between linear models, where the flow of timeis depicted as a line, and backward-linear models, which allow for atree-like representation, supporting the view that the past is fixed(and hence linear) while the future may be open (branching intomultiple future possibilities). In either case, the temporal orderingmay or may not contain minimal or maximal elements, corresponding tofirst or last instants in time, respectively.

Another important distinction is between discrete models of time,which are prevalent in computer science, and dense or continuous ones,which are more common in natural sciences and philosophy. Inforward-discrete (resp. backward-discrete) models, each time instantthat has a successor (resp. predecessor) has an immediate successor(resp. immediate predecessor). In dense models, by contrast, betweenany two subsequent time instants, there is another instant.

Many, but not all, properties that may be imposed on an instant-basedmodel of time \(\mathcal{T} = \left\langle T, \prec \right\rangle\)can be expressed by first-order sentences as follows (where\(\preceq\) is an abbreviation of \(x\prec y \lor x=y\)):

reflexivity: \(\forall x (x\prec x);\)
irreflexivity: \(\forall x\lnot (x\prec x);\)
transitivity: \(\forall x\forall y\forall z(x\precy\wedge y\prec z\rightarrow x\prec z);\)
asymmetry: \(\forall x\forall y \lnot(x\prec y\wedgey\prec x);\)
antisymmetry: \(\forall x\forall y(x\prec y\wedge y\precx\rightarrow x=y);\)
linearity (trichotomy): \(\forall x\forall y(x=y\veex\prec y\vee y\prec x);\)
forward-linearity: \(\forall x\forall y\forall z(z\precx\wedge z\prec y\rightarrow (x=y \vee x \prec y\vee y\prec x));\)
backward-linearity: \(\forall x\forall y\forall z(x\precz\wedge y\prec z\rightarrow (x=y \vee x \prec y\vee y\prec x));\)
beginning: \(\exists x\lnot\exists y(y\prec x);\)
end: \(\exists x\lnot\exists y(x\prec y);\)
no beginning (backward-seriality): \(\forall x\existsy(y\prec x);\)
no end (forward-seriality, unboundedness): \(\forallx\exists y(x\prec y);\)
density: \(\forall x\forall y(x\prec y\rightarrow \existsz(x\prec z\wedge z\prec y));\)
forward-discreteness: \(\forall x\forall y(x\precy\rightarrow \exists z(x\prec z \wedge z\preceq y \wedge \lnot\existsu(x\prec u\wedge u\prec z)));\)
backward-discreteness: \(\forall x\forall y(y\precx\rightarrow \exists z(z\prec x \wedge y\preceq z \wedge \lnot\existsu(z\prec u\wedge u\prec x))).\)

Note that, in linear models, the two discreteness conditions simplifyto

\(\forall x\forall y(x\prec y\rightarrow \exists z(x\prec z \wedge\forall u(x\prec u \rightarrow z\preceq u)))\) and
\(\forall x\forall y(y\prec x\rightarrow \exists z(z\prec x \wedge\forall u(u\prec x \rightarrow u\preceq z))),\) respectively.

Key examples of properties that cannot be expressed by first-ordersentences, but require a second-order language with quantificationover sets, arecontinuity,well-ordering, thefinite interval property, andforward/backwardinduction. Continuity demands that there be ‘no gaps’in the temporal order. Not only must the temporal order be dense, itmust also beDedekind complete (i.e., every non-empty set oftime instants that has an upper bound has a least upper bound). Theordering of the real numbers fulfills this condition, but the rationalnumbers do not. To see this, consider the set of all rational numberswhose square is less than 2 and note that \(\sqrt{2}\) is notrational. An instant-based model of time is well-ordered if there areno infinite descending chains (i.e., every non-empty, linear set oftime instants has a least element), and it has the finite intervalproperty if between any two comparable time instants there are at mostfinitely many instants. The natural numbers are well-ordered and havethe finite interval property, the integers are not well-ordered buthave the finite interval property, and the rationals are neitherwell-ordered nor do they have the finite interval property. Lastly, apartial order is forward (resp. backward) inductive if there are‘no transfinite forward (resp. backward) jumps’ (i.e.,every infinite ascending (resp. descending) chain lacks a strict upper(resp. lower) bound). As we will see inSection 3.6, these second-order properties can be expressed in propositionaltemporal languages.

2.2 Interval-based models of time

In contrast to instant-based models of time, interval-based modelsrely ontime intervals, i.e. periods rather than instants, asthe primitive entities. They can, and have been, motivated byconsiderations concerning Zeno’s famous flying arrow paradox: Ifthe flying arrow is always at an instant and if at each instant thearrow is at rest, then how is movement possible? By modelling theflight of the arrow as an event that occupies a temporal interval theparadox can arguably be avoided. Other examples that naturally invokeinterval-based reasoning are: “Last night Alice cried a lotwhile writing the letter, and then she calmed down” and“Bill was drinking his tea when the postman came”.

Interval-based models usually presuppose linear time. But they arericher than instant-based models as there are more possiblerelationships between time intervals than between time instants. Aninterval-based model of time can, for instance, include the relationstemporal precedence \(\prec,\)inclusion\(\sqsubseteq,\) andoverlap \(O\) over a given set of timeintervals \(T\): formally, \(\mathcal{T}= \left\langleT,\prec,\sqsubseteq, O \right\rangle.\) Some natural properties ofsuch interval-based relations include:

reflexivity of \(\sqsubseteq:\) \(\forall x(x\sqsubseteqx);\)
antisymmetry of \(\sqsubseteq:\) \(\forall x\forally(x\sqsubseteq y\wedge y\sqsubseteq x\rightarrow x=y);\)
atomicity of \(\sqsubseteq\) (for discrete time):\(\forall x\exists y(y\sqsubseteq x\wedge \forall z(z\sqsubseteqy\rightarrow z=y));\)
downward monotonicity of \(\prec\) w.r.t.\(\sqsubseteq:\) \(\forall x\forall y\forall z(x\prec y\wedgez\sqsubseteq x\rightarrow z\prec y);\)
symmetry of \(O\): \(\forall x\forall y(xOy\rightarrowyOx);\)
overlapping intervals intersect in a subinterval:
\(\forall x\forall y (xOy \rightarrow \exists z( z \sqsubseteq x \landz \sqsubseteq y \land \forall u ( u \sqsubseteq x \land u \sqsubseteqy \to u \sqsubseteq z)));\)
monotonicity of \(\sqsubseteq\) w.r.t. \(O\): \(\forallx\forall y \forall z(x \sqsubseteq y \land xOz \rightarrow z\sqsubseteq y \lor zOy).\)

In an influential early work on interval-based temporal ontology andreasoning in AI, Allen (1983) considered the family of all binaryrelations that can arise between two intervals in a linear order,subsequently calledAllen relations. These 13 relations,displayed inTable 1, are mutually exclusive and jointly exhaustive, i.e., exactly one ofthem holds between any given pair of strict intervals (excludingpoint-intervals). Moreover, they turn out to be definable in terms ofonly two of them, viz. in terms of ‘meets’ and‘met-by’ (Allen 1983).

Interval relations	Allen’s notation	\(\textsf{HS}\) notation
┣━━┫	equals \(\{=\}\)
├──┤ ┣┫	before \(\{\lt\}\) /after \(\{\gt\}\)	\(\langle L\rangle\:/\:\langle\overline{L}\rangle\)Later
├──╊┫	meets \(\{m\}\) /met-by \(\{mi\}\)	\(\langle A\rangle\:/\:\langle\overline{A}\rangle\)After
├─╊┿━┫	overlaps \(\{o\}\) /overlapped-by\(\{oi\}\)	\(\langle O\rangle\:/\:\langle\overline{O}\rangle\)Overlaps
├─╊┫	finished-by \(\{fi\}\) /finishes\(\{f\}\)	\(\langle E\rangle\:/\:\langle\overline{E}\rangle\)Ends
├╊╉┤	contains \(\{di\}\) /during \(\{d\}\)	\(\langle D\rangle\:/\:\langle\overline{D}\rangle\)During
┣╉─┤	started-by \(\{si\}\) /starts \(\{s\}\)	\(\langle B\rangle\:/\:\langle\overline{B}\rangle\)Begins

Table 1: Allen relations between timeintervals and the corresponding Halpern-Shoham modal operators (seeSection 6).

More abstract questions can also be posed: assume, for example, thatwe are provided with a structure defined by a set of intervalrelations (of arbitrary arity) that are required to fulfill certainconditions. Can this structure be represented by a concreteinterval-based model over linear time? Answers are provided by variousrepresentation theorems, see e.g. van Benthem (1983); Ladkin (1987);and Venema (1990).

2.3 Instant-based vs. interval-based models of time

The choice between instants and intervals as the primary objects oftemporal ontology has been a highly debated philosophical theme sincethe times of Zeno and Aristotle (Øhrstrøm and Hasle1995). Technically, the two types of temporal ontologies are closelyrelated, and they are reducible to each other: on the one hand, timeintervals can be defined by pairs of time instants (beginning andend); on the other hand, a time instant can be construed as adegenerate interval, viz. as a point-interval whose beginning and endpoints coincide.

Still, the technical reductions do not resolve the question whethersentences are to be evaluated with respect to instants or with respectto intervals, and one may argue that both instants and intervals areneeded as mutually complementary. Two-sorted point-interval modelswere studied in e.g. Balbiani et al. (2011), and more complex modelsof time have been investigated as well, including models of timegranularity (Euzenat and Montanari 2005), which allow for differentresolution levels of temporal intervals (e.g. minutes, hours, days,years, etc.), metric and layered temporal models (Montanari 1996),etc.

Here we focus mainly on instant-based logics and discussinterval-based logics in somewhat less detail. For further discussionon the ontological primacy of instants versus intervals in temporallogics, see Hamblin (1972); Kamp (1979); Humberstone (1979); Galton(1996); as well as van Benthem (1983; 1984), who provides a detailedcomparative exploration of both approaches. A more philosophical andhistorical overview is provided in e.g. Øhrstrøm andHasle (1995; 2006); Dyke and Bardon (2013); Meyer (2013); and Goranko(2023).

3. Prior’s basic tense logic TL

In this section, we discuss the language, semantics, andaxiomatization of the basic tense logic TL introduced by Prior (1957;1967; 1968), who is widely regarded as the founding father of temporallogic. Prior’s motivation for inventing tense logic was largelyphilosophical, and his ideas were inspired by the use of tense innatural language. The innovative feature of Prior’s approach wasthat he treated propositions as tensed rather than tenseless.Technically, this was achieved by the introduction of temporaloperators into the language, which were given a modal-logic stylesemantics. In view of the pivotal role that tense played in hisframework, Prior himself referred to his account asTenseLogic, whereas nowadays the more general expressionTemporalLogic is more prevalent.

3.1 Prior’s tense operators

The basic language of Prior’s Tense Logic TL extends thestandard propositional language (with atomic propositions andtruth-functional connectives) by four temporal operators with intendedmeaning as follows:

\(P\):“It was(at some point in thePast) the case that…”
\(F\):“It will(at some point in theFuture) be the case that…”
\(H\):“ItHas always been the case that …”
\(G\):“It isalwaysGoing to be the case that …”

For example, “It will always be the case that Prior inventedTense Logic” translates in TL as \(GP(\mathsf{Prior\ invents\TL})\), which can be glossed as “It is always going to be thecase that it was the case that Prior invents Tense Logic”.Formulae not containing temporal operators are considered presenttensed.

The language of TL contains one pair of temporal operators for thepast, \(P\) and \(H\), and one pair of temporal operators for thefuture, \(F\) and \(G\). The operators \(P\) and \(F\) are oftenreferred to as the ‘weak’ temporal operators, while \(H\)and \(G\) are known as the ‘strong’ ones. The respectivepast and future operators are duals of each other, i.e., they areinterdefinable by means of the following equivalences:

\[P\varphi \equiv \neg H\neg \varphi, H\varphi \equiv \neg P\neg\varphi \text{ and } F\varphi \equiv \neg G\neg \varphi, G\varphi \equiv \negF\neg \varphi.\]

In light of these equivalences, the set of formulae of TL can berecursively defined as follows, over a given set of atomicpropositions \(PROP\): \[\varphi := p \in {PROP} \mid \lnot \varphi \mid (\varphi \land \varphi) \midP\varphi \mid F\varphi.\] The truth-functional connectives\(\vee,\to,\) and \(\leftrightarrow\) as well as the logical constants\(\top\) and \(\bot\) are definable in terms of \(\lnot\) and\(\land\) as usual. Besides, we can define \(A\varphi =H\varphi \wedge\varphi \wedge G\varphi\) and, dually, \(E\varphi =P\varphi \vee\varphi \vee F\varphi,\) which on linear flows of time mean“always” and “sometime”, respectively.

As said, Prior’s introduction of the temporal operators wasmotivated by the use of tense in natural language, and indeed, varioustenses in natural language can, at least approximately, be captured inTL. For example:

\(P\): “Prior(has) invented Tense Logic”.
\(F\): “Priorwill invent Tense Logic”.
\(PP\): “Priorhad invented Tense Logic”.
\(FP\): “Priorwill have invented Tense Logic”.
\(PF\):“Priorwould invent Tense Logic”.

Hamblin and Prior showed that, in models of linear time, any sequenceof temporal operators reduces to a sequence of at most two operators.In total, they identified 15 different such combinations — ortenses, as they called them (see Prior 1967, Chapter III.5).These combinations seem to surpass the number of verbal tenses in e.g.English, but there are also temporal features of natural language thatcannot be captured in TL: Prior’s temporal operators cannot, forinstance, distinguish between the simple past and the present perfect(“I wrote a letter” vs. “I have written aletter”), a distinction that drove Reichenbach’s work.Moreover, they are not suited to model the linguistic differentiationbetween perfective and imperfective aspect (“I wrote aletter” vs. “I was writing a letter”), which isarguably more adequately dealt with in an interval-based framework.For details, see Kuhn and Portner (2006) and the entry ontense and aspect.

3.2 Semantics of TL

The standard semantics of TL is essentially a Kripke-style semantics,familiar from modal logic. In modal logic, sentences are evaluatedover so-called Kripke frames consisting of a non-empty set of possibleworlds and an accessibility relation between them. In temporal logic,the possible worlds are time instants, and the accessibility relationhas a concrete interpretation in terms of temporal precedence. Inother words, sentences are evaluated over instant-based models of time\(\mathcal{T}=\left\langle T, \prec \right\rangle\), hereafter calledtemporal frames. Note that so far no conditions, liketransitivity, irreflexivity, etc., are imposed on the precedencerelation \(\prec\).

Given a set of atomic propositions \(PROP\), atemporal modelfor TL is a triple \(\mathcal{M}= \left\langle T, \prec, V\right\rangle\) where \(\mathcal{T} =\left\langle T, \prec\right\rangle\) is a temporal frame and \(V: PROP \rightarrow\mathcal{P}(T)\) is avaluation function that assigns to eachatomic proposition \(p\in{PROP}\) the set of time instants \(V(p)\subseteq T\) at which \(p\) is considered true. (Equivalently, thevaluation can be given by a function \(I: T\times{PROP}\to\{\mathit{true},\mathit{false}\},\) which assigns a truth value toeach atomic proposition at each time instant in the temporal frame, orby alabeling orstate description \(L: T \to\mathcal{P}({PROP})\), which assigns to each time instant the set ofatomic propositions that are considered true at that instant.)

Thetruth of an arbitrary formula \(\varphi\) of TL at a giventime instant \(t\) in a temporal model \(\mathcal{M}\) (denoted\(\mathcal{M},t \models\varphi\)) is then defined inductively asfollows:

\(\mathcal{M},t \models p\) iff \(t \in V(p)\), for\(p \in {PROP}\);
\(\mathcal{M},t \models \neg\varphi\) iff \(\mathcal{M},t \not\models\varphi\) (i.e., it is not the case that\(\mathcal{M},t \models \varphi\));
\(\mathcal{M},t \models \varphi \wedge \psi\) iff \(\mathcal{M},t \models\varphi\) and \(\mathcal{M},t\models\psi\);
\(\mathcal{M},t \models P\varphi\) iff \(\mathcal{M},t'\models \varphi\) for some time instant \(t'\) suchthat \(t'\prec t{;}\)
\(\mathcal{M},t \models F\varphi\) iff \(\mathcal{M},t'\models \varphi\) for some time instant \(t'\) suchthat \(t\prec t'.\)

That is, a formula of the form \(P\varphi\) is true at an instant\(t\) iff \(\varphi\) is true at some earlier instant \(t',\) while\(F\varphi\) is true at \(t\) iff \(\varphi\) is true at some laterinstant \(t'.\) Accordingly, for the duals \(H\) and \(G\), we havethat \(H\varphi\) is true at \(t\) iff \(\varphi\) is true at allearlier instants \(t',\) and \(G\varphi\) is true at \(t\) iff\(\varphi\) is true at all later instants \(t'.\)

\(\mathcal{M},t \models H\varphi\) iff \(\mathcal{M},t'\models \varphi\) for all time instants \(t'\) suchthat \(t'\prec t\);
\(\mathcal{M},t \models G\varphi\) iff \(\mathcal{M},t'\models \varphi\) for all time instants \(t'\) suchthat \(t\prec t'\).

Note that, from the point of view of modal logic, there are twodifferent accessibility relations involved here: an‘earlier-relation’ in the case of the past operators and a‘later-relation’ in the case of the future operators. Intemporal logic, these two relations are covered by a single precedencerelation; after all, ‘earlier’ and ‘later’ arejust converses of each other (i.e., \(t\) is earlier than \(t'\) iff\(t'\) is later than \(t\)).

A formula \(\varphi\) of TL isvalid in a temporal model\(\mathcal{M}\) (denoted \(\mathcal{M} \models \varphi\)) iff itis true at every time instant in that model. Moreover, we say that\(\varphi\) isvalid in a temporal frame \(\mathcal{T}\)(denoted \(\mathcal{T} \models \varphi\)) iff it is valid in everymodel on that frame. Accordingly, a formula \(\varphi\) isvalid (denoted \(\models \varphi\)) iff it is valid in alltemporal frames, i.e. true at all time instants in all temporalmodels. A formula \(\varphi\) issatisfiable iff its negationis not valid, i.e. if \(\varphi\) is true at some time instant in sometemporal model.

3.3 Standard translation of TL into first-order logic

As in the case of modal logic, the language and semantics of TL can betranslated into classical first-order logic (see e.g. van Benthem1983).

Suppose that the set of atomic propositions of TL is given by\({PROP}=\left\{p_{0},p_{1},...\right\}\), and let \(L_{1}\) be afirst-order language with a denumerable set of unary predicate symbols\(\mathcal{P}=\left\{P_{0},P_{1},...\right\}\), one for each atomicproposition of TL, and a binary predicate symbol \(R\) for theprecedence relation. Thestandard translation \(ST\) of TLinto \(L_{1}\) is defined as follows, where \(\theta[y/x]\) is theresult of substituting \(y\) for all free occurrences of \(x\) in\(\theta\):

\(ST(p_{i}) = P_{i}(x);\)
\(ST(\lnot\varphi) = \lnot ST(\varphi);\)
\(ST(\varphi \land \psi) = ST(\varphi)\land ST(\psi);\)
\(ST(P\varphi) = \exists y(yRx\wedge ST(\varphi)[y/x]),\) where\(y\) is a new variable (i.e. one unused so far);
\(ST(F\varphi) = \exists y(xRy\wedge ST(\varphi)[y/x]),\) where\(y\) is a new variable.

It then follows that

\(ST(H\varphi) = \forall y(yRx\rightarrowST(\varphi)[y/x]);\)
\(ST(G\varphi) = \forall y(xRy\rightarrowST(\varphi)[y/x]).\)

For example:

\[ST(Gp_{1}\lor FHp_{2})=\forall y(xRy\rightarrowP_{1}(y))\lor \exists y(xRy\wedge \forall z(zRy\rightarrowP_{2}(z))).\]

Not every first-order formula has a correspondent in TL. Actually, bycarefully re-using variables, TL can be translated into thetwo-variable fragment FO\(^{2}\) of first-order logic, whicheventually implies decidability (since validity in FO\(^{2}\) isdecidable, as shown by Grädel and Otto 1999). For instance, theexample above can be re-written as

\[ST(Gp_{1}\lor FHp_{2})=\forall y(xRy\rightarrowP_{1}(y))\lor \exists y(xRy\wedge \forall x(xRy\rightarrow P_{2}(x))).\]

Given the standard translation, every temporal model\(\mathcal{M}=\left\langle T,\prec ,V\right\rangle\) can be regardedas an \(L_{1}\)-model where \(R\) is interpreted by \(\prec\) and each\(P_{i}\) by \(V(p_{i}).\) Then:

\[\begin{align}\mathcal{M},t \models \varphi \ & \text{ iff } \mathcal{M}\models ST(\varphi)[x:=t], \\\mathcal{M} \models \varphi \ & \text{ iff } \mathcal{M}\models \forall x ST(\varphi).\end{align}\]

Thus, validity of a formula of TL in a temporal model is a first-orderproperty. Validity in a temporal frame, on the other hand, turns outto be a second-order property as it involves universal quantificationover valuations. If we treat the unary predicates from \(\mathcal{P}\)as predicatevariables of a second-order language \(L_{2}\)that range over all subsets of \(T\), every temporal frame\(\mathcal{T} = \langle T,\prec\rangle\) can be regarded as an\(L_{2}\)-model. We have:

\[\begin{align}\mathcal{T}\models \varphi \ & \text{ iff }\mathcal{T}\models \forall P_0 \forall P_1\dots\forall x ST(\varphi), \\\models \varphi \ & \text{ iff }\models \forall P_0 \forall P_1\dots\forall x ST(\varphi). \end{align}\]

The standard translation of TL into first-order logic enables asystematic treatment of various aspects of temporal logic with thetools and techniques of classical logic (see e.g. van Benthem 2001;Blackburn et al. 2007). However, since TL validity is essentiallysecond-order, when it comes to frame definability, there are alsointeresting divergences. As we will see inSection 3.6, not all first-order properties of temporal frames are definable bytemporal formulae; and vice versa, not all properties of temporalframes that can be expressed by formulae of TL are first-orderdefinable. A non-trivial correspondence between temporal logic andfirst-order logic as alternative languages for describing propertiesof time emerges, see e.g. van Benthem (1995).

3.4 Tense logic, first-order logic, and McTaggart’s time series

The standard translation discussed in the previous section links thesemantics of Prior’s basic tense logic to first-order logic.Yet, there are crucial differences between the two approaches. Infact, in the early days of temporal logic, Prior’s approach wasperceived as a rival to more conventional approaches using first-orderlogic. The rivalry between tense logic and first-order logic can beseen as reflecting a fundamental distinction concerning the nature oftime, namely the distinction between the A-series and the B-series oftime introduced by McTaggart (1908).

Roughly speaking, the A-series characterizes time and temporal orderin terms of past, present, and future. The B-series, in contrast, isbased on the notions ‘earlier’ and ‘later’.McTaggart argued that the B-series is insufficient because it lacks anappropriate notion of change, and he rejected the A-series asinconsistent because what is future now will be past, which, accordingto him, requires that one and the same time instant has incompatibleproperties. From this he concluded that time is unreal. For a detaileddiscussion of McTaggart’s account and its philosophicalrelevance, see Ingthorsson (2016) and the entry ontime.

There is arguably a close correspondence between the A-seriesconception of time and tense logic, on the one hand, and between theB-series conception and first-order logic, on the other, as wasalready noted by Prior (1967, Chapter 1). Consider, for example, thesentence “It was light, it is dark, and it will be lightagain.” This sentence can be formalized in TL as \[P(\mathsf{light}) \wedge \mathsf{dark} \wedge F(\mathsf{light})\]while its first-order formulation reads \[\exists t_0 (t_0 \prec t_1 \wedge \mathsf{light}(t_0)) \wedge \mathsf{dark}(t_1) \wedge \exists t_2 (t_1 \prec t_2 \wedge \mathsf{light}(t_2)).\] The TL formulaconsists of tensed propositions, and it invokes the local perspectiveof the present. Accordingly, the truth value of the formula changesover time. The first-order formula, by contrast, is built up fromtenseless propositions and has a fixed truth value once and for all.Here we are provided with predicates of time instants rather thantenses, and the perspective involved is an overarching, global one.Prior felt that not everything that can be expressed in a tensedlanguage can likewise be expressed in a tenseless one, his classicexample being: “Thank goodness, that’s over!” (Prior1959).

3.5 Axiomatic system \(\mathbf{K}_{t}\) for TL

Like every formal logical system, temporal logic has two majoraspects: asemantic and adeductive one. In thissection, we present a deductive system for TL, viz. theminimaltemporal logic \(\mathbf{K}_{t}\). The system we are providing isa Hilbert-style axiomatic one, i.e., it consists of lists of axiomsand inference rules. The system was first studied by Lemmon, followingearlier axiomatizations proposed by Hamblin and Prior (see Rescher andUrquhart 1971, Chapter VI).

The list of axioms of the minimal temporal logic \(\mathbf{K}_{t}\)extends classical propositional logic by the following four axiomschemata:

\((K_H)\)\(H(\varphi\rightarrow \psi)\rightarrow (H\varphi \rightarrow H\psi)\)
\((K_G)\)\(G(\varphi\rightarrow \psi)\rightarrow (G\varphi \rightarrow G\psi)\)
(GP)\(\varphi\rightarrow GP\varphi\)
(HF)\(\varphi\rightarrow HF\varphi\)

The first two axiom schemata are the temporal correspondents of theso-calledK-axiom of modal logic, hence the terminology\(\mathbf{K}_{t}\). The third and fourth axiom schemata capture theinteraction of the past and future operators. They guarantee thatthese operators exploit converse temporal relations, viz. earlier andlater, respectively.

The inference rules comprise, in addition to the classicalmodusponens, twonecessitation rules for the temporaloperators (where \(\vdash\) means “deducible”):

(MP)If \(\vdash\varphi \rightarrow \psi\) and \(\vdash \varphi,\) then \(\vdash\psi.\)
(NEC\(_H\))If \(\vdash\varphi,\) then \(\vdash H\varphi.\)
(NEC\(_G\))If \(\vdash\varphi,\) then \(\vdash G\varphi.\)

The axiomatic system \(\mathbf{K}_{t}\) is sound and complete forvalidity in TL: all and only those formulae that are valid in TL canbe deduced from the axioms according to the rules. For a proof, seee.g. Rescher and Urquhart (1971); McArthur 1976; Goldblatt (1992); andGabbay et al. (1994).

3.6 Expressing temporal properties in TL and extensions of \(\mathbf{K}_{t}\)

The minimal temporal logic \(\mathbf{K}_{t}\) captures thosevalidities of TL that do not depend on any specific assumptionsconcerning the properties of the temporal precedence relation. In thissection, we will see that many natural properties of temporal framescan be expressed by temporal formulae, and, taken as additionalaxioms, these formulae can often be used to define logics on therelevant subclasses of temporal frames.

A temporal formula of TLexpresses (defines orcorresponds to) a property of temporal frames if the formulais valid in all and only those frames that have the property. The mostimportant correspondences between properties of temporal frames (seelist inSection 2.1) and TL formulae include:

(REF)	any of \(H\varphi \rightarrow \varphi,\) \(G\varphi \rightarrow\varphi,\) \(\varphi \rightarrow P\varphi,\) or \(\varphi \rightarrowF\varphi\) (reflexivity)
(TRAN)	any of \(H\varphi \rightarrow HH\varphi,\) \(G\varphi\rightarrow GG\varphi,\) \(PP\varphi \rightarrow P\varphi,\) or\(FF\varphi \rightarrow F\varphi\) (transitivity)
(LIN-F)	\(PF\varphi \rightarrow (P\varphi \vee \varphi \vee F\varphi)\)or \(F\varphi \wedge F\psi \rightarrow (F(\varphi\wedge \psi) \veeF(F\varphi \wedge \psi) \vee F(\varphi \wedge F\psi))\) (forward-linearity)
(LIN-P)	\(FP\varphi \rightarrow (P\varphi \vee \varphi \vee F\varphi)\)or \(P\varphi \wedge P\psi \rightarrow (P(\varphi\wedge \psi) \veeP(P\varphi \wedge \psi) \vee P(\varphi \wedge P\psi))\) (backward-linearity)
(LIN)	\((PF\varphi \lor FP\varphi) \rightarrow (P\varphi \vee \varphi\vee F\varphi)\) (linearity)
(BEG)	\(H\bot \vee PH\bot\) (time has a beginning, assuming irreflexivityand transitivity)
(END)	\(G\bot \vee FG\bot\) (time has an end, assuming irreflexivity andtransitivity)
(NOBEG)	\(P\top\) or \(H\varphi\rightarrow P\varphi\) (time has no beginning)
(NOEND)	\(F\top\) or \(G\varphi\rightarrow F\varphi\) (time has no end)
(DENSE)	any of \(HH\varphi \rightarrow H\varphi,\) \(GG\varphi\rightarrow G\varphi,\) \(P\varphi \rightarrow PP\varphi,\) or\(F\varphi \rightarrow FF\varphi\) (density)
(DISCR-F)	\((F\top \wedge \varphi \wedge H\varphi) \rightarrowFH\varphi\) (forward-discreteness, assumingforward-linearity)
(DISCR-P)	\((P\top \wedge \varphi \wedge G\varphi) \rightarrowPG\varphi\) (backward-discreteness, assumingbackward-linearity)
(COMPL)	\((FG\lnot\varphi \wedge F\varphi) \rightarrow F(G\lnot\varphi\wedge HF\varphi)\) or \(A(H\varphi \rightarrow FH\varphi)\rightarrow (H\varphi \rightarrowG\varphi)\) (Dedekind completeness, recall that \(A\varphi =H\varphi \wedge \varphi \wedge G\varphi\))
(WELLORD)	\(H(H\varphi \rightarrow \varphi)\rightarrow H\varphi\) (well-ordering withtransitivity)
(FIN-INT)	\((G(G\varphi\rightarrow\varphi)\rightarrow(FG\varphi\rightarrow G\varphi))\ \wedge\)\((H(H\varphi\rightarrow\varphi)\rightarrow (PH\varphi\rightarrowH\varphi))\) (finite intervals)
(IND\(_{G}\))	\(F\varphi \wedge G(\varphi \rightarrow F\varphi)\rightarrowGF\varphi\) (forward induction)
(IND\(_{H}\))	\(P\varphi \wedge H(\varphi\rightarrow P\varphi)\rightarrowHP\varphi\) (backward induction)

The principle (LIN) combines forward-linearity (LIN-F) andbackward-linearity (LIN-P) in a single condition. The resultingformula is, however, not sufficient to guarantee the connectedness ofthe temporal frame. In other words, it cannot rule out disjoint lineartime lines. Moreover, (FIN-INT) is equivalent to the conjunction of(IND\(_{H}\)) and (IND\(_{G}\)). Note that (IND\(_{H}\)) impliesforward-discreteness and that (IND\(_{G}\)) impliesbackward-discreteness, but not conversely. For instance, a time flowconsisting of a copy of the natural numbers followed by a copy of theintegers is backward-discrete, but does not satisfy (IND\(_{G}\)). Tosee this, assume that \(\varphi\) is true on the copy of the naturalnumbers but not on the copy of the integers and evaluate at theinitial point of the structure.

Recall that the last five properties mentioned above — Dedekindcompleteness, well-ordering, the finite interval property, andforward/backward induction — are not definable by first-ordersentences. However, they can be expressed by temporal formulae. On theother hand, some very simple first-order definable properties oftemporal frames, such as irreflexivity or asymmetry, are notexpressible in TL. Proofs of some of the correspondence claims listedabove can be found in Goranko (2023). For more results and details onthe expressibility of properties of temporal frames, see Segerberg(1970); Rescher and Urquhart (1971); Burgess (1979); van Benthem(1983; 1995); Goldblatt (1992); and Hodkinson and Reynolds (2007).

By extending the list of axioms of \(\mathbf{K}_{t}\) with one orseveral of the above principles one can axiomatize the logics ofvarious natural models of time; that is, there are axiomaticextensions that are sound and complete for validity on the relevantclass of temporal frames. Some of these extensions were alreadystudied in the early days of Temporal Logic. Prior (1967) discussesvarious systems resulting from different combinations of axioms. Weprovide some important ones below:

\[\begin{align}\mathbf{K4}_{t} = & \ \mathbf{K}_{t} + \text{(TRAN): all transitive frames.} \\\mathbf{S4}_{t} = & \ \mathbf{K}_{t} + \text{(REF) + (TRAN): all partial orderings.} \\\mathbf{L}_{t} = & \ \mathbf{K}_{t} + \text{(TRAN) + (LIN): all strict linear orderings.} \\\mathbf{N}_{t} = & \ \mathbf{L}_{t} + \text{(NOEND) + (IND\(_{G}\)) + (WELLORD) or} \\& \ \mathbf{L}_{t} + \text{(BEG) + (NOEND) + (FIN-INT): } \langle \mathbf{N,\lt}\rangle. \\\mathbf{Z}_{t} = & \ \mathbf{L}_{t} + \text{(NOBEG) + (NOEND) + (IND\(_{H}\)) + (IND\(_{G}\)) or} \\& \ \mathbf{L}_{t} + \text{(NOBEG) + (NOEND) + (FIN-INT): } \langle \mathbf{Z,\lt}\rangle. \\\mathbf{Q}_{t} = & \ \mathbf{L}_{t} + \text{(NOBEG) + (NOEND) + (DENSE): } \left\langle \mathbf{Q, \lt}\right\rangle. \\\mathbf{R}_{t} = & \ \mathbf{L}_{t} + \text{(NOBEG) + (NOEND) + (DENSE) + (COMPL): } \left\langle \mathbf{R, \lt}\right\rangle.\end{align}\]

As the axiomatizations of the number systems illustrate, the fact that(LIN) is not sufficient to guarantee connectedness, or thatirreflexivity is not definable in TL, does not hamper axiomatizbility(even though it requires some manipulations in the completenessproofs, see e.g. Blackburn et al. 2001, Chapter 4). Indeed,connectedness and irreflexivity do not yield any new validities.

Each of the above logics turns outdecidable (i.e., it has adecidable set of validities). This is typically shown by proving thefinite model property: “Every satisfiable formula issatisfiable in a finite model”. In most cases, such proofsinvolve non-standard models. For proofs of completeness of (variationsof) these axiomatic systems as well as proofs of decidability, seeSegerberg (1970); Rescher and Urquhart (1971); Burgess (1979); Burgessand Gurevich (1985); Goldblatt (1992); and Gabbay et al. (1994).

4. Extensions of TL over linear time

A natural class of instant-based models of time is the class of linearmodels, and soon after Prior’s invention of Tense Logic severalextensions of TL over linear time have been proposed. In this section,we discuss two such extensions: theNext Time operator andthe operatorsSince andUntil. We then introduce thelinear time temporal logic LTL, which is based on those operators andhas important applications in computer science.

4.1 Adding theNext Time operator

In forward-discrete, linear temporal models \(\mathcal{M}=\left\langle T,\prec, V \right\rangle\) without end point, where everyinstant \(t\) has a unique immediate successor \(s(t),\) it is naturalto add a new temporal operator \(X\) (“NeXt Time”or “Tomorrow”) with the following semantics:^[2]

\[ \mathcal{M},t \models X\varphi \text{ iff } \mathcal{M},s(t) \models \varphi.\]

That is, \(X\varphi\) is true at a time instant \(t\) iff \(\varphi\)is true at the immediate successor \(s(t)\) of \(t\). TheNextTime operator was already mentioned by Prior (1967, ChapterIV.3), but its importance was first fully appreciated in the contextof LTL.

The operator \(X\) satisfies the K-axiom

(K\(_{X}\))\(X(\varphi\to \psi) \to (X\varphi \to X\psi);\)

and the functionality axiom

(FUNC)\(X\lnot \varphi\leftrightarrow \lnot X\varphi.\)

It also enables a recursive fixed point definition of \(G\) and, onthe ordering of the natural numbers, the operators \(X\) and \(G\)satisfy an induction principle. Assuming the reflexive closure of theprecedence relation \(\prec\), as is common in computer science, theseproperties can be expressed as follows:

(FP\(_G\))\(G\varphi\leftrightarrow (\varphi \wedge XG\varphi);\)
(IND)\(\varphi \wedgeG(\varphi \rightarrow X\varphi )\rightarrow G\varphi.\)

In the language with \(G,H,\) and \(X\), these principles can be usedto provide sound and complete axiomatizations of the temporal logic offorward-discrete, linear orderings without end points and the naturalnumbers with successor function, respectively:

\(\mathbf{L}_{t}(X) = \mathbf{L}_{t}\) + (K\(_{X}\)) + (FUNC) +(FP\(_{G}\)): all forward-discrete, linear orderings without endpoints.
\(\mathbf{N}_{t}(X) = \mathbf{N}_{t}\) + (K\(_{X}\)) + (FUNC) +(FP\(_{G}) \) + (IND): \(\left\langle \mathbf{N},s,\leq\right\rangle,\) where \(s(n) = n+1.\)

A past analogue of \(X\), usually denoted \(Y\)(“Yesterday”), can be defined and axiomatizedlikewise. For details, see Goldblatt (1992) and Andréka et al.(1995).

4.2 AddingSince andUntil

Perhaps the most important extension of Prior’s basic tenselogic TL over linear time was the introduction of the binary temporaloperators \(S\) (“Since”) and \(U\)(“Until”) by Hans Kamp in his doctoraldissertation (Kamp 1968). The intuitive meanings of these are^[3]

\(\varphi S\psi\)“\(\varphi\)has been the case since a time when\(\psi\) was the case.”
\(\varphi U\psi\)“\(\varphi\)will be the case until a time when\(\psi\) is the case.”

For instance, the sentence “I will keep trying until Isucceed” can be formalized as: \(\mathsf{try}\,U\,\mathsf{succeed}.\) As another example, “Ever since Mia lefthome, Joe has been unhappy and has been drinking until losingconsciousness” translates as:

\[ (\mathsf{Joe\ unhappy} \land (\mathsf{Joe\ drinks}\ U\ \lnot(\mathsf{Joe\conscious})))\ S\ (\mathsf{Mia\ leaves}).\]

The formal semantics of \(S\) and \(U\) in a temporal model\(\mathcal{M} = \langle T,\prec,V\rangle\) is given by the followingtwo clauses:

\[\begin{array}{ll} \mathcal{M},t\vDash \varphi S\psi\quad \text{ iff }&\mathcal{M},s\vDash \psi \text{ for some } s \text{ such that }s\prec t \\ & \text{ and } \mathcal{M},u\vDash \varphi \text{for every } u \text{ such that } s\prec u\prec t; \\\mathcal{M},t\vDash \varphi U\psi \quad \text{ iff }&\mathcal{M},s\vDash \psi \text{ for some } s \text{ such that } t\prec s \\ & \text{ and } \mathcal{M},u\vDash \varphi\text{ for every } u \text{ such that } t\prec u\prec s.\end{array}\]

These are the ‘strict’ versions of \(S\) and \(U\),prevalent in philosophy. In computer science, usually reflexiveversions of the semantics clauses are considered.

Prior’s temporal operators \(P\) and \(F\) are definable interms of \(S\) and \(U\):

\[P\varphi :=\top S\varphi \ \text{ and } \ F\varphi :=\topU\varphi.\]

On irreflexive, forward-discrete, linear temporal orders without endpoint, \(S\) and \(U\) also allow for a definition of theNextTime operator \(X\):

\[X\varphi := \bot U \varphi.\]

This definition fails on reflexive temporal orders, which shows thatthe strict versions of \(S\) and \(U\) are more expressive than theirreflexive counterparts.^[4] Other operators can be defined in terms of \(S\) and \(U\) as well,such as for instanceBefore, given by \(\varphi B\psi :=\lnot((\lnot \varphi)U\psi)\) with intuitive reading “If \(\psi\)will be the case in the future, \(\varphi\) will occur before\(\psi\)”.

Temporal languages withSince andUntil afford greatexpressive power. Kamp (1968) proved the following remarkableresult:

Every temporal operator on a class of continuous, strict linearorderings that is definable in first-order logic is expressible interms of \(S\) and \(U\).

The result was later extended by Stavi to all linear orders, byintroducing two additional operators. However, it turns out that nofinite number of new operators can make the temporal languagefunctionally complete on allpartial orderings, as shown byGabbay. See Gabbay et al. (1994) for an overview of these results.

A complete axiomatic system for the Since-Until logic on the class ofall reflexive linear orderings was provided by Burgess (1982a) andfurther simplified by Xu (1988). Extensions of this axiomatization forstrict linear orderings were obtained by Venema (1993) and Reynolds(1994; 1996). For details and related results, see Burgess (1984);Zanardo (1991); Gabbay et al. (1994); Finger et al. (2002); andHodkinson and Reynolds (2007). The Burgess-Xu axiomatic system andsome of its extensions are presented in the supplementarydocument:

Burgess-Xu Axiomatic System forSince andUntil and Some Extensions

4.3 The linear time temporal logic LTL

The most popular and widely used temporal logic in computer science isthe linear time temporal logic LTL, which was proposed in a seminalpaper by Pnueli (1977) and was first explicitly axiomatized andstudied in Gabbay et al. (1980). In LTL, the flow of time is viewed asa discrete, linear sequence of time instants, which are taken torepresent successive states of a run of a computer system. To be moreprecise, LTL is interpreted over the reflexive closure of the orderingof the natural numbers \(\left\langle \mathbf{N},\leq\right\rangle,\)and the language involves the operators \(G,\) \(X\), and \(U\) (nopast operators).

The logic LTL is very useful for expressing properties of infinitecomputations in reactive systems, such as safety, liveness, andfairness, as laid out inSection 11.1. For example, the specification “Every time when a message issent, an acknowledgment of receipt will eventually be returned, andthe message will not be marked ‘sent’ before theacknowledgment of receipt is returned” can be formalized in LTLas:

\[ G(\mathsf{Sent} \to (\lnot \mathsf{MarkedSent} \ U\ \mathsf{AckReturned})).\]

The axiomatic system for LTL extends classical propositional logic bythe K-axiom for \(G\), the K-axiom and the functionality axioms for\(X\), as well as by axioms providing fixed point characterizations ofthe reflexive versions of \(G\) and \(U\):

(K\(_G\))\(G(\varphi\rightarrow \psi)\rightarrow (G\varphi \rightarrow G\psi)\)
(K\(_X\))\(X(\varphi\rightarrow \psi)\rightarrow (X\varphi \rightarrow X\psi)\)
(FUNC)\(X\lnot \varphi\leftrightarrow \lnot X\varphi\)
(FP\(_G\))\(G\varphi\leftrightarrow (\varphi \wedge XG\varphi)\)
(GFP\(_G\))\(\psi\land G(\psi \rightarrow (\varphi \land X\psi)) \rightarrow G\varphi\)
(FP\(_U\))\(\varphiU\psi \leftrightarrow (\psi \vee (\varphi \wedge X(\varphi U\psi)))\)
(LFP\(_U\))\(G((\psi\vee (\varphi \wedge X\theta))\rightarrow \theta)\rightarrow (\varphiU\psi \rightarrow \theta)\)

The inference rules involve onlymodus ponens and thenecessitation rule for \(G\). In technical terms, the axiom(FP\(_{G}\)) says that \(G\varphi\) is afixed point of theoperator \(\Gamma_{G}\) defined by \(\Gamma_{G} (\theta) = \varphi\land X\theta,\) whereas (GFP\(_{G}\)) says that \(G\varphi\) is (interms of its set-theoretic extension) agreatest post-fixedpoint of \(\Gamma_{G}.\) Likewise, the axiom (FP\(_{U}\)) saysthat \(\varphi U\psi\) is afixed point of the operator\(\Gamma_{U}\) defined by \(\Gamma_{U}(\theta) = \psi \lor (\varphi\land X\theta),\) whereas (LFP\(_{U}\)) says that \(\varphi U\psi\) isaleast pre-fixed point of \(\Gamma_{U}\). Some variations ofthis axiomatic system are presented in the supplementary document:

Some Variations of the Axiomatic System for LTL

Early studies of temporal logics for linear time are presented inRescher and Urquhart (1971) and McArthur (1976). Proofs ofcompleteness of variations of the axiomatic system given above can befound in Gabbay et al. (1980; 1994); Goldblatt (1992); and Finger etal. (2002). All logics mentioned in this section have the finite modelproperty (usually with respect to non-standard models) and hence aredecidable (see the references on completeness).

5. Branching time temporal logics

Much of Prior’s work on Tense Logic was motivated by the MasterArgument of Diodorus Chronus and its fatalistic conclusion. Confrontedwith the following trilemma

Every true proposition concerning the past is necessary.
The impossible does not follow from the possible.
Something that neither is nor will be is possible.

Diodorus went on to define the possible as “what is or will bethe case” (see Prior 1967, Chapter 3.1). Prior set out to showthat Diodorus’ argument was wrong.

Prior was interested in themes like indeterminism and the open future;one of his objectives here was to allow for human freedom. In order toanalyze and clarify the assumptions underlying the Master Argument, heopted for a branching representation of the interrelation of time andmodality, which was suggested to him in a letter by Kripke in 1958(see Ploug and Øhrstrøm 2012).^[5] The Diodorean conception of modality as quantification over lineartime was abandoned and replaced by the picture of a tree, whosebranches depict alternative possibilities for the future. Prior (1967,Chapter 7) considered two different versions of branching timetemporal logic, which he associated with the historical views ofPeirce and Ockham, respectively. An early formal treatment of theseideas is provided in Thomason (1970; 1984) and Burgess (1978). Manytechnical results and further developments have been proposed sincethen, and we mention some of them below, including the computationtree logics CTL and CTL*.

For Prior’s motivational views on indeterminism and humanfreedom, see Øhrstrøm and Hasle (1995, Chapters 2.6 and3.2) and Øhrstrøm (2019). A detailed discussion of thephilosophical aspects of the theory of branching time is contained ine.g. Belnap et al. (2001); Correia and Iacona (2013); the entry onfuture contingents and the entry onbranching time.

5.1 Prior’s theory of branching time

In Prior’s theory of branching time, the interrelation of timeand modality is represented as a tree that is linear towards the pastand branches into multiple possible futures. Backward-linearitycaptures the idea that the past is fixed; forward-branching reflectsthe openness of the future. At each point in time, there may be morethan one branch leading towards the future, and each such branchrepresents a future possibility.

Formally, atree (orbranching time structure) is atemporal frame \(\mathcal{T} = \left\langle T, \prec \right\rangle\)where the temporal precedence relation \(\prec\) is a backward-linearpartial order on the set of time instants \(T\) such that any twoinstants have a common \(\prec\)-predecessor in \(T\). That is, everytime instant in the tree has a linearly ordered set of\(\prec\)-predecessors, and any two instants share some common past.The former condition rules out backward-branching, while the latterensures ‘historical connectedness’. In the philosophicalliterature, the temporal precedence relation \(\prec\) is commonlyassumed to be irreflexive, i.e. a strict partial order, whereas in thecomputational tree logics, its reflexive closure is exploited, as wewill see inSection 5.5.

A tree \(\mathcal{T} = \left\langle T, \prec \right\rangle\) depictsalternative possibilities for the future in a unified structure, andit can be carved up into multiple histories. Ahistory in\(\mathcal{T}\) is a maximal (i.e. non-extendable) set of timeinstants that is linearly ordered by \(\prec\), that is, an entirepath through the tree; it represents a complete possible course ofevents. We denote the set of all histories in \(\mathcal{T}\) by\(\mathcal{H}(\mathcal{T})\), and we use \(\mathcal{H}(t)\) for theset of histories passing through a given time instant \(t\).

Some philosophers have criticized the label ‘branchingtime’ as a misnomer, arguing that time does not branch butrather evolves linearly. Early criticism along these lines is found inRescher and Urquhart (1971), and a similar point is raised in Belnapet al. (2001), who suggest the name ‘branching histories’instead. This criticism also casts doubt on the terminology‘time instants’ used here to refer to the primitive pointsof the tree. We stick to the terminology for reasons of uniformity. Inthe branching time literature, the more neutral expression‘moments’ prevails, and in Belnap et al. (2001) thedistinction between instants of time and moments is formally workedout: branching time structures are associated with a linearly orderedset of time instants, where an instant is defined as the set ofcontemporaneous moments across different histories.

5.2 The Peircean branching time temporal logic

Prior’s basic tense logic TL remains neutral about the structureof time. In a branching time setting with alternative futurepossibilities, however, the original semantics of the future operator\(F\) no longer adequately captures future truth. In such a setting,the future operator \(F\) merely reads “it will possibly be thecase that \(\dots\)”. Prior (1967, Chapter 7) thereforeconsidered two alternative semantics for the future operator, whichgive rise to the Peircean and Ockhamist branching time temporallogics, respectively.

In the Peircean branching time logic PBTL, the intuitive meaning ofthe future operator \(F\) is “it will necessarily be the casethat \(\dots\)”. That is, future truth is conceived of as truthinall possible futures. On this new reading, the futureoperator \(F\) is no longer dual to the strong future operator \(G\),which retains its original semantics but now needs to be included asan additional primitive operator into the language. Given a set ofatomic propositions \({PROP}\), the set of formulae of PBTL can berecursively defined as follows:

\[\varphi := p \in {PROP}\mid \neg \varphi\mid (\varphi \wedge \varphi) \mid P \varphi \mid F\varphi \mid G \varphi. \]

Formulae of PBTL are evaluated in a temporal model \(\mathcal{M} =\langle T,\prec,V\rangle\) on a tree \(\mathcal{T} = \langleT,\prec\rangle\), called aPeircean tree model. As usual,\(V\) is a valuation that assigns to every atomic proposition \(p \in{PROP}\) the set of time instants \(V(p) \subseteq T\) at which \(p\)is considered true. Thetruth of an arbitrary formula \(\varphi\)of PBTL at a given time instant \(t\) in a Peircean tree model\(\mathcal{M}\) is then defined inductively. The semantic clausesfor the truth-functional connectives \(\neg\) and \(\wedge\), the pastoperator \(P\), and the strong future operator \(G\) are as in TL (seeSection 3.2), and we only provide the semantic clause for the new future operator\(F\) here:

\[\begin{array}{ll} \mathcal{M},t\vDash F\varphi \quad \text{ iff }& \text{for all histories } h\in \mathcal{H}(t)\text{, there is some time } \\ & \text{instant } t'\in h \text{ such that } t\prec t' \text{ and } \mathcal{M},t'\vDash \varphi.\end{array}\]

Thus, according to the Peircean semantics, a formula of the form\(F\varphi\) is true at an instant \(t\) iff every history passingthrough \(t\) contains some later instant \(t'\) at which \(\varphi\)is true. The strong future operator \(G\) implicitly containsuniversal quantification over histories and reads “it willnecessarily always be the case that \(\dots\)”. The dual of\(G\) is the original future operator of TL, which is now denoted by\(f\), while the dual of the Peircean \(F\) is commonly written \(g\)(cf. Burgess 1980). Thus, all future operators involve (implicitly orexplicitly) quantification over histories and are modalized: theyexpress possibility and necessity regarding the future. There is noactual future and, accordingly, no notion of plain future truth. Asthis accords well with the view held by Peirce, Prior called thissystem ‘Peircean’.

In the Peircean temporal logic, the formula \(\varphi \rightarrowHF\varphi\) is no longer valid: what is the case now need not havebeen necessary in the past. This blocks the Master Argument ofDiodorus Chronus on Prior’s reconstruction, where the formulafigures as an additional premise (see Prior 1967, Chapter 3.1).Moreover, while Peirceanism preserves bivalence and the principle ofexcluded middle \(\varphi \vee \neg\varphi\), it renders all formulaeexpressing future contingents false and hence invalidates theprinciple of future excluded middle \(F\varphi \vee F\neg\varphi\).This principle is interpreted as saying that eventually either\(\varphi\) or \(\neg\varphi\) will be the case and is usually judgedintuitively valid (see e.g. Thomason 1970).

A complete finite axiomatization of the Peircean branching timetemporal logic was given by Burgess (1980), using a version of theso-called Gabbay Irreflexivity Rule. Zanardo (1990) provides analternative axiomatization, where the Gabbay Irreflexivity Rule isreplaced by an infinite list of axioms. Decidability of Peirceanismwas established in Burgess (1980), too. Burgess’ (1980)axiomatization of PBTL is provided in the supplementary document:

Burgess’ Axiomatic System for PBTL

5.3 The Ockhamist branching time temporal logic

While Prior favored Peirceanism, his alternative Ockhamist branchingtime temporal logic has become far more influential. In the Ockhamistbranching time logic OBTL, truth is not only relativized to a timeinstant in the tree but also to one of the histories passing throughthat instant, and the future operator \(F\) is evaluated along thatgiven history. Thus, the intuitive meaning of \(F\) becomes“With respect to the given history, it will be the casethat \(\dots\)”. In addition to the temporal operators \(F\) and\(P\), the language of OBTL contains a modal operator \(\Diamond\) andits dual \(\Box\), which are interpreted as quantifiers overhistories. Given a set of atomic propositions \({PROP}\), the set offormulae of OBTL can be recursively defined by

\[\varphi := p \in {PROP}\mid \neg \varphi\mid (\varphi \wedge \varphi) \mid P\varphi \mid F\varphi \mid \Diamond\varphi. \]

In the Ockhamist semantics, these formulae will be evaluated in amodel on a tree \(\mathcal{T} = \langle T,\prec\rangle\) at pairs\((t,h)\) consisting of a time instant \(t\in T\) and a history \(h\in \mathcal{H}(t)\) containing that instant. Naturally, the questionarises how to evaluate the atomic propositions in the model: do theirtruth values depend only on the given time instant, or do they dependon the history parameter as well? The answer to this questioncrucially hinges on whether atomic propositions may contain‘traces of futurity’ or not (Prior 1967, 124). There is noconsensus on the treatment of atomic propositions in the literature(cf. Zanardo 1996), and Prior himself entertained the idea of atwo-sorted language with two different kinds of atomic propositionsthat each require a different treatment (Prior 1967, Chapter 7.4).Here we will allow the truth values of atomic propositions to dependon both the time instant and the history. The more specific case ofinstant-based propositions can be obtained by imposing the additionalrequirement that the scheme \(p \leftrightarrow \Box p\) be valid for\(p \in {PROP}\).

Thus, anOckhamist tree model is a triple \(\mathcal{M} =\left\langle T, \prec, V \right\rangle\) where \(\mathcal{T} = \langleT,\prec\rangle\) is a tree and \(V\) is a valuation that assigns toevery atomic proposition \(p\in {PROP}\) the set of admissibleinstant-history pairs \(V(p) \subseteq T \times\mathcal{H}(\mathcal{T})\) at which \(p\) is considered true. Thetruth of an arbitrary formula \(\varphi\) of OBTL at a giveninstant-history pair \((t,h)\) in an Ockhamist tree model\(\mathcal{M}\) is defined inductively as follows:

\(\mathcal{M},(t,h)\vDash p\) iff \((t,h)\in V(p)\),for \(p\in {PROP}\);
\(\mathcal{M},(t,h) \vDash \neg\varphi\) iff \(\mathcal{M},(t,h) \not\vDash \varphi\);
\(\mathcal{M},(t,h) \vDash \varphi \wedge \psi\) iff \(\mathcal{M},(t,h) \models \varphi\) and \(\mathcal{M},(t,h) \vDash\psi\);
\(\mathcal{M},(t,h)\vDash P\varphi\) iff \(\mathcal{M},(t',h) \vDash \varphi\) for some time instant \(t'\inh\) such that \(t' \prec t\);
\(\mathcal{M},(t,h)\vDash F\phi\) iff \(\mathcal{M},(t',h)\models \phi\) for some time instant \(t'\in h\)such that \(t \prec t'\);
\(\mathcal{M},(t,h)\vDash \Diamond \varphi\) iff \(\mathcal{M},(t,h')\vDash \varphi\) for some history \(h'\in\mathcal{H}(t)\).

The temporal operators are essentially interpreted as they are inlinear temporal logic: the instant of evaluation is simply shiftedbackwards and forwards on the given history. Note that the requirement“\(t'\in h\)” is redundant in the semantic clause for thepast operator \(P\) as there is no backward branching. It is crucial,however, in the clause for the future operator \(F\). As usual, thestrong temporal operators \(H\) and \(G\) are defined as the duals of\(P\) and \(F\), respectively. The modal operators quantify over theset of histories passing through the current instant. The operator\(\Diamond\) is an existential quantifier over that set and capturespossibility, while its dual \(\Box\) involves universal quantificationand expresses ‘inevitability’ or ‘historicalnecessity’.

We say that a formula of OBTL isOckhamist valid iff it istrue at all admissible instant-history pairs in all Ockhamist treemodels. Obviously, all temporal formulae that are valid in linearmodels of time are Ockhamist valid as well. Hence, Ockhamism validatesthe principle of future excluded middle \(F\varphi \vee F\neg\varphi\) (under the assumption that time does not end) as well asthe formula \(\varphi \rightarrow HF\varphi\). It invalidates,however, the principle of the necessity of the past \(P\varphi\rightarrow \Box P\varphi\), and thus, like Peirceanism, blocksDiodorus’ Master Argument, albeit for a different reason.

Whereas in the Peircean branching time logic PBTL future truth ismodalized, in the Ockhamist branching time logic OBTL future truth andmodality come apart. The Peircean formulae \(F\varphi\) and\(G\varphi\) are equivalent to the Ockhamist \(\Box F\varphi\) and\(\Box G\varphi\), respectively. In fact, PBTL can be regarded as aproper fragment of OBTL, namely the fragment that comprises all andonly those formulae that are recursively built up from (instant-based)atomic propositions using truth-functional connectives and thecombined modalities \(\Box F\) and \(\Box G\) (with their duals\(\Diamond G\) and \(\Diamond F\)). In fact, the Peircean language isstrictly less expressive than the Ockhamist one, lacking e.g. anequivalent for \(\Diamond GF\varphi\) (for a proof, see Reynolds2002).

By relativizing truth at an instant to a history in the tree, theOckhamist branching time logic provides a notion of plain futuretruth. From a philosophical point of view, however, the relativizationto a history is not entirely unproblematic. There are essentially twodifferent ways to interpret the Ockhamist history parameter. First,one may think of it as referring to the actual course of events in thetree of possibilities, and since this idea meshes well withOckham’s view on the future, Prior chose the label‘Ockhamism’. This idea of an actual history has triggereda variety of so-called ‘Thin Red Line’ theories (for adiscussion, see Belnap and Green 1994; Belnap et al. 2001; andØhrstrøm 2009). Second, one may think of the history asan auxiliary parameter of truth that cannot be initialized in acontext: the context of utterance uniquely determines the time instantof the utterance, but it cannot single out one of the historiespassing through that instant if the future is genuinely open. Thisline of thought has given rise to ‘post-semantic’accounts, which aim to bridge the gap between the recursive semanticmachinery and a context by introducing a notion ofsuper-truth, most notably Thomason’s supervaluationism(Thomason 1970) and MacFarlane’s assessment-sensitivepost-semantics (MacFarlane 2003; 2014). These accounts sacrificebivalence, but they preserve the principles of excluded middle\(\varphi \vee \neg\varphi\) and future excluded middle \(F\varphi\vee F\neg\varphi\).

From a logical point of view, the Ockhamist approach to branching timestrongly resembles the idea underlying the notion of a\(T\timesW\) frame and the more general notion of aKamp frame,discussed in Thomason (1984), as well as the definition of anOckhamist frame introduced in Zanardo (1996). These kinds offrames build on a non-empty set of possible worlds, each of which isendowed with an internal linear temporal structural, and assume atime-relative, historical accessibility relation between possibleworlds. That is, overlap of histories is replaced by accessibility,and possible worlds are considered primitive elements, whereas inbranching time histories are defined in terms of instants. As aconsequence, if we merge a frame consisting of historically relatedpossible worlds into a tree, new histories may emerge that do notcorrespond to any of the possible worlds (for the construction, seee.g. Reynolds 2002).

Technically, the difference between a possible worlds based approachand a branching time based approach can be overcome by equippingbranching time structures with a primitive set of histories that isrich enough to cover the entire structure, a so-calledbundle. Abundled tree is defined as a triple\(\langle T,\prec,\mathcal{B}\rangle\) where \(\mathcal{T} = \langleT,\prec\rangle\) is a tree and the bundle \(\mathcal{B} \subseteq\mathcal{H}(\mathcal{T})\) is a non-empty set of histories such thatevery instant in \(\mathcal{T}\) belongs to some history in\(\mathcal{B}\) (Burgess 1978; 1980). The Ockhamist semanticsstraightforwardly generalizes to bundled trees, with the onlydifference being that quantification over histories is now restrictedto histories from the bundle. Bundled tree validity is equivalent toKamp validity (Zanardo 1996; Reynolds 2002), but weaker than fullOckhamist validity. Reynolds (2002) provides the following example ofa formula that is Ockhamist valid but falsifiable in bundled trees(assuming instant-based atomic propositions); further counterexampleswere provided in e.g. Burgess 1978 and Nishimura 1979: \[\Box G(p \to \Diamond F p) \to \Diamond G(p \to F p).\]Intuitively, the antecedent of this formula allows one to construct a‘limit history’ in which \(p\) always holds. Such limithistories may be omitted in bundled trees, which gave rise tophilosophical discussions concerning the adequacy of those frames (seee.g. Nishimura 1979; Thomason 1984; and Belnap et al. 2001).

A complete axiomatization for bundled tree validity is given inZanardo (1985) and Reynolds (2002; 2003). Finding a completeaxiomatization for Ockhamist validity turned out to be more difficult.It has been shown that the class of Ockhamist trees is not definablein the class of bundled trees (Zanardo et al. 1999). In Reynolds(2003), an axiomatization for Ockhamist validity is proposed and acompleteness proof sketched. In this system, the problem of emergenthistories is dealt with by an infinite axiom scheme based on theformula given above. The full proof, however, has never appeared inprint, and so the problem appears to be still open. Moreover, bundledtree validity is known to be decidable (see Burgess 1979). The sameholds for Ockhamist validity, under the assumption of instant-basedatomic propositions (see Gurevich and Shelah 1985a; 1985b; andReynolds 2002). We are not aware of results establishing decidabilityor undecidability of Ockhamist validity with history-dependent atomicpropositions. Reynolds’ (2003) axiomatization for bundled treevalidity and his proposed extension to Ockhamist validity is providedin the supplementary document:

Reynolds’ Axiomatic System for OBTL

Recently, generalizations of the Ockhamist branching time logic havebeen proposed, replacing the Ockhamist history parameter by asetof histories. In Zanardo (1998), trees \(\mathcal{T} = \langleT,\prec\rangle\) are equipped with an indistinguishability functionthat assigns to each time instant a partition of the set of historiespassing through that instant, and truth at an instant is relativizedto one such indistinguishability cell, i.e. to a set of histories. Fordetails, see Zanardo (1998) and Ciuni and Zanardo (2010). An accountthat is similar in spirit is thetransition semanticspresented in Rumberg (2016). In that framework, possible courses ofevents are construed as chains of local future possibilities, viz.transitions, and can be extended towards the future. Transitionsemantics introduces a second local perspective in time, which —unlike Zanardo’s (1998) indistinguishability cells — canbe shifted independently of the time instant and which — unlikeMacFarlane’s (2003; 2014) postsemantic moment of assessment— is incorporated in the semantics proper. The language containsa so-called stability operator that allows one to capture how thetruth value of a formula about the future at an instant changes in thecourse of time. For details, see Rumberg (2016; 2019) and Rumberg andZanardo (2019). Both the branching time logic withindistinguishability functions and the transition approach subsumePeirceanism and Ockhamism as limiting cases, namely the cases wherethe set of histories taken into account in the semantic evaluation isa singleton, resp. the set of all histories passing through the giveninstant. A brief overview of the transition based approach ispresented in the supplementary document:

Transition Semantics

5.4 The computation tree logics CTL and CTL*

Branching time logics are extensively used in computer science. Themost popular ones are the computation tree logics CTL and CTL*, whichare variants of the Peircean and the Ockhamist branching time temporallogics, respectively. They are interpreted on the class of so-calledcomputation trees, where every history has the order type ofthe natural numbers. These trees are naturally obtained as treeunfoldings of discrete transition systems and represent the possibleinfinite computations arising in such systems. As usual in computerscience, they are based on the reflexive closure of the precedencerelation \(\prec\). While CTL historically preceded CTL*, nowadays CTLis often viewed as a fragment of CTL*, and we follow this conventionhere.

Thefull computation tree logic CTL* is the computationalvariant of Ockhamism, and it was introduced by Emerson and Halpern(1985). The language of CTL* contains (the reflexive versions of) thefuture operators \(G\) and \(U\) (Until) as well as theNext Time operator \(X\) (no past operators), which are nowinterpreted on computation trees. As in the general Ockhamistbranching time logic, the evaluation is relativized to both an instant(here called astate) and a history (here called acomputation path, or just apath). We note that incomputer science usually instant-based atomic propositions areassumed, i.e., the evaluation of the atomic propositions depends onlyon the state.

Thecomputation tree logic CTL is the computational variantof Peirceanism, and it was introduced by Emerson and Clarke (1982).CTL is the fragment of CTL* where each of the temporal operators\(G\), \(U\), and \(X\) is immediately preceded by a modal operator,\(\Box\) or \(\Diamond\), here usually denoted by the path quantifiers\(\forall\) and \(\exists\). That is, the language of CTL isrecursively built up using the combined modalities \(\forallG\varphi\), \(\forall(\varphi U\psi)\), \(\forall X\varphi,\) and\(\exists G\varphi\), \(\exists(\varphi U\psi)\), \(\existsX\varphi\). A precursor of CTL is the logic UB, introduced by Ben-Ariet al. (1983), in which \(U\) does not occur.

The logic CTL became widely used owing to its good computationalproperties with regard tomodel checking, having linearcomplexity both in the size of the input formula and in the size ofthe input model (as finite transition system). However, CTL is notalways sufficiently expressive, which led to its extension CTL*. Thelogic CTL* is much more expressive and subsumes the linear timetemporal logic LTL, but it has higher complexities of model checking(PSPACE) and of deciding satisfiability (2EXPTIME). For furtherdetails and proofs of decidability, see Emerson and Sistla (1984);Emerson and Halpern (1985); Emerson (1990); Goldblatt (1992); Stirling(1992); Gabbay et al. (1994); Finger et al. (2002); and Demri et al.(2016).

A complete axiomatization of CTL can be obtained by replacing theaxioms of LTL by their path-quantified versions. For proofs ofcompleteness, see Emerson (1990) and Goldblatt (1992). For CTL* moreaxioms must be added to account for the interaction of temporal andmodal operators and to enforce the limit closure property of trees. Acomplete axiomatization for CTL* was obtained by Reynolds (2001), anda completeness result for the extension of CTL* with past operatorswas established in Reynolds (2005). For more on CTL and CTL*, seeDemri et al. (2016). A sketch of the axiomatic system for CTL isincluded in the supplementary document:

An Axiomatic System for CTL

6. Interval temporal logics

Instant-based and interval-based models of time introduce twodifferent temporal ontologies, and even though they are technicallyreducible to each other, this does not solve the semantic issue:should propositions about time be interpreted as referring to timeinstants or to intervals?

There have been various explorations of interval-based temporal logicsin the philosophical logic literature. Important early contributionsinclude Hamblin (1972); Humberstone (1979); Röper (1980); andBurgess (1982b). The latter provides an axiomatization for aninterval-based temporal logic with a precedence relation betweenintervals on the rationals and the reals. The interval-based approachto temporal reasoning has been very prominent in ArtificialIntelligence. Some notable works here include Allen’s (1984)logic of planning, Kowalski and Sergot’s (1986) calculus ofevents, and Halpern and Shoham’s (1986) modal interval logic. Italso features in some applications in computer science, such asreal-time logics andhardware verification, notablyMoszkowski’s (1983) interval logic and Zhou, Hoare, andRavn’s duration calculus (see Hansen and Zhou 1997).

Here we briefly present the propositional modal-logic style approachproposed by Halpern and Shoham (1986), hereafter called\(\mathsf{HS}.\) The language of \(\mathsf{HS}\) includes a family ofunary interval operators of the form \(\langle X\rangle,\) one foreach of Allen’s interval relations over linear time. Therespective notations are listed inTable 1 (Section 2.2). Given a set of atomic propositions \(PROP\), formulaeare recursively defined by the following grammar: \[\varphi := p \in {PROP} \mid \neg \varphi \mid (\varphi \wedge \varphi) \mid \langle X\rangle\varphi.\]

The interval logic \(\mathsf{HS}\) starts from instant-based modelsover linear time, and intervals are considered defined elements. Let\(\mathcal{T} = \langle T,\prec\rangle\) be a temporal frame with aprecedence relation \(\prec\) that induces a strict linear order onthe set of time instants \(T\). Aninterval in\(\mathcal{T}\) is defined as an ordered pair \([a,b]\) such that\(a,b\in T\) and \(a\leq b.\) The set of all intervals in\(\mathcal{T}\) is denoted by \(\mathbb{I}(\mathcal{T)}.\) Note thatthe definition allows for ‘point intervals’ whosebeginning and end points coincide, following the original proposal byHalpern and Shoham (1986). Sometimes only ‘strict’intervals are considered.

Crucially, in interval-based temporal logic, formulae are evaluatedrelative to time intervals rather than instants. Anintervalmodel is a triple \(\mathcal{M} = \langle T,\prec,V\rangle\)consisting of a strict linear temporal frame \(\mathcal{T} = \langleT,\prec\rangle\) and a valuation \(V\) that assigns to each atomicproposition \(p\in{PROP}\) the set of time intervals \(V(p) \subseteq\mathbb{I}(\mathcal{T})\) at which \(p\) is considered true. Thetruth of an arbitrary formula \(\varphi\) at a given interval\([a,b]\) in an interval model \(\mathcal{M}\) is defined bystructural induction on formulae as follows:

\(\mathcal{M},[a,b] \models p\) iff \([a,b]\inV(p)\), for \(p \in {PROP};\)
\(\mathcal{M},[a,b] \models \neg\varphi\) iff \(\mathcal{M},[a,b] \not\models \varphi;\)
\(\mathcal{M},[a,b] \models \varphi \wedge \psi\) iff \(\mathcal{M},[a,b] \models \varphi\) and \(\mathcal{M},[a,b]\models \psi;\)
\(\mathcal{M},[a,b] \models \langle X\rangle\varphi\) iff \(\mathcal{M},[c,d] \models \varphi\) for some interval\([c,d]\) such that \([a,b]R_{X}[c,d]\), where \(R_X\) isAllen’s interval relation corresponding to the modal operator\(\langle X\rangle\) (cf.Table 1).

That is, the new interval operators are given a Kripke-style semanticsover the associated Allen relations. E.g., for the Allen relation“meets”, we have:

\[\mathcal{M},[t_{0},t_{1}] \models \langle A\rangle \varphi \text{ iff } \mathcal{M},[t_{1},t_{2}] \models \varphi \text{ for some interval } [t_{1},t_{2}].\]

For each diamond modality \(\langle X\rangle,\) the corresponding boxmodality is defined as its dual: \([X] \varphi \equiv \neg \langleX\rangle \neg \varphi.\) Sometimes it is useful to include anadditional modal constant for point intervals, denoted \(\pi,\) withthe following truth definition:

\[ \mathcal{M},[a,b]\models\pi \ \text{ iff } \ a=b.\]

Some of the \(\mathsf{HS}\) modalities are definable in terms ofothers, and both for the semantics with and without point intervals,minimal fragments have been identified that are expressive enough todefine all other operators. Complete sets of equivalences that capturethe interdefinability of some \(\mathsf{HS}\) modalities are presentedin the supplementary document:

Interdefinability of \(\mathsf{HS}\) Modalities

The logic \(\mathsf{HS}\) has over a thousand expressivelynon-equivalent fragments involving only some of the modal operators(see Della Monica et al. 2011 for a survey). Most of its fragments arevery expressive, and the respective notions of validity are usuallyundecidable (under some additional assumptions even highlyundecidable, viz. \(\Pi^{1}_{1}\)-complete). However, some non-trivialdecidable fragments of HS have been identified. The probably beststudied one is theneighborhood interval logic, whichinvolves the operators \(\langle A \rangle\) and\(\langle\overline{A}\rangle\) (Goranko et al. 2003). An example of anaxiom for \(\langle A\rangle\) is \(\langle A \rangle\langle A\rangle\langle A \rangle p \to \langle A \rangle\langle A \rangle p,\)saying that any two consecutive right-neighboring intervals can bejoined into one right-neighboring interval.

In addition to the unary \(\mathsf{HS}\) interval modalitiesassociated with Allen’s binary interval relations, someoperators of higher arity naturally arise. For instance, there is theoperation of chopping an interval into two subintervals, which givesrise to the ternary interval relation ‘chop’, proposed andstudied in Moszkowski (1983) and extended in Venema (1991) to thelogic CDT, which involves next to ‘chop’ (\(C\)), the tworesidual ‘chop’ operators \(D\) and \(T.\) The logic CDTwas completely axiomatized in Venema (1991); see also Goranko et al.(2004) and Konur (2013).

There is a natural spatial interpretation of interval temporal logics,based on the idea that the pairs that define an interval on a linearorder \(L\) can be considered coordinates of a point in the \(L \timesL\)-plane. Relations between intervals are then interpreted as spatialrelations between the relevant points. This interpretation has beenfruitfully used to transfer various technical results between intervaland spatial logics, such as undecidability, see e.g. Venema (1990) andMarx and Reynolds (1999).

Lastly, a few words about the relationship between interval temporallogics and first-order logic. The standard translation ofPrior’s basic tense logic TL into first-order logic (presentedinSection 3.3) extends naturally to interval logics, where atomic propositions arerepresented in the first-order language by binary relations. It turnsout that some fragments of \(\mathsf{HS}\) can be translated into thetwo-variable fragment FO\(^{2}\) of first-order logic, whicheventually implies their decidability. The expressively strongest suchinterval logic is the neighborhood interval logic, proven to beexpressively complete for FO\(^{2}\) (Bresolin et al. 2009). Otherfragments of \(\mathsf{HS}\) require at least three distinct variablesfor the standard translation. But even the full logic \(\mathsf{HS}\)is less expressive than the three-variable fragment FO\(^{3}\) offirst-order logic, for which Venema (1991) showed that the logic CDTis expressively complete.

For more on interval temporal logics, see Halpern and Shoham (1986);Venema (1990); Goranko et al. (2003; 2004); Della Monica et al.(2011); the survey Konur (2013), and the references therein.

7. Other variants of propositional temporal logics

So far we have discussed the traditional family of propositionaltemporal logics, but there are numerous variations and alternativedevelopments that provide useful formalisms for various applications.We briefly present some of them here: hybrid temporal logics, metricand real-time temporal logics, and quantified propositionallogics.

7.1 Hybrid temporal logics

A notable family of temporal logics, enriching the traditionalframework, arehybrid temporal logics, which combinepropositional temporal logic with elements of first-order logic andthereby considerably increase the expressive power of thelanguage.

The most important notion in hybrid temporal logics is that of anominal. Nominals are special atomic symbols: they areconsidered to be true at exactly one instant of the temporal model.Hence, one can think of a nominal \(a\) as saying “It is \(a\)o’clock now”. For this reason, nominals are sometimes alsocalled ‘clock variables’. The idea of nominals can betraced back to Prior (1967, Chapter V; 1968, Chapter XI), whoconsidered the possibility of identifying instants withinstant-propositions: an instant can be conceived of as theconjunction of all those propositions that are true at that instant.The first mathematical exploration of hybrid temporal logic was givenin Bull (1970). In addition to nominals, hybrid languages are oftenaugmented by further syntactic mechanisms, such as satisfactionoperators, quantifiers over nominals, and reference pointers, which webriefly discuss below. Satisfaction operators and quantifiers overnominals can already be found in Prior’s work (see Blackburn2006) and were reinvented independently in Passy and Tinchev (1985).Reference pointers were introduced only much later in Goranko (1996),and a similar referencing mechanism is found in Alur and Henzinger(1994).

Satisfaction operators: The satisfaction operator\(@_{i}\) allows one to express that a given formula is true at thetime instant denoted by the nominal \(i\). That is,\(\mathcal{M},t\vDash @_{i}\varphi\) iff \(\mathcal{M},V(i)\vDash\varphi,\) where \( V(i)\) is the unique instant where \(i\) is true.The notion of truth at an instant of a temporal model is imported intothe object-language.
Quantifiers over nominals: The nominal quantifier\(\forall i\) expresses that a formula is true at the given timeinstant no matter which instant the nominal \(i\) denotes. Moreformally, \(\mathcal{M},t\vDash \forall i\varphi\) iff\(\mathcal{M}_{[i\rightarrow s]},t\vDash \varphi\) for any instant\(s\) in \(\mathcal{M},\) where \(\mathcal{M}_{[i\rightarrow s]}\) isthe model obtained from \(\mathcal{M}\) by re-assigning the denotationof \(i\) to be \(s.\) The full power of first-order quantification isbrought into the temporal language, while many of its propositionalvirtues are preserved.
Reference pointers: Reference pointers \(\downarrow_{i}\)(also known as ‘binders’) provide a mechanism forreferring to the current time instant, i.e. saying ‘now’.A formula \(\downarrow_{i}\varphi\) is true at a given instant \(t\)iff \(\varphi\) is true at \(t\) when all occurrences of the nominal\(i\) in \(\varphi\) denote \(t\). That is, \(\mathcal{M},t\vDash\downarrow_{i}\varphi\) iff \(\mathcal{M}_{[i\rightarrow t]},t\vDash\varphi\).

Other operators that can be considered hybrid temporal logic operatorsare theuniversal modality, thedifference modality,andpropositional quantifiers. The universal modality \(A\)says that a given formula is true at every instant of the temporalmodel and hence captures the notion of validity in a model:\(\mathcal{M},t\vDash A\varphi\) iff \(\mathcal{M}\vDash\varphi\). Thedifference modality \(D\), on the other hand, states that the givenformula is true at some other instant. Note that both modalitiesabstract away from the underlying accessibility relation.Propositional quantifiers \(\forall p\) introduce second-orderquantification into the propositional language, and we discuss them inSection 7.3 below.

Hybrid languages are very expressive. Here are just two examples:

Irreflexivity of the precedence relation, which is not expressiblein TL, can be expressed in a language with nominals by \(i \rightarrow\neg Fi\) or with the help of the satisfaction operator by \(@_{i}\negFi.\)
The operators \(S\) and \(U\) are definable in a language withnominals and reference pointers: \(\varphi U\psi :={\downarrow_{i}}F(\psi \wedge H(Pi\rightarrow \varphi))\), and likewise for\(S.\)

While the weaker versions of hybrid logics — with nominals,satisfaction operators, universal modality, and difference modality— are still decidable, the more expressive ones — withquantifiers over nominals or reference pointers — are usuallyundecidable. For details, see Goranko (1996); and Areces and ten Cate(2007).

Branching time versions of hybrid temporal logics have beeninvestigated as well. For an overview of varieties of hybrid temporallogics and their historical development, see Blackburn (1993); Gargovand Goranko (1993); Blackburn and Seligman (1995), Blackburn andTzakova (1999) and the entry onhybrid logic.

7.2 Metric and real-time temporal logics

Metric temporal logics go back to Prior, too (see Prior 1967, ChapterVI). He used the notation \(Pn\varphi\) for “It was the case theinterval \(n\) ago that \(\varphi\)” (i.e. \(\varphi\) was thecase \(n\) time units ago) and \(Fn\varphi\) for “It will be thecase the interval \(n\) hence that \(\varphi\)” (i.e \(\varphi\)will be the case \(n\) time units hence). These operators presupposethat time has a certain metric structure and can be carved up intotemporal units, which may be associated with clock times (e.g. hours,days, years, etc.). If the relevant units are days, for example, theoperator \(F 1\) reads ‘the following day’ (or just‘tomorrow’).

Prior noted that \(P n\varphi\) can be defined as \(F(-n)\varphi.\)The case \(n=0\) accordingly amounts to the present tense. The metricoperators validate combination principles such as:

\[FnFm\varphi \rightarrow F(n+m)\varphi.\]

The interrelation of the metric and non-metric versions of thetemporal operators is captured by the following equivalences:

\[\begin{matrix}P\varphi \equiv \exists {n}({n} \lt 0 \land Fn\varphi) & F\varphi \equiv \exists n(n \gt 0 \land Fn\varphi) \\H\varphi \equiv \forall {n}({n} \lt 0 \rightarrow Fn\varphi) & G\varphi \equiv \forall n(n \gt 0 \rightarrow Fn\varphi).\end{matrix}\]

Instant-based temporal logics for metric time are studied in e.g.Rescher and Urquhart (1971, Chapter X); Montanari (1996); andMontanari and Policriti (1996). For metric interval logics, seeBresolin et al. (2013).

Various metric extensions of temporal logics over the structure of thereal numbers have been proposed, giving rise to so-calledreal-time logics. These logics introduce additionaloperators, such as the following, which enable differentformalizations of the sentence “whenever \(p\) holds in thefuture, \(q\) will hold within three time units later”:

time-bounded operators, e.g.: \(G(p \to F_{_{\leq 3}} q);\)
freeze quantifiers (similar to hybrid logic reference pointers),e.g.: \(Gx. (p \to Fy. (q \land y\leq x+3));\)
quantifiers over time variables, e.g.: \(\forall x G(p \land t=x\to F(q \land t\leq x+3)).\)

Such real-time extensions are usually very expressive and often leadto logics with undecidable decision problems. A way to regaindecidability is to relax “punctuality” requirementsinvolving precise time durations by requirements involving timeintervals. For details, see e.g. Koymans (1990); Alur and Henzinger(1992; 1993; 1994) as well as Reynolds (2010; 2014) on the real-timelinear temporal logic RTL, and the survey Konur (2013).

7.3 Quantified propositional temporal logics

Propositional temporal logics can be extended with quantifiers overatomic propositions. For example, the formula \(F\forall p(p\rightarrow Fp)\) can be used to express that there is a future timesuch that everything that is the case then will again be the case inthe future (see Rescher and Urquhart 1971, Chapter XIX).Set-theoretically, such quantifiers range over all valuations of therespective atomic propositions and hence are tantamount to monadicsecond-order quantifiers. The resulting languages are very expressive,and the respective logics are usually undecidable (often not evenrecursively axiomatizable). Notable extensions include the logic QPTL,the quantified propositional version of LTL (which is decidable albeitwith non-elementary complexity), as well as the extension of CTL* (seeFrench 2001). Complete axiomatic systems and decidability results forthe quantified propositional temporal logic QPTL (with and withoutpast operators) have been presented in Kesten and Pnueli (2002) andFrench and Reynolds (2003). See also Fritz (2024) for a systematicstudy of modal logics with propositional quantification.

8. First-order temporal logics

Objects exist in time, and they change their properties over time.Propositional temporal logics are not expressive enough to capturethis aspect of the world: all that is associated with a time instantis a set of unstructured atomic propositions that are considered truethere. What is needed is a more fine-grained model of the temporalhistory of the world, with objects that may have certain propertiesand stand in certain relations. Accordingly, in addition to temporaloperators, the language should contain names for objects, variablesand quantifiers ranging over objects, as well as predicates fordenoting properties and relations. This is what first-order temporallogics provide.

8.1 Existence and quantification in time

Existence in time is an important topic in the philosophy of time.Usually, objects come into being at one point in time and go out ofbeing at some later time. But what is it for an object to exist intime? Do only present objects exist, as apresentist wouldhold, or is existence to be understood in a broader sense comprisingpast and future objects as well, as aneternalist would say?The controversy betweenpresentism andeternalism isaccompanied by a debate onpersistence, that is, on thequestion how objects exist through time. Are objects wholly present ateach instant at which they exist — a view known asendurantism — or do they persist by having differenttemporal stages at different instants in time — a view calledperdurantism? For a detailed overview of these debates, seee.g. Dyke and Bardon (2013); Meyer (2013); Correia and Rosenkranz(2018), as well as the entries ontime,temporal parts, andidentity over time.

Similar questions arise in the context of first-order temporal logics,albeit under a different guise. Issues concerning existence in andidentity over time reveal themselves in the interaction of temporaloperators and individual quantifiers. For example, the sentence“A philosopher will be a king” can be interpreted inseveral different ways:^[6]

\(\exists {x}(philosopher({x})\land {F} \, king({x}))\)
Someone who is now a philosopher will be a king at some futuretime.
\(\exists {x}{F} (philosopher({x})\land king({x}))\)
There now exists someone who will at some future time be both aphilosopher and a king.
\({F} \exists {x}(philosopher({x})\land {F}\, king({x}))\)
There will exist someone who is a philosopher and later will be aking.
\({F} \exists {x}(philosopher({x})\land king({x}))\)
There will exist someone who is at the same time both aphilosopher and a king.

All of the above readings presuppose that the domain of quantificationis relative to a time instant and that the same individual may existat multiple times. To accommodate this idea, we need to equip ourmodels with alocal domain of objects \({D}({t})\) at eachtime instant \(t\), restrict the range of the individual quantifiersto that domain, and incorporate a mechanism that enables us toidentify an object across different times.

Moreover, the example suggests that the local domain at a given timeinstant contains exactly those individuals that do in fact exist atthat instant. However, there are alternative ways of understanding thelocal domains associated with time instants, which mirror differentconceptions of existence in time. Here are four natural options:

The first view corresponds to the view sketched above: objects comeinto being at one point in time and go out of being at a later time,i.e., they exist only over a certain period of time. This idea can becaptured formally by assuming that the local domains are constitutedsolely by the present objects. The local domains accordingly vary overtime.
Objects actually exist only over a period of time, but they remain inthe temporal history of the world once they have ceased to exist. Onthis account, the local domains include not only the present objectsbut all past objects as well; they increase as time progresses and newobjects come into being.
Alternatively, one may hold that all objects that will ever exist areinitially part of the temporal history of the world but drop out oncethey have ceased to exist. That is, the local domains comprise allpresent and future objects; they decrease as time progresses andobjects go out of being.
Past, present, and future objects likewise exist. This is the notionof existence in an eternalist sense. One way to formally capture thisidea is by stipulating that the local domains contain all objects thatare part of the temporal history of the world. Hence, they areconstant over time.

A conceptually different but technically closely related issueconcerns the range of quantification. What do we quantify over in atemporal setting?

Only over those objects that exist at the current time instant, aspresupposed in the above example?
Over all present, past, and future objects in the temporal history ofthe world?

Adopting the terminology ‘actualist quantification’ and‘possibilist quantification’ by Fitting and Mendelsohn(2023) to the temporal case, we may refer to the first kind ofquantification aspresentist quantification and use the termeternalist quantification for the latter. Depending on thechoice between these options, the sentence “Every human is bornafter 1888” comes out true or false. It is true if we quantifyover only those humans that are currently alive, but it is false if wequantify over all humans in the temporal history of the world,including those that have ever lived. A further issue concernsfictitious entities, such as Santa Claus or Pippi Longstocking, whichdo not really exist at any time instant. Still, they may be said toexist in a broader sense, and one may want to include them in thedomain of quantification. We set this issue aside here and refer thereader to the entry onfree logic, which is a logic that allows reference to non-existing entities (cf.alsoSection 8.6).

Many of the questions concerning the interrelation of existence andquantification arising here correspond to well known problems in modalfirst-order logics, where an extensive discussion on these issuesstarted already with Frege and Russell and peaked in the 1940s-1950sin the works of R. Barcan-Marcus, R. Carnap, W. Quine, R. Montague,and others (see the entry onmodal logic). A central theme in first-order modal logics is the validity orinvalidity of the so-called Barcan formula. In a temporal setting, aversion of the formula (referring to the future) can be glossed asfollows: “If at some time in the future there will be somethingthat is \(Q\), then there is something now that will be \(Q\) at sometime in the future.” Whether this statement is guaranteed to betrue crucially depends on how the local domains at the variousinstants in time are construed and what our quantifiers range over.Furthermore, temporal logic yields two versions of the Barcan formula,one for the future and one for the past.

8.2 The language and models of FOTL

A basic language of first-order temporal logic (FOTL) is an extensionof a given first-order language by the operators \(P\) and \(F\).Whereas in propositional temporal logics atomic propositions areconsidered unstructured entities, in first-order temporal logicsatomic formulae are built up from terms denoting individuals andpredicate symbols denoting properties and relations. In addition, thelanguage usually contains quantifiers ranging over individuals. (Abrief overview of plain first-order logic is provided in thesupplementary documentFirst-order Relational Structures and Languages.) In what follows, we consider FOTL over a relational first-orderlanguage (no function symbols) with individual quantifiers andequality. The set of formulae is defined as follows:

where \(R(\tau_1,\dots,\tau_n)\) and \(\tau_1 = \tau_2\) are atomicformulae. The truth functional connectives \(\vee, \rightarrow\), and\(\leftrightarrow\), the logical constants \(\top\) and \(\bot\), aswell as the temporal operators \(H\) and \(G\) can be defined asusual. Moreover, the dual \(\exists\) of \(\forall\) is defined by\(\exists x \varphi := \neg \forall x \neg \varphi\).

The models of FOTL are based on temporal frames, where each timeinstant is associated with a first-order relational structure.Formally, afirst-order temporal model is a quintuple\(\mathcal{M}= \langle T, \prec,\mathcal{U},D,\mathcal{I}\rangle\)where:

\(\mathcal{T}= \left\langle T, \prec \right\rangle\) is a temporalframe;
\(\mathcal{U}\) is theglobal domain(universe)ofthe model;
\(D: T \to \mathcal{P}(\mathcal{U})\) is adomain functionthat assigns to each time instant \(t\in T\) alocal domain\(D_{t} \subseteq \mathcal{U}\) such that \(\mathcal{U}= \bigcup_{t\in T}D_t\).^[7]
\(\mathcal{I}\) is aninterpretation function that assignsfor each time instant \(t\in T\):
- an object \(\mathcal{I}_{t}(c) \in \mathcal{U}\) to each constantsymbol \(c\);
- an \(n\)-ary relation \(\mathcal{I}_{t}(R) \subseteq \mathcal{U}^{n}\)to each \(n\)-ary predicate symbol \(R\).
Note that even though the interpretations of the constant andpredicate symbols are defined locally in that they are relativized toa given time instant, their extensions range over the global domain.This approach allows for reference to objects that do not currentlyexist and enables a proper treatment of cross-temporal relations, as,for example, in the sentence “One of my friends is a descendantof a follower of William the Conqueror”.

The quadruple \(\mathcal{F} = \langle T,\prec,\mathcal{U},D\rangle\)is called theaugmented temporal frame (or theskeleton) of the model \(\mathcal{M}\). Since the model issupposed to represent the temporal history of the world, the localdomains associated with the different time instants in the underlyingaugmented temporal frame must be suitably connected. There are fournatural cases to be distinguished, which relate back to the fournotions of existence discussed inSection 8.1 above:

varying domains: no restrictions apply;
expanding(increasing)domains: for all \(t,t' \in T\), if \(t\prec t',\) then \(D_{t} \subseteq D_{t'}\);
shrinking(decreasing)domains: for all \(t,t' \in T\), if \(t\prec t',\) then \(D_{t'} \subseteq D_{t}\);
locally constant domains: for all \(t,t' \in T\), if \(t\prec t',\) then \(D_{t} = D_{t'}\).

Thus, an augmented temporal frame \(\mathcal{F}\) has locally constantdomains if and only if it has both expanding and shrinking domains. Wesay that \(\mathcal{F}\) hasa constant domain if all localdomains equal the global domain. Note that, since the global domain isrequired to be the union of all local domains, having locally constantdomains implies having a constant domain just in case the set of timeinstants forms a temporally connected structure.

8.3 Semantics of FOTL

There is a variety of semantics for first-order modal logics, whichcan be adapted to first-order temporal logics, including counterpartsemantics, bundle semantics, metaframe semantics, admissible setssemantics, etc. We present here the temporal versions of the standardsemantics for first-order modal logic as provided in Fitting andMendelsohn (2023).

As in propositional temporal logic, formulae of FOTL are evaluatedlocally at time instants. However, since FOTL formulae may containvariables, their evaluation at a given time instant in a first-ordertemporal model depends also on a variable assignment. Let us denotethe set of individual variables of FOTL by \(\mathrm{VAR}\) and theset of individual terms (i.e. variables and constants) by\(\mathrm{TERM}\). Given a first-order temporal model \(\mathcal{M}=\langle T, \prec,\mathcal{U},D,\mathcal{I}\rangle\), avariableassignment in \(\mathcal{M}\) is a mapping \(v: \mathrm{VAR} \to\mathcal{U}\) that assigns to each variable \(x \in \mathrm{VAR}\) anobject \(v(x)\) in the global domain \(\mathcal{U}\). Such anassignment can be uniquely extended to a time-relativetermvaluation as follows: \[v_{t}(x) := v(x), \ v_{t}(c) := \mathcal{I}_{t}(c).\] While variable assignments areconstant across time, the interpretation of the constant symbolsdepends on the respective time instant. (Versions where variables areevaluated locally as well have also been studied, see e.g. Gabbay etal. 2009.)

Thetruth of an arbitrary formula \(\varphi\) of FOTL at a giventime instant \(t\) in a first-order temporal model \(\mathcal{M}\)with respect to a variable assignment \(v\) (denoted\(\mathcal{M},t \models_{v} \varphi\)) is now defined inductively asfollows:

\(\mathcal{M},t \models_{v} R(\tau_{1},\ldots,\tau_{n})\) iff \(\langle v_{t}(\tau_{1}),\ldots,v_{t}(\tau_{n})\rangle \in\mathcal{I}_{t}(R)\),
for any \(n\)-ary predicate symbol \(R\) and terms\(\tau_{1},\ldots,\tau_{n} \in \mathrm{TERM}\);
\(\mathcal{M},t \models_{v} \tau_{1}=\tau_{2}\) iff \(v_{t}(\tau_1) = v_{t}(\tau_2)\), for any terms \(\tau_{1},\tau_{2}\in \mathrm{TERM}\);
\(\mathcal{M},t \models_{v} \lnot \varphi\) iff \(\mathcal{M},t\not\models_{v} \varphi\);
\(\mathcal{M},t\models_{v} \varphi \land \psi\) iff \(\mathcal{M},t\models_{v} \varphi\) and \(\mathcal{M},t\models_{v}\psi\);
\(\mathcal{M},t\models_{v} P \varphi\) iff \(\mathcal{M},t'\models_{v} \varphi\) for some \(t'\in T\) such that\(t' \prec t\);
\(\mathcal{M},t\models_{v} F \varphi\) iff \(\mathcal{M},t'\models_{v} \varphi\) for some \(t'\in T\) such that\(t \prec t'\);
\(\mathcal{M},t\models_{v} \forall x \varphi\) iff …
- presentist quantification:…\(\mathcal{M},t\models_{v[a/x]} \varphi\) for every \(a\inD_{t}\);
- eternalist quantification:…\(\mathcal{M},t\models_{v[a/x]} \varphi\) for every \(a\in\mathcal{U}\),
where \(v[a/x]\) is the variant of the variable assignment \(v\) thatassigns to the variable \(x\) the object \(a\), i.e. \(v[a/x](x) =a\).

As we mentioned earlier, there are two natural approaches toquantification in temporal logic:presentist quantificationandeternalist quantification. Technically, presentistquantification amounts to quantification over thelocaldomain at the given time instant, whereas eternalist quantification isconstrued as quantification over theglobal domain. Therespective semantic clauses for the dual \(\exists\) of \(\forall\)accordingly read as follows:

\(\mathcal{M},t\models_{v} \exists x \varphi\) iff …
- presentist quantification:…\(\mathcal{M},t\models_{v[a/x]} \varphi\) for some \(a\inD_t\);
- eternalist quantification:…\(\mathcal{M},t\models_{v[a/x]} \varphi\) for some \(a\in\mathcal{U}\).

Note that presentist quantification naturally suggests first-ordertemporal models with varying domains. In the semantics based oneternalist quantification the local domains do not play any essentialrole. In fact, eternalist quantification is tantamount to theassumption that the model has a constant domain, i.e., all localdomains equal the global domain. In what follows, we often refer tothe semantics with presentist quantification asvarying domainsemantics and to the semantics with eternalist quantification asconstant domain semantics.

In each of these semantics, a FOTL formula \(\varphi\) is said to bevalid in a first-order temporal model \(\mathcal{M}\) iff itis true in that model at each time instant with respect to everyvariable assignment; it isvalid in an augmented temporalframe iff it is valid in each model based on that frame; and itisvalid iff it is valid in every model.

Adopting one or the other approach to quantification affects thenotion of validity, even for non-temporal principles. For instance,the sentence \(\exists x(x= c)\) is valid in first-order logic, and itis valid in the constant domain semantics as well. However, it is nolonger valid in the varying domain semantics because the objectassigned to the constant \(c\) may not belong to the local domain.Another principle from plain first-order logic that distinguishes thetwo semantics is the scheme ofUniversal Instantiation (where\(\tau\) is any term free for substitution for \(x\) in \(\varphi\)):\[\forall x \varphi(x) \to \varphi(\tau),\] which is likewise valid in the constant domain semanticsbut invalid in the varying domain semantics, for analogous reasons.The main distinction between the two semantics, however, is reflectedin principles involving interaction of temporal operators andindividual quantifiers, such as the Barcan formula schemata and theirconverses. In the following two sections, we take a closer look atvalidity in the respective semantics.

8.4 Eternalist quantification and constant domain semantics

Let us consider some FOTL validities and non-validities in theconstant domain semantics, that is, in the semantics with eternalistquantification. We denote validity in the constant domain semantics by\(\models_{\mathrm{CD}}\).

All FOTL instances of valid first-order formulae areCD-valid.
In particular, the scheme ofUniversal Instantiation isCD-valid:
\(\models_{\mathrm{CD}} \forall x \varphi(x) \to \varphi(\tau)\), forany term \(\tau\) free for substitution for \(x\) in\(\varphi\).
TheFuture Barcan Formula^[8] scheme, \(\mathsf{BF}_{G}\), is CD-valid:
\(\models_{\mathrm{CD}} \forall x G \varphi(x) \to G \forall x\varphi(x)\) or, equivalently,
\(\models_{\mathrm{CD}} F \exists x \varphi(x) \to \exists x F\varphi(x)\).
TheConverse Future Barcan Formula scheme,\(\mathsf{CBF}_{G}\), is CD-valid:
\(\models_{\mathrm{CD}} G \forall x \varphi(x) \to \forall x G\varphi(x)\) or, equivalently,
\(\models_{\mathrm{CD}} \exists x F \varphi(x) \to F \exists x\varphi(x)\).
Some important non-validities include:
\(\not\models_{\mathrm{CD}} \forall x F \varphi(x) \to F \forall x\varphi(x)\) and \(\not \models_{\mathrm{CD}} G \exists x\varphi(x) \to \exists x G \varphi(x)\).

Analogous claims hold for the past versions of the above schemata,with \(H\) and \(P\) instead of \(G\) and \(F\). An axiomatic systemfor the minimal FOTL with constant domain semantics as well as someimportant theorems of it are provided in the supplementarydocument:

Axiomatic SystemFOTL(CD) for the Minimal FOTL with Constant Domain Semantics

8.5 Presentist quantification and varying domain semantics

In the varying domain semantics, the range of the individualquantifiers is restricted to the local domains. As a consequence, someformulae that are valid in the semantics with constant domains are nolonger valid in the varying domain semantics. Most importantly, thevarying domain semantics invalidates Universal Instantiation \(\forallx \varphi(x) \to \varphi(\tau)\) as well as both the Future and PastBarcan Formula schemata and their converses. We denote validity in thevarying domain semantics by \(\models_{\mathrm{VD}}\).

It turns out that the Barcan formulae schemata \(\mathsf{BF}_{G}\) and\(\mathsf{BF}_{H}\) and their converses \(\mathsf{CBF}_{G}\) and\(\mathsf{CBF}_{H}\) define conditions on the local domains. For anyaugmented temporal frame \(\mathcal{F}\), the following holds:

\(\mathcal{F}\) has expanding domains iff \(\mathcal{F}\models_{\mathrm{VD}} \mathsf{BF}_{H}\) iff \(\mathcal{F}\models_{\mathrm{VD}} \mathsf{CBF}_{G}\);
\(\mathcal{F}\) has shrinking domains iff \(\mathcal{F}\models_{\mathrm{VD}} \mathsf{BF}_{G}\) iff \(\mathcal{F}\models_{\mathrm{VD}} \mathsf{CBF}_{H}\).

Note that the Future Barcan scheme \(\mathsf{BF}_{G}\) semanticallycorresponds to the converse Past Barcan scheme \(\mathsf{CBF}_{H}\),andvice versa. From the above it follows that an augmentedtemporal frame \(\mathcal{F}\) has locally constant domains iff eitherof the following formulae is VD-valid in \(\mathcal{F}\):\(\mathsf{BF}_{G} \wedge \mathsf{BF}_{H}\), \(\mathsf{CBF}_{G} \wedge\mathsf{CBF}_{H}\), \(\mathsf{BF}_{G} \wedge \mathsf{CBF}_{G}\), or\(\mathsf{BF}_{H} \wedge \mathsf{CBF}_{H}\).

An axiomatic system for the minimal FOTL with varying domain semanticsis provided in the supplementary document:

Axiomatic SystemFOTL(VD) for the Minimal FOTL with Varying Domain Semantics

8.6 The existence predicate

Although presentism and eternalism are philosophically distinctontologies, their technical manifestations are interreducible. On theone hand, the constant domain semantics with eternalist quantificationcan be obtained from the varying domain semantics with presentistquantification by imposing the constraint that the Past and FutureBarcan Formula schemata and their converses be valid (provided thatthe temporal frame is connected). On the other hand, the varyingdomain semantics can be simulated in the constant domain semantics byadding to the language of FOTL anexistence predicate \(E\)for ‘existence at the current time instant’ with thefollowing semantics: \(\mathcal{M},t\vDash_v E(\tau)\) iff \(v_t(\tau)\in D_t\). In the varying domain semantics, \(E\) can be defined by\(E(\tau) := \exists x (x=\tau)\).

The existence predicate enables an alternative formalization of thesentence “Some man exists who signed the Declaration ofIndependence”. Instead of writing \[\exists x(\mathsf{man}(x) \land P(\mathsf{signs}(x))),\] we can write\[\exists x(E(x) \land \mathsf{man}(x) \land P(\mathsf{signs}(x))).\] Assuming a constant domain semantics with eternalistquantification, the first formula is true at the present instant,whereas the second formula is presently false. It was true in1777.

For every formula \(\varphi\) of FOTL, we can form its\(E\)-relativization by replacing every occurrence of\(\forall x\) in \(\varphi\) by “\(\forall x (E(x) \to...)\)” and every occurrence of \(\exists x\) by“\(\exists x (E(x) \land ...)\)”. We then have that\(\varphi\) is valid in the varying domain semantics if and only ifits \(E\)-relativization is valid in the constant domain semantics.The question that remains, from a philosophical point of view, iswhether existence is a legitimate predicate. An axiomatic system forthe minimal FOTL with existence predicate can be obtained along thelines of free logic, as outlined in the supplementary document:

Axioms for the Minimal FOTL with \(E\): the Free Logic Version

8.7 Proper names and definite descriptions

A further issue arising in first-order temporal logics concerns theinterpretation of individual terms. Depending on what kind of terms weare dealing with, we may or may not want to allow their interpretationto vary with time.

In the semantics outlined above, variable assignments are definedglobally, and hence individual variables pick out the same object atall times. In other words, they arerigid designators. Theinterpretation of the constant symbols, on the other hand, isspecified locally, i.e. relative to a time instant. If we wish toregard constants as proper names, it seems natural to treat them asrigid designators, too. Constant symbols can then be used to identifyan object across different times. For instance, treating \(a\) as aname for Aristotle, the sentence “Aristotle was sitting but nowhe is standing” can be formalized as \(P\mathsf{sit}(a) \wedge\mathsf{stand}(a)\). Note that if constants are treated as rigiddesignators, the principle of theNecessity of Identity\(\tau_1 = \tau_2 \rightarrow A(\tau_1 = \tau_2)\) is valid, for bothvariables and constants (recall that \(A \varphi = H \varphi \land\varphi \land G\varphi\)).

But there are also individual terns that are not rigid. Prime examplesaredefinite descriptions, such as “the Pope”,which may pick out different objects at different times. Clearly,proper names and definite descriptions will require a differentsemantic treatment and are not freely inter-substitutable. For example“The Pope was born in Argentina” was false in 2012,whereas “Jorge Mario Bergoglio was born in Argentina” wastrue then. Moreover, in a temporal setting, the question arises how todeal with definite descriptions that refer to objects that do nolonger or do not yet exist, such as “the first child to be bornin South Africa in 2050”. The issues get even more intricate ina branching time setting, where time and modality are combined. Note,for instance, that some definite descriptions that are temporallyrigid may be modally non-rigid. For more on definite descriptions andtheir challenges in the context of temporal logic, see Rescher andUrquhart (1971, Chapters XIII and XX) and Cocchiarella (2002).

One way to deal with definite descriptions is to switch from anextensional to an intensional account of individual terms. That is,rather than assigning to each term at each time instant anextension, i.e. an object from the domain, one mayassign to each term anintension, i.e. a function fromtime instants to objects. A general framework in which individualterms are assigned both extensions and intensions is the CaseIntensional First-Order Logic (CIFOL) proposed in Belnap andMüller (2014a; 2014b). In CIFOL, identity is extensional,predication is intensional, and individuals can be identified acrosstimes without making use of rigid designation. The framework alsobecomes interesting in the debate on persistence as it remainsmetaphysically neutral with respect to the precise nature of theobjects included in the overall domain: it could be genuineindividuals, but it could just as well be temporal stages.

8.8 Some technical results on first-order temporal logics

First-order temporal logics are very expressive, and this often comeswith a high computational price: these logics can be deductively verycomplex and are typicallyhighly undecidable (cf. Merz 1992;Gabbay et al. 1994; Hodkinson et al. 2002). The first-ordertemporal logic with constant domain semantics over the naturalnumbers, for example, with only two variables and unary relationsymbols is not only undecidable but not even recursively axiomatizable(cf. Börger et al. 1997; Hodkinson et al. 2000).

Few axiomatizable — and even fewer decidable — naturalfragments of first-order temporal logics have been identified andinvestigated so far. These include first-order temporal logics withSince andUntil over the class of all linear flowsof time and over the order of the rationals (Merz 1992; Reynolds1996), the fragment T(FOs) of FOTL, where temporal operators may notoccur inside the scope of an individual quantifier (Gabbay etal. 1994, Chapter 14), as well as themonodic fragment,only allowing formulae with at most one free variable in the scope ofa temporal operator (see Hodkinson et al. 2000; 2001; 2002 andWolter and Zakharyaschev 2002). Still, as shown in the latter paper,already the monodic fragment with equality is no longer recursivelyaxiomatizable. For further decidability results for suitablyrestricted fragments of FOTL, see Hodkinson et al. (2000).Additional technical references are given in Gabbay et al. (1994,Chapter 14) and Kröger and Merz (2008). For completeness resultsfor first-order modal logics, see also Fitting and Mendelsohn (2023)and the entry onmodal logic.

For further philosophical discussion on first-order modal and temporallogics, see Rescher and Urquhart (1971, Chapter XX); McArthur (1976);Garson (1984): Linsky and Zalta (1994); van Benthem (1995, Section 7);Fitting and Mendelsohn (2023); Wölfl (1999); Cocchiarella (2002);as well as Lindström and Segerberg (2007).

9. Combining temporal and other logics

Logics are used to model various aspects of the world, includingaspects that may dynamically change over time. For instance, thenotion of knowledge studied in epistemic logic, the idea of an actionunderlying logics of agency, or the concept of space in spatial logicsall bear an intimate relation to time. It is therefore natural to adda temporal dimension to these logics and equip the correspondinglanguages with temporal operators.

From a technical point of view, there are several ways of combiningmodels and logical systems: products, fusions, etc. (see the entry oncombining logics). These constructions provide different mechanisms for temporalizing alogic. Generic questions about transfer of logical properties, such asaxiomatizability and decidability, arise: decidability, for instance,is usually preserved in fusions, while it is often lost in products oflogical systems. For a general discussion of temporalizing logicalsystems and properties of temporalized logics, see Finger and Gabbay(1992; 1996); Finger et al. (2002); and Gabbay et al. (2003). Here webriefly discuss some of the most popular cases of temporalized logicalsystems.

9.1 Temporal-epistemic logics

Temporal-epistemic logics bring together temporal logics and(multi-agent) logics of knowledge. Some interesting properties cannaturally be expressed by combining the epistemic modality \(K\)(“the agent knows that”) with temporal operators. Here arejust two examples:perfect recall: \(K \varphi \to GK\varphi\) (If the agent knows \(\varphi\) now, then the agent willalways know \(\varphi\) in the future) andno learning: \(FK\varphi \to K \varphi\) (If the agent will know \(\varphi\) at sometime in the future, then the agent already knows \(\varphi\) now).

Various temporal-epistemic logics were developed during the 1980s,with a unifying study by Halpern and Vardi (1989). They consider avariety of 96 temporal-epistemic logics on so-calledinterpretedsystems, i.e. sets of temporal runs in a transition system withepistemic indistinguishability relations on the state space for eachagent. The variety is based on several parameters:number ofagents (one or many),the language (with or withoutcommon knowledge),the formal model of time (linear orbranching time),recall abilities (no recall, bounded recall,or perfect recall),learning abilities (learning or nolearning),synchrony (synchronous or asynchronous),unique initial state. Depending on the particular choice ofthese parameters, the computational complexity of the decision problemfor these logics ranges very broadly from PSPACE-complete to highlyundecidable (\(\Pi^{1}_{1}\)-complete). For details, see Halpern andVardi (1989); Fagin et al. (1995); as well as the more recent vanBenthem and Pacuit (2006), which surveys a number of decidability andundecidability results for temporal-epistemic logics and illustrateshow the combination of time with other modalities bears oncomputational complexity.

9.2 Temporal logics and logics of agency

Temporal reasoning is an important aspect of reasoning about agentsand their actions. Probably the most influential family of logics ofagency in philosophy is the family of so-calledstit logics,originating from the work of Belnap and Perloff (1988). These logicscontain formulae of the formstit\(\varphi\), reading“The agent sees to it that \(\varphi\)”, which allow oneto reason about how an agent’s action choices affect the world.The original versions ofstit logic do not involve temporaloperators. Nevertheless, their semantics is based on Ockhamist treemodels, where an agent’s set of choices at a given time instantis represented by a partition of the set of histories passing throughthat instant. Roughly, the formulastit\(\varphi\) is true atan instant \(t\) with respect to a history \(h\) iff the agent’schoice at the instant \(t\) with respect to the history \(h\)guarantees that \(\varphi\), i.e. if \(\varphi\) is true at \(t\)relative to all histories in the choice cell containing \(h\). For adetailed discussion of varieties ofstit logic and theirhistorical development, see Segerberg (1992); Belnap et al. (2001) andthe entry onthe logic of action. Temporal extensions ofstit logics have first been proposedin Broersen (2011) and Lorini (2013): in Broersen (2011) thestit operator is combined with theNext Timeoperator \(X\) into a single operator which requires that theobjective be met in the next step, whereas in Lorini (2013) thestit operator and the temporal operators are treatedseparately. Furthermore, in Broersen (2019) a spatial dimension isadded to the temporal dimension.

Another important family of temporal logics of agency are thealternating-time logics ATL and ATL*, introduced in Alur etal. (2002). ATL and ATL* are multi-agent extensions of the computationtree logics CTL and CTL*, and they have become a popular logicalframework for strategic reasoning in multi-agent systems.Alternating-time temporal logics enrich the language with strategicpath quantifiers \(\langle\!\langle C \rangle\!\rangle \varphi,\)intuitively saying “The coalition \(C\) has a collectivestrategy to guarantee that the objective \(\varphi\) is met”,where the objective \(\varphi\) is a temporal formula. That is, theformula \(\varphi\) is required to be true in every path enabled bythe collective strategy of \(C\). Whilestit logics build onbranching time, ATL and ATL* are interpreted over so-called concurrentgame structures, in which paths are viewed as sequences of statesgenerated by collective actions of all agents. A combination of ATLandstit theory was developed in Broersen et al. (2006). Thebranching time logics CTL and CTL* can be regarded as single-agentversions of ATL and ATL*. Even though the latter are much moreexpressive, they generally preserve the good computational propertiesof the former. For details, see Alur et al. (2002), as well as Gorankoand van Drimmelen (2006), where a complete axiomatization anddecidability results for ATL are established. A general introductionto ATL from a temporal logic perspective is provided in Demri et al.(2016, Chapter 9).

9.3 Spatial-temporal logics

Space and time are intimately related in the physical world, and theyhave become inseparable in modern physical theories. While earlyphysical theories, culminating in Newton’s classical mechanics,presuppose an absolute notion of time that is independent of space,Einstein’s relativity theory views time and space asinextricably interwoven, as modeled by Minkowski’sfour-dimensional space-time manifold.

Early thoughts on space-time and special relativity theory can alreadybe found in Prior’s work (see Kofod 2020 for a discussion ofPrior’s youth ideas and Prior 1967 for his mature work.) InGoldblatt (1980), the Diodorean modal logic of Minkowski space-timewas studied and proved to be exactly the modal logic D4.2, as Priorhad conjectured. Further results are provided in Uckelman and Uckelman(2007). Logical investigations into general relativity theory havebeen conducted as well, see e.g. Andréka et al. (2007).

In Artificial Intelligence, space-time reasoning has been activelyevolving over the past decades, particularly in the context ofspatio-temporal ontologies, databases, and constraint networks. Themain focus here is on the logical characterization of spatio-temporalmodels, computational complexity, and expressiveness (Gabelaia et al.2005; Kontchakov et al. 2007).

Another interesting line of research is triggered by the theory ofbranching space-times, initially developed in Belnap (1992). Thistheory relates to space-time just as Prior’s theory of branchingtime relates to linear time; that is, it combines space-time reasoningwith indeterminism. An extensive presentation of branching space-timescan be found in Belnap et al. (2022). For an intuitive introduction,see Belnap (2012).

9.4 Temporal description logics

Description logics are essentially variations of modal logics. Theyinvolveconcepts (unary predicates) androles(binary predicates) and are used to describe various ontologies andthe relations between the concepts in them (see e.g. Baader and Lutz2007). For example, the description logic term\(\textsf{philosopher}\sqsubseteq\exists \mathsf{READ}.\textsf{book}\)says that every philosopher reads a book. Description logics can betemporalized in various ways. E.g. the temporalized version\(G(\textsf{philosopher} \sqsubseteq P\,\mathsf{READ}.\textsf{book})\) allows us to express that it willalways be the case that everyone who is a philosopher has read a book.For more on temporal description logics, see Artale and Franconi(2000); Wolter and Zakharyaschev (2000); and Lutz et al. (2008).

9.5 Temporal logics and other non-classical logics

Temporal reasoning can naturally be combined with variousnon-classical logical systems, resulting, for instance, in many-valuedtemporal logics (Rescher and Urquhart 1971, Chapter XVIII),intuitionistic temporal logics (Ewald 1986), constructive andparaconsistent temporal logics (Kamide and Wansing 2010; 2011),probabilistic temporal logics (Hart and Sharir 1986; Konur 2013),etc.

10. Logical deduction and decision methods for temporal logics

There exists a great variety of deduction systems and decision methodsfor the temporal logics mentioned here and many more.Hilbertstyle axiomatic systems, such as the ones provided inSection 3.5 andSection 4.3, are the most common deduction systems for temporal logics. Butnumerousnatural deduction systems,sequent calculi,resolution-based systems, andsemantic tableauxsystems have been proposed as well. We briefly discuss the latterbelow. Some general references on deductive systems for temporallogics (in addition to the more specific references mentionedelsewhere in this text) include: Rescher and Urquhart (1971); McArthur(1976); Burgess (1984); Emerson (1990); Goldblatt (1992); Gabbay etal. (1994); van Benthem (1995); Bolc and Szalas (1995); Gabbay andGuenthner (2002); Gabbay et al. (2003); Fisher et al. (2005);Blackburn et al. (2007); Baier and Katoen (2008); Kröger and Merz(2008); Fisher (2011); Demri et al. (2016).

One of the most important logical decision problems is to determinewhether a given formula is valid, respectively satisfiable.Particularly efficient and practically useful for this purpose are thetableaux-based methods, originating from pioneering work byBeth, Hintikka, Smullyan, and Fitting. Unlike axiomatic systems,semantic tableaux calculi are refutation-based systems: in order toprove validity, one negates the input formula and shows that thenegation is not satisfiable. This is done by a systematic, tree-likesearch for a satisfying model, and the search is guaranteed to findsuch a model whenever it exists. If no model for the negation can befound, the input formula must be valid. A survey on tableaux systemsfor many temporal logics is provided in Goré (1999). Morespecific references include: Ben-Ari et al. (1983) for the branchingtime logic UB; Emerson and Halpern (1985) for the computation treelogic CTL; Wolper (1985) for the linear time temporal logic LTL;Kontchakov et al. (2004) on temporalizing tableaux; Reynolds (2007)for CTL with bundled tree semantics; Goranko and Shkatov (2010) forATL; Reynolds (2011) for the full computation tree logic CTL*;Reynolds (2014) for the real-time temporal logic RTL, etc.

In addition to the proof systems mentioned above, anothercomputationally powerful approach for solving logical decisionproblems areautomata-based methods, which have been activelydeveloping since the early 1990s. These methods transform temporalformulae into automata on infinite words (for linear time logics) orinfinite trees (for branching time logics) and represent models forthe logics as input objects (infinite words or trees) for theassociated automata. Thus, satisfiability of a formula becomesequivalent to the automaton accepting at least one input, i.e. thelanguage of the automaton being non-empty. The methods are based onclassical results about decidability of the monadic second-ordertheories of the natural numbers (by Büchi) and of the infinitebinary tree (by Rabin). For instance, in Emerson and Sistla (1984),automata on infinite trees and Rabin’s theorem were used toobtain a decision procedure for CTL*. For further details see Vardi(2007).

Important references on decidability results and decision proceduresfor various temporal logics include: Burgess (1980) and Gurevich andShelah (1985) for branching time logics; Burgess and Gurevich (1985a;1985b) for linear temporal logics; Goldblatt (1992) for both linearand branching time logics; Montanari and Policriti (1996) for metricand layered temporal logics; French (2001) for some quantifiedpropositional branching time logics.

While most propositional temporal logics are decidable, adding someextra syntactic or semantic features can make them explodecomputationally and become undecidable. The most common causes ofundecidability of temporal logics, besides combinations with otherexpressive logics, include: grid-like models; temporal operators alongmultiple time-lines; products of temporal logics; interval-basedlogics with no locality assumptions; time reference mechanisms, suchas hybrid reference pointers and freeze quantifiers; arithmeticfeatures, such as time addition, exact time constraints, etc. Suchnegative results have given rise to extensive research on how to tametemporal logics and restore decidability, such as adding syntactic andparametric restrictions (e.g. on the number of propositional variablesor the depth of nesting), imposing suitable semantic restrictions(e.g. locality for interval logics), identifying decidable fragments(e.g. the two-variable fragment FO\(^{2}\) of classical first-orderlogic, guarded fragments, monodic fragments), etc.

11. Applications of temporal logics

Temporal logic is a field whose early development was largely drivenby philosophical considerations. In a surprisingly short time,however, temporal logics were applied and further developed in variousdifferent disciplines, ranging from computer science, artificialintelligence, and linguistics, to natural, cognitive, and socialsciences. In this section, we briefly discuss some applications oftemporal logics in computer science, artificial intelligence, andlinguistics.

11.1 Temporal logics in Computer Science

The idea of applying temporal reasoning to the analysis ofdeterministic and stochastic transition systems was already present inthe theory of processes and events in Rescher and Urquhart (1971,Chapter XIV). However, it was with the seminal paper of Pnueli (1977)that temporal logic became important in computer science. Pnueliproposed the application of temporal logics to the specification andverification ofreactive and concurrent programs and systems.In order to ensure correct behavior of a reactive program, in whichcomputations are non-terminating (e.g. an operating system), it isnecessary to formally specify and verify the acceptable infiniteexecutions of that program. Moreover, to ensure correctness of aconcurrent program, where two or more processors are working inparallel, it is necessary to formally specify and verify theirinteraction and synchronization.

Key properties of infinite computations that can be captured bytemporal patterns are liveness, safety, and fairness (see Manna andPnueli 1992):

Liveness properties oreventualities involvetemporal patterns of the forms \(F{p},\) \(q \to F {p},\) or \(G(q \toF {p}),\) which ensure that if a specific precondition (\(q\)) isinitially satisfied, then a desirable state (satisfying \(p\)) willeventually be reached in the course of the computation. Examples are“If a message is sent, it will eventually be delivered”and “Whenever a printing job is activated, it will eventually becompleted”.
Safety orinvariance properties involve temporalpatterns of the forms \({G} {p},\) \(q \to {G} {p},\) or \(G(q \to {G}{p}),\) which ensure that if a specific precondition (\(q\)) isinitially satisfied, then undesirable states (violating the safetycondition \(p\)) will never occur. Examples are: “No more thanone process will be in its critical section at any moment oftime”, “A resource will never be used by two or moreprocesses simultaneously”, or, to give more practical examples:“The traffic lights will never show green in bothdirections”, “A train will never pass a redsemaphore”.
Fairness properties involve combined temporal patterns ofthe forms \({GF} {p}\) (“infinitely often \(p\)”) or\({FG} {p}\) (“eventually always \(p\)”). Intuitively,fairness requires that whenever several processes that share resourcesare run concurrently, they must be treated ‘fairly’ by theoperating system, scheduler, etc. A typical fairness requirement saysthat if a process is persistent enough in sending a request (e.g.keeps sending it over and over again), its request will eventually begranted.

An infinite computation is formally represented by a model of thelinear time temporal logic LTL. Non-deterministic systems are modeledby tree structures. Thus, both LTL and the computation tree logics CTLand CTL* have become instrumental in the specification andverification of reactive and concurrent systems.

The following example refers to a single computation and combinesliveness and safety properties: “Whenever a state of alert isreached, the alarm is activated and remains activated until a safestate is eventually reached”. This property is expressible inLTL as

\[ G(\textsf{alert} \to (\textsf{alarm} \ U\ \textsf{safe})).\]

Another example, referring to all computations in the system, is:“If the process \(\sigma\) is eventually enabled on somecomputation starting from the current state, then on every computationstarting there, whenever \(\sigma\) is enabled, it will remain enableduntil the process \(\tau\) is disabled”. This property can beformalized in CTL* as

\[ \Diamond F\,\textsf{enabled}_{\sigma} \to \BoxG(\textsf{enabled}_{\sigma} \to (\textsf{enabled}_{\sigma} \,U\,\textsf{disabled}_{\tau})). \]

A variation of LTL useful for specifying and reasoning aboutconcurrent systems is Lamport’s (1994)temporal logic ofactions TLA. Other applications of temporal logics in computerscience include: temporal databases, real-time processes and systems,hardware verification, etc. Further details on such applications canbe found in e.g. Pnueli (1977); Emerson and Clarke (1982); Moszkowski(1983); Galton (1987); Emerson (1990); Alur and Henzinger (1992);Lamport (1994); Vardi and Wolper (1994); Bolc and Szalas (1995);Gabbay et al. (2000); Baier and Katoen (2008); Kröger and Merz(2008); Fisher (2011); Demri et al. (2016).

11.2 Temporal logics in Artificial Intelligence

Artificial Intelligence (AI) is one of the major areas of applicationof temporal logics. Important topics in AI which have been exploredwith their help include: temporal ontologies, spatial-temporalreasoning, temporal databases and constraint solving, executabletemporal logics, temporal planning, temporal reasoning in agent-basedsystems, and natural language processing. Comprehensive overviews of awide variety of applications may be found in e.g. Vila (1994); Galton(1995); Fisher et al. (2005); and Fisher (2008). See also the relateddiscussion on reasoning about action and change in Section 4 of theentry onlogic and artificial intelligence.

The idea of relating temporal reasoning and AI was first discussed inthe late 1960s and 70s, and it flourished in the 1980s and 90s; foroverviews of historical developments, see Galton (1987); Vila (1994);Øhrstrøm and Hasle (1995); and Pani and Bhattacharjee(2001). The combination of temporal logic and AI was suggested in theearly philosophical discussion on AI by McCarthy and Hayes (1969), thetheory of processes and events in Rescher and Urquhart (1971, ChapterXIV), and the period-based theories of Hamblin (1972). Seminal workfrom the 1980s and 90s include: McDermott’s (1982) temporallogic for reasoning about processes and plans, Allen’s (1984)general theory of action and time, the event calculus of Kowalski andSergot (1986), the reified temporal logic by Shoham (1987), the logicof time representation by Ladkin (1987), the work on temporal databasemanagement by Dean and McDermott (1987), the introduction ofinterval-based temporal logics by Halpern and Shoham (1991) and byAllen and Ferguson (1994) (with representation of actions and events),the situation calculus of Pinto and Reiter (1995), and Lamport’s(1994) action theory.

Although it is much concerned with applications, the debate in the AIliterature raises interesting philosophical issues, too. Philosophicalquestions naturally arise with respect to the ontological foundationsof the temporal models: the choice between discrete and continuous,instant-based and interval-based temporal models is one example. Bothinstant-based and interval-based approaches have been developed andcompared, see e.g. van Benthem (1983); Allen (1983); Allen and Hayes(1989); Allen and Ferguson (1994); Galton (1090; 1995); Vila (2005);etc.

Furthermore, the AI literature distinguishes between different kindsof temporal phenomena, such as fluents, events, actions, and states.While fluents concern states of the world that may change over time(e.g. whether the light is on or off), events and actions representwhat happens in the world and causes changes between states (e.g. theturning on of the light, the room becoming light). Theories oftemporal incidence explore the structural properties of thesephenomena, such as whether they are homogenous over an extended periodof time (e.g. if the light is on from 2 o'clock to 4 o'clock, can weinfer that it was on at 3 o'clock?). See e.g. Galton (2005); Vila(2005); etc.

Once we have incorporated such temporal phenomena in our models, weneed to specify a logical language that allows us to express when theyhappen or occur. In the AI literature, different methods of temporalqualification can be found. For an overview, see Reichgelt and Vila(2005). Traditionally, temporalized variations of first-order logicrather than Prior style temporal logics have been used. Perhaps thesimplest first-order approach is the so-calledmethod of temporalarguments (McCarthy and Hayes 1969; Shoham 1987; Vila 1994). Herethe temporal dimension is captured by augmenting propositions andpredicates with ‘time stamp’ arguments; for example“Publish(A. Prior,Time and Modality, 1957)”. Analternative, yet closely related approach, is that ofreifiedtemporal logics (McDermott 1982; Allen 1984; Shoham 1987; see Maand Knight 2001 for a survey). This approach makes use of reifyingmeta-predicates, such as ‘TRUE’ and ‘FALSE’,but also ‘HOLDS’, ‘OCCURS’,‘BEFORE’, ‘AFTER’, and interval relations suchas ‘MEETS’, ‘OVERLAPS’, etc., which areapplied to propositions of some standard logical language (e.g.classical first-order logic); for example “OCCUR(Born(A. Prior),1914)”. Still, the modal-logic style approach has had a recentresurgence, e.g. in the context of agent-based temporal reasoning (cf.Fisher and Wooldridge 2005).

However, philosophical questions arise not only with respect totraditional issues, such as the choice of the temporal models and thequestion about which temporal phenomena exist and how they are to bereasoned about. AI supplies novel puzzles as well. A famous example istheframe problem: if a change occurs, how can we keep trackof what does not change as a result? This problem has been widelyexplored and relates to issues in philosophy and cognitive science.For a detailed discussion, see the entry on theframe problem.

11.3 Temporal logics in Linguistics

Tense is an important feature of natural languages. It is a linguisticdevice that allows one to specify the relative location of events intime, usually with respect to the speech time. In several languages,including English, tense becomes manifest in a system of differentverbal tenses. English allows for a distinction between past, present,and future tense (‘will’ future), and traditionally, therespective perfect and progressive forms are referred to as tenses aswell.

As laid out above, Prior’s invention of tense logic wasmotivated by the use of tense in natural language. An alternativeearly logical approach to tense was provided by Reichenbach (1947),who suggested an analysis of the English verbal tenses in terms ofthree points in time: speech time, event time, and reference time,where the reference time is a contextually salient point in time,which, intuitively, captures the perspective from which the event isviewed. Using the notion of reference time, Reichenbach was able todistinguish, for example, between the simple past (“I wrote aletter”) and the present perfect (“I have written aletter”), which are conflated in Prior’s account. Withboth the simple past and the present perfect, the event time precedesthe speech time; but in the former case the reference time coincideswith the event time, whereas in the latter case the reference time issimultaneous with the speech time.

Neither Prior’s nor Reichenbach’s frameworks can accountfor the difference between, for instance, the simple past (“Iwrote a letter”) and the past progressive (“I was writinga letter”). The relevant distinction here is one of aspectrather than of tense and seems to call for an interval-based orevent-based setting. For accounts along these lines, see e.g. Dowty(1979); Parsons (1980); Galton (1984); and van Lambalgen and Hamm(2005).

Whereas Reichenbach’s analysis makes reference to a contextuallysalient point in time, on Prior’s account tenses are construedas temporal operators, which are interpreted as quantifiers overinstants in time. This raises the general question: are tenses innatural language to be treated as quantifiers, or do they refer tospecific points in time? In an influential paper, Partee (1973)provided the following counterexample against a quantifier treatmentof tenses: the sentence “I didn’t turn off thestove” means neither (1) there is an earlier time instant atwhich I do not turn off the stove, nor does it mean (2) there is noearlier instant at which I turn off the stove. The first requirementis too weak, the second too strong. Partee suggested an analogybetween tenses and referential pronouns. According to this proposal,tenses refer to specific, contextually given points in time (e.g. 8o’clock this morning), which are presupposed to stand inappropriate temporal relations to the speech time. Subsequently,accounts that restrict quantification to a contextually given timeinterval (e.g. this morning) have become popular. On these accounts,Partee’s example sentence has the intuitive meaning: there is noearlier time instant in the contextually salient time interval atwhich I turn off the stove. Formally, this is compatible with bothquantifier and referential treatments of tense; for details see Kuhnand Portner (2002) and Ogihara (2011). Moreover, the idea of combiningquantificational and referential elements can be dealt with in thehybrid variants of tense logic discussed inSection 7.1 (see Blackburn and Jørgensen 2016). The hybrid approach alsoallows for a Hans Kamp style treatment of temporal indexicals, such as“now” (Kamp 1971), as was noticed by Prior as early as1968 (Prior 1968).

Other pertinent issues in linguistics relating to time concern themeaning of temporal adverbs and connectives, the interaction of tenseand quantification, the interpretation of embedded tenses and sequenceof tense, as well as the interrelation of tense and modality. For anoverview and further discussion on the application of temporal logicsin linguistics, see e.g. Steedman (1997); Kuhn and Portner (2002);Mani et al. (2005); ter Meulen (2005); Moss and Tiede (2007); Ogihara(2007; 2011); Dyke (2013); and the entry ontense and aspect.

Bibliography

Albretsen, J., P. Hasle, and P. Øhrstrøm (eds.),2016,Special Issue on the Philosophy and Logic of A.N.Prior,Synthese, 193(11).
Allen, J.F., 1983, “Maintaining Knowledge about TemporalIntervals”,Communications of the ACM, 26(11):832–843.
–––, 1984, “Towards a General Theory ofAction and Time”,Artificial Intelligence, 23:123–154.
Allen, J.F., and G. Ferguson, 1994, “Actions and Events inInterval Temporal Logic”,Journal of Logic andComputation, 4(5): 531–579.
Allen, J.F., and P. Hayes, 1989, “Moments and Points in anInterval-Based Temporal Logic”,ComputationalIntelligence, 5(4): 225–238.
Alur, R., and T. Henzinger, 1992, “Logics and Models ofReal-Time: A Survey”, inReal-Time: Theory in Practice,Proceedings of the REX Workshop 1991 (Lecture Notes in ComputerScience: Volume 600), Berlin: Springer, pp. 74–106.
–––, 1993, “Real-Time Logics: Complexityand Expressiveness”,Information and Computation, 104:35–77.
–––, 1994, “A Really TemporalLogic”,Journal of the ACM, 41: 181–204.
Alur, R., T. Henzinger, and O. Kupferman, 2002,“Alternating-Time Temporal Logic”,Journal of theACM, 49(5): 672–713.
Andréka, H., V. Goranko, S. Mikulas, I. Németi, andI. Sain, 1995, “Effective First-Order Temporal Logics ofPrograms”, in Bolc and Szalas (1995), pp. 51–129.
Andréka, H., J. Madarász, and I. Németi,2007, “Logic of Space-Time and Relativity Theory”, in M.Aiello, J. van Benthem, and I. Pratt-Hartmann (eds.),Handbook ofSpatial Logics, Dordrecht: Springer, pp. 607–711.
Areces, C., and B. ten Cate, 2007, “Hybrid Logics”, inBlackburn et al. (2007), pp. 821–868.
Aristotle,Organon, II — On Interpretation, Chapter 9.See https://archive.org/stream/AristotleOrganon/AristotleOrganoncollectedWorks.
Artale, A., and E. Franconi, 2000, “A Survey of TemporalExtensions of Description Logics”,Annals of Mathematics andArtificial Intelligence, 30: 171–210.
Baader, F., and C. Lutz, 2007, “Description Logic”, inBlackburn et al. (2007), pp. 757–819.
Baier, C., and J.P. Katoen, 2008,Principles of ModelChecking, Cambridge, Massachusetts: MIT Press.
Balbiani, P., V. Goranko, and G. Sciavicco, 2011,“Two-Sorted Point-Interval Temporal Logics”, inProceedings of the 7th International Workshop on Methods forModalities (Electronic Notes in Theoretical Computer Science:Volume 278), pp. 31–45.
Belnap, N., 1992, “Branching Space-Time”,Synthese, 92(3): 385–434.
–––, 2012, “Newtonian Determinism toBranching Space-Time Indeterminism in Two Moves”,Synthese, 188: 5–21.
Belnap, N., and M. Green, 1994, “Indeterminism and the ThinRed Line”,Philosophical Perspectives, 8:365–388.
Belnap, N., and T. Müller, 2014a, “CIFOL:Case-Intensional First Order Logic (I): Toward a Theory ofSorts”,Journal of Philosophical Logic, 43(2–3):393–437.
–––, 2014b, “BH-CIFOL: Case-IntensionalFirst Order Logic (II): Branching Histories”,Journal ofPhilosophical Logic, 43(5): 835–866.
Belnap, N., T. Müller, and T. Placek, 2022,BranchingSpace-Times: Theory and Applications, Oxford: Oxford UniversityPress.
Belnap, N., and M. Perloff, 1988, “Seeing to it that: ACanonical Form for Agentives”,Theoria, 54:175–199, reprinted with corrections in H. E. Kyberg et al.(eds.),Knowledge Representation and Defeasible Reasoning,Dordrecht: Kluwer, 1990, pp. 167–190.
Belnap, N., M. Perloff, and M. Xu, 2001,Facing the Future:Agents and Choices in Our Indeterminist World, Oxford: OxfordUniversity Press.
Ben-Ari, M., A. Pnueli, and Z. Manna, 1983, “The TemporalLogic of Branching Time”,Acta Informatica, 20(3):207–226.
van Benthem, J., 1983,The Logic of Time, Dordrecht,Boston, and London: Kluwer Academic Publishers. [Second edition:1991.]
–––, 1984, “Tense Logic and Time”,Notre Dame Journal of Formal Logic, 25(1): 1–16.
–––, 1995, “Temporal Logic”, in D.M.Gabbay, C.J. Hogger, and J.A. Robinson (eds.),Handbook of Logicin Artificial Intelligence and Logic Programming (Volume 4),Oxford: Clarendon Press, pp. 241–350.
–––, 2001, “Correspondence Theory”,in D.M. Gabbay, and F. Guenther (eds.),Handbook of PhilosophicalLogic (Volume 3), Second Edition, Dordrecht: Kluwer, pp.325–408.
van Benthem, J., and E. Pacuit, 2006, “The Tree of Knowledgein Action: Towards a Common Perspective”, inAdvances inModal Logic (Volume 6), London: College Publications, pp.87–106.
Blackburn, P., 1993, “Nominal Tense Logic”,NotreDame Journal of Formal Logic, 34: 56–83.
–––, 2006, “Arthur Prior and HybridLogic”,Synthese, 150: 329–372.
Blackburn, P., J. van Benthem, and F. Wolter, 2007,Handbookof Modal Logic, Amsterdam: Elsevier.
Blackburn, P., P. Hasle, and P. Øhrstrøm (eds.),2019,Logic and Philosophy of Time: Further Themes from Prior(Volume 2), Aalborg: Aalborg University Press.
Blackburn, P., and K. Jørgensen , 2016, “Reichenbach,Prior, and Hybrid Tense Logic”,Synthese, 193(11):3677–3689.
Blackburn, P., M. de Rijke, and Y. Venema, 2001,ModalLogic, Cambridge: Cambridge University Press.
Blackburn, P., and J. Seligman, 1995, “HybridLanguages”,Journal of Logic, Language and Information,4: 251–272.
Blackburn, P., and M. Tzakova, 1999, “Hybrid Languages andTemporal Logic”,Logic Journal of the IGPL, 7:27–54.
Bolc, L., and A. Szalas (eds.), 1995,Time and Logic: AComputational Approach, London: UCL Press.
Börger, E., E. Grädel, and Y. Gurevich, 1997,TheClassical Decision Problem, Berlin, Heidelberg: Springer.
Boyd, S., 2014, “Defending History: Temporal Reasoning inGenesis 2:7–3:8”,Answers Research Journal, 7:215–237.
Bresolin, D., V. Goranko, A. Montanari, and G. Sciavicco, 2009,“Propositional Interval Neighborhood Logics: Expressiveness,Decidability, and Undecidable Extensions”,Annals of Pureand Applied Logic, 161(3): 289–304.
Bresolin, D., D. Della Monica, V. Goranko, A. Montanari, and G.Sciavicco, 2013, “Metric Propositional Neighborhood Logics onNatural Numbers”,Software and Systems Modeling, 12(2):245–264.
Broersen, J., 2011, “Deontic EpistemicStit LogicDistinguishing Modes of Mens Rea”,Journal of AppliedLogic, 9: 137–152.
–––, 2019, “Agents Necessitating Effectsin Newtonian Time and Space: From Power and Opportunity toEffectivity”,Synthese, 196: 31–68.
Broersen, J., A. Herzig, and N. Troquard, 2006, “ASTIT-Extension of ATL”, inProceedings of JELIA 2006(Lecture Notes in Artificial Intelligence: Volume 4160), Berlin:Springer, pp. 69–81.
Bull, R., 1970, “An Approach to Tense Logic”,Theoria, 36: 282–300.
Burgess, J., 1978, “The Unreal Future”,Theoria, 44(3): 157–179.
–––, 1979, “Logic and Time”,Journal of Symbolic Logic, 44: 566–582.
–––, 1980, “Decidability for BranchingTime”,Studia Logica, 39: 203–218.
–––, 1982a, “Axioms for Tense Logic I:‘Since’ and ‘Until’”,Notre DameJournal of Formal Logic, 23: 367–374.
–––, 1982b, “Axioms for Tense Logic II:Time Periods”,Notre Dame Journal of Formal Logic, 23:375–383.
–––, 1984, “Basic Tense Logic”, inD.M. Gabbay, and F. Guenthner (eds.),Handbook of PhilosophicalLogic (Volume 2), Dordrecht: Reidel, pp. 89–133. [Newedition in Gabbay and Guenthner (2002), pp. 1–42.]
–––, 2009,Philosophical Logic,Princeton: Princeton University Press.
Burgess, J., and Y. Gurevich, 1985, “The Decision Problemfor Linear Temporal Logic”,Notre Dame Journal of FormalLogic, 26(2): 115–128.
Ciuni, R., and A. Zanardo, 2010, “Completeness of aBranching-Time Logic with Possible Choices”,StudiaLogica, 96: 393–420.
Cocchiarella, N., 2002, “Philosophical Perspectives onQuantification in Tense and Modal Logic”, in Gabbay andGuenthner (2002), pp. 235–276.
Correia, F., and F. Iacona (eds.), 2013,Around the Tree:Semantic and Metaphysical Issues Concerning Branching and the OpenFuture (Synthese Library: Volume 361), Dordrecht: Springer.
Correia, F., and S. Rosenkranz, 2018,Nothing to Come: ADefense of the Growing Block Theory of Time (Synthese Library:Volume 395), Dordrecht: Springer.
Dean, T., and D.V. McDermott, 1987, “Temporal Data BaseManagement”,Artificial Intelligence,32:1–55.
Della Monica, D., V. Goranko, A. Montanari, and G. Sciavicco,2011, “Interval Temporal Logics: A Journey”,Bulletinof the European Association for Theoretical Computer Science,105: 73–99.
Demri, S., V. Goranko, and M. Lange, 2016,Temporal Logics inComputer Science, Cambridge: Cambridge University Press.
Dowty, D., 1979,Word Meaning and Montague Grammar,Dordrecht: Reidel.
Dyke, H., 2013, “Time and Tense”, in Dyke and Bardon(2013), pp. 328–344.
Dyke, H., and A. Bardon (eds.), 2013,A Companion to thePhilosophy of Time (Blackwell Companions to Philosophy), Oxford:Wiley-Blackwell.
Emerson, E.A., 1990, “Temporal and Modal Logics”, inJ. van Leeuwen (ed.),Handbook of Theoretical ComputerScience (Volume B: Formal Models and Semantics), Amsterdam:Elsevier, pp. 995–1072.
Emerson, E.A., and E.C. Clarke, 1982, “Using Branching TimeTemporal Logic to Synthesise Synchronisation Skeletons”,Science of Computer Programming, 2: 241–266.
Emerson, E.A., and J. Halpern, 1985, “Decision Proceduresand Expressiveness in the Temporal Logic of Branching Time”,Journal of Computer and Systems Science, 30: 1–24.
Emerson, E.A., and A. Sistla, 1984, “Deciding Full BranchingTime Logic”,Information and Control, 61:175–201.
Euzenat, J., and A. Montanari, 2005, “TimeGranularity”, in Fisher et al. (2005), pp. 59–118.
Ewald, W., 1986, “Intuitionistic Tense and ModalLogic”,Journal of Symbolic Logic, 51(1):166–179.
Fagin, R., J. Halpern, Y. Moses, and M. Vardi, 1995,Reasoningabout Knowledge, Boston: MIT Press.
Finger, M., and D.M. Gabbay, 1992, “Adding a TemporalDimension to a Logic System”,Journal of Logic, Language andInformation, 1(3): 203–233.
–––, 1996, “Combining Temporal LogicSystems”,Notre Dame Journal of Formal Logic, 37(2):204–232.
Finger, M., D.M. Gabbay, and M. Reynolds, 2002, “AdvancedTense Logic”, in Gabbay and Guenthner (2002), pp.43–204.
Fisher, M., 2008, “Temporal Representation andReasoning”, in F. van Harmelen, V. Lifschitz, and B. Porter(eds.),Handbook of Knowledge Representation, Amsterdam:Elsevier, pp. 513–550.
–––, 2011,An Introduction to PracticalFormal Methods Using Temporal Logic, New York: Wiley.
Fisher, M., D.M. Gabbay, and L. Vila, 2005,Handbook ofTemporal Reasoning in Artificial Intelligence, Amsterdam:Elsevier.
Fisher, M., and M. Wooldridge, 2005, “Temporal Reasoning inAgent-Based Systems”, in Fisher et al. (2005), pp.469–495.
Fitting, M., and R. Mendelsohn, 2023,First-Order ModalLogic (Second edition), Springer.
French, T., 2001, “Decidability of Quantified PropositionalBranching Time Logics”,Advances in AI (Lecture Notesin Computer Science: Volume 2256), Berlin: Springer, pp.165–176.
French, T., and M. Reynolds, 2003, “A Sound and CompleteProof System for QPTL”, in Balbiani et al. (eds.),Advancesin Modal Logic (Volume 4), London: College Publication, pp.127–148.
Fritz, P., 2024 (forthcoming), PropositionalQuantifiers, Cambridge Elements in Philosophy and Logic,Cambridge: Cambridge University Press.

Gabbay, D.M., and F. Guenthner (eds.), 2002,Handbook ofPhilosophical Logic (Volume 7), Second Edition, Dordrecht:Kluwer.
Gabbay, D.M., I. Hodkinson, and M. Reynolds, 1994,TemporalLogic: Mathematical Foundations and Computational Aspects (Volume1), Oxford: Clarendon Press.
Gabbay, D., A. Kurucz, F. Wolter, and M. Zakharyaschev, 2003,Many-Dimensional Modal Logics: Theory and Applications,Amsterdam: Elsevier.
Gabbay, D.M., A. Pnueli, S. Shelah, and J. Stavi, 1980, “Onthe Temporal Basis of Fairness”, inProceedings of the 7thACM SIGPLAN-SIGACT Symposium on Principles of ProgrammingLanguages, pp. 163–173.
Gabbay, D.M., M. Reynolds, and M. Finger, 2000,TemporalLogic: Mathematical Foundations and Computational Aspects (Volume2), Oxford: Oxford University Press.
Gabbay, D.M., D. Skvortsov, and V. Shehtman, 2009,Quantification in Nonclassical Logic (Studies in Logic and theFoundations of Mathematics, Volume 153), Elsevier.
Gabelaia, D., R. Kontchakov, A. Kurucz, F. Wolter, and M.Zakharyaschev, 2005, “Combining Spatial and Temporal Logics:Expressiveness vs. Complexity”,Journal of ArtificialIntelligence Research, 23: 167–243.
Galton, A.P., 1984,The Logic of Aspect, Oxford:Clarendon Press.
–––, 1987,Temporal Logics and theirApplications, London: Academic Press.
–––, 1990, “A Critical Examination ofAllen’s Theory of Action and Time”,ArtificialIntelligence, 42: 159–188.
–––, 1995, “Time and Change for AI”,in D.M. Gabbay, C.J. Hogger, and J.A. Robinson,Handbook of Logicin Artificial Intelligence and Logic Programming (Volume 4),Oxford: Clarendon Press, pp. 175–240.
–––, 1996, “Time and Continuity inPhilosophy, Mathematics, and Artificial Intelligence”,Kodikas/Code, 19 (1–2): 101–119.
–––, 2005, “Eventualities”, inFisher et al. (2005), pp. 25–58.
–––, 2008, “Temporal Logic”, in E.N.Zalta (ed.),The Stanford Encyclopedia of Philosophy (Fall2008 Edition), URL = <https://plato.stanford.edu/archives/fall2008/entries/logic-temporal/>.
Gargov, G., and V. Goranko, 1993, “Modal Logic withNames”,Journal of Philosophical Logic, 22:607–636.
Garson, J., 1984, “Quantification in Modal Logic”, inD.M. Gabbay, and F. Guenthner (eds.),Handbook of PhilosophicalLogic, Dordrecht: Reidel, pp. 249–307.
Goldblatt, R., 1980, “Diodorean Modality in MinkowskiSpacetime”,Studia Logica, 39: 219–236.[Reprinted inMathematics of Modality (CSLI Lecture Notes43), Stanford: CSLI Publications, 1993.]
–––, 1992,Logics of Time andComputation (CSLI Lecture Notes 7), Second Edition, Stanford:CSLI Publications.
Goranko, V., 1996, “Hierarchies of Modal and Temporal Logicswith Reference Pointers”,Journal of Logic, Language andInformation, 5(1): 1–24.
–––, 2023, Temporal Logics, CambridgeElements in Philosophy and Logic, Cambridge: Cambridge UniversityPress.
Goranko, V., and G. van Drimmelen, 2006, “CompleteAxiomatization and Decidablity of the Alternating-Time TemporalLogic”,Theoretical Computer Science, 353:93–117.
Goranko, V., A. Montanari, and G. Sciavicco, 2003,“Propositional Interval Neighborhood Logics”,Journalof Universal Computer Science, 9(9): 1137–1167.
–––, 2004, “A Road Map of PropositionalInterval Temporal Logics and Duration Calculi”,Journal ofApplied Non-Classical Logics (Special Issue on Interval TemporalLogics and Duration Calculi), 14(1–2): 11–56.
Goranko, V., and D. Shkatov, 2010, “Tableau-Based DecisionProcedures for Logics of Strategic Ability in Multi-AgentSystems”,ACM Transactions of Computational Logic,11(1): 3–51.
Goré, R., 1999, “Tableau Methods for Modal andTemporal Logics”, in M. D’Agostino, D.M. Gabbay, R.Hahnle, and J. Posegga (eds.),Handbook of Tableau Methods,Dordrecht: Kluwer, pp. 297–396.
Grädel, E., and M. Otto, 1999, “On Logics With TwoVariables”,Theoretical Computer Science,224(1–2), pp. 73–113.
Gurevich, Y., and S. Shelah, 1985a, “The Decision Problemfor Branching Time Logic”,Journal of Symbolic Logic,50: 668–681.
–––, 1985b, “To the Decision Problem forBranching Time Logic”, in P. Weingartner, and G. Dold (eds.),Foundations of Logic and Linguistics: Problems and theirSolutions, Plenum, pp. 181–198.
Halpern, J., and Y. Shoham, 1986. “A Propositional ModalLogic of Time Intervals”, inProceedings of the 2nd IEEESymposium on Logic in Computer Science, pp. 279–292.[Reprinted inJournal of the ACM, 38(4): 935–962,1991.]
Halpern, J., and M. Vardi, 1989, “The Complexity ofReasoning about Knowledge and Time I: Lower Bounds”,Journalof Computer and System Sciences, 38(1): 195–237.
Hamblin, C.L., 1972, “Instants and Intervals”, in J.T.Fraser, F. Haber, and G. Müller (eds.),The Study ofTime, Berlin/Heidelberg: Springer, pp. 324–331.
Hansen, M.R., and C. Zhou, 1997, “Duration Calculus: LogicalFoundations”,Formal Aspects of Computing, 9:283–330.
Hart, S., and M. Sharir, 1986, “Probabilistic PropositionalTemporal Logics”,Information and Control,70(2–3): 97–155.
Hasle, P., P. Blackburn, and P. Øhrstrøm (eds.),2017,Logic and Philosophy of Time: Themes from Prior (Volume1), Aalborg: Aalborg University Press.
Hasle, P., D. Jakobsen, and P. Øhrstrøm (eds.),2020,Logic and Philosophy of Time: The Metaphysics of Time(Volume 4), Aalborg: Aalborg University Press.
Hodkinson, I., and M. Reynolds, 2007, “TemporalLogic”, in Blackburn et al. (2007), pp. 655–720.
Hodkinson, I., F. Wolter, and M. Zakharyaschev, 2000,“Decidable Fragments of First-Order Temporal Logics”,Annals of Pure and Applied Logic, 106(1–3):85–134.
–––, 2001, “Monodic Fragments ofFirst-Order Temporal Logics: 2000-2001 A.D.”, inLogic forProgramming, Artificial Intelligence, and Reasoning, Proceedingsof the 8th International Conference LPAR 2001, Springer, pp.1–23.
–––, 2002, “Decidable and UndecidableFragments of First-Order Branching Temporal Logics”, inProceedings of the 17th Annual IEEE Symposium on Logic in ComputerScience, IEEE Computer Society Press, pp. 393–402.
Humberstone, I.L., 1979, “Interval Semantics for TenseLogic: Some Remarks”,Journal of Philosophical Logic,8: 171–196.
Ingthorsson, R.D., 2016,McTaggart’s Paradox, NewYork: Routledge.
Jakobsen, D., P. Øhrstrøm, M. Prior, and A. Rini(eds.), 2020,Logic and Philosophy of Time: Three Little Essays.Arthur Prior in 1931 (Volume 3), Aalborg: Aalborg UniversityPress.
Kamide, N., and H. Wansing, 2010, “Combining Linear-TimeTemporal Logic with Constructiveness and Paraconsistency”,Journal of Applied Logic, 6: 33–61.
–––, 2011, “A Paraconsistent Linear-TimeTemporal Logic”,Fundamenta Informaticae, 106:1–23.
Kamp, J., 1968,Tense Logic and the Theory of LinearOrder, PhD Thesis, University of California, Los Angeles.
–––, 1971, “Formal Properties of‘Now’”,Theoria, 37: 227–273.
–––, 1979, “Events, Instants and TemporalReference”, in R. Bäuerle, U. Egli, and A. von Stechow(eds.),Semantics from Different Points of View, Berlin:Springer, pp. 376–417.
Kesten, Y., and A. Pnueli, 2002, “Complete Proof System forQPTL”.Journal of Logic and Computation, 12(5):701–745.
Kofod, J., 2020, “Arthur Prior’s Early Thoughts onPhysics and Cosmology”, in Jakobsen et al. (2020), pp.73–97.
Kontchakov, R., A. Kurucz, F. Wolter, and M. Zakharyaschev, 2007,“Spatial Logic + Temporal Logic = ?”, in M. Aiello, J. vanBenthem, and I. Pratt-Hartmann (eds.),Handbook of SpatialLogics, Berlin: Springer, pp. 497–564.
Kontchakov, R., C. Lutz, F. Wolter, and M. Zakharyaschev, 2004,“Temporalising Tableaux”,Studia Logica, 76(1):91–134.
Konur, S., 2013, “A Survey on Temporal Logics for Specifyingand Verifying Real-Time Systems”,Frontiers of ComputerScience, 7(3): 370–403.
Koymans, R., 1990, “Specifying Real-Time Properties withMetric Temporal Logic”,Real-Time Systems, 2(4):55–299.
Kowalski, R.A., and M.J. Sergot, 1986, “A Logic-BasedCalculus of Events”,New Generation Computing, 4:67–95.
Kröger, F., and S. Merz, 2008,Temporal Logic and StateSystems (EATCS Texts in Theoretical Computer Science Series),Berlin: Springer.
Kuhn, S.T., and P. Portner, 2002, “Tense and Time”, inGabbay and Guenthner (2002), pp. 277–346.
Ladkin, P., 1987,The Logic of Time Representation, PhDThesis, University of California, Berkeley.
van Lambalgen, M., and F. Hamm, 2005,The Proper Treatment ofEvents, Malden: Blackwell.
Lamport, L., 1994, “The Temporal Logic of Actions”,ACM Transactions on Programming Languages and Systems, 16(3):872–923.
Lindström, S., and K. Segerberg, 2007, “Modal Logic andPhilosophy”, in Blackburn et al. (2007), pp.1149–1214
Linsky, B., and E. Zalta, 1994, “In Defense of the SimplestQuantified Modal Logic”,Philosophical Perspectives, 8:431–458.
Lorini, E., 2013, “Temporal STIT Logic and Its Applicationto Normative Reasoning”,Journal of Applied Non-ClassicalLogics, 23(4): 372–399.
Lutz, K., F. Wolter, and M. Zakharyaschev, 2008, “TemporalDescription Logics: A Survey”,Proceedings of TIME2008, pp. 3–14.
Ma, J., and B. Knight, 2001, “Reified Temporal Logics: AnOverview”,Artificial Intelligence Review, 15(3):189–217.
MacFarlane, J., 2003, “Future Contingents and RelativeTruth”,The Philosophical Quarterly, 53(212):321–336.
–––, 2014,Assessment Sensitivity: RelativeTruth and Its Applications, Oxford: Oxford University Press.
Manna, Z., and A. Pnueli, 1992,The Temporal Logic of Reactiveand Concurrent Systems (Specification: Volume 1), Springer: NewYork.
Mani, I., J. Pustejovsky, and R. Gaizauskas, 2005,TheLanguage of Time: A Reader, Oxford: Oxford University Press.
Marx, M., and M. Reynolds, 1999, “Undecidability of CompassLogic”,Journal of Logic and Computation, 9(6):897–914.
McArthur, R., 1976,Tense Logic, Synthese Library,Springer.
McCarthy, J., and P.J. Hayes, 1969, “Some PhilosophicalProblems from the Standpoint of Artificial Intelligence”, in D.Michie, and B. Meltzer (eds.),Machine Intelligence 4,Edinburgh: Edinburgh University Press, pp. 463–502.
McDermott, D., 1982, “A Temporal Logic for Reasoning aboutProcesses and Plans”,Cognitive Science, 6:101–155.
McTaggart, E.J., 1908, “The Unreality of Time”,Mind, 17(68): 457–472.
Merz, S., 1992, “Decidability and Incompleteness Results forFirst-Order Temporal Logics of Linear Time”,Journal ofApplied Non-Classical Logic, 2(2): 139–156.
ter Meulen, A., 2005, “Temporal Reasoning in NaturalLanguage”, in Fisher et al. (2005), pp. 559–585.
Meyer, U., 2013,The Nature of Time, Oxford: OxfordUniversity Press.
Montanari, A., 1996,Metric and Layered Temporal Logic forTime Granularity, PhD Thesis (Institute for Logic, Language, andComputation Dissertation Series, Volume: 1996–02), University ofAmsterdam.
Montanari, A., and A. Policriti, 1996, “Decidability Resultsfor Metric and Layered Temporal Logics”,Notre Dame JournalFormal Logic, 37(2): 260–282.
Moss, S.L., and H.J. Tiede, 2007, “Applications of ModalLogic in Linguistics”, in Blackburn et al. (2007), pp.1003–1076.
Moszkowski, B., 1983,Reasoning about Digital Circuits,PhD Thesis (Technical Report STAN-CS-83–970), Department ofComputer Science, Stanford University.
Müller, T., 2011, “Tense or Temporal Logic”, inR. Pettigrew (ed.),The Continuum Companion to PhilosophicalLogic, London: Continuum, pp. 324–350.
––– (ed.), 2014,Nuel Belnap onIndeterminism and Free Action (Outstanding Contributions toLogic: Volume 2), Springer.
Nishimura, H., 1979, “Is the Semantics of BranchingStructures Adequate for Non-Metric Ockhamist Tense Logics?”,Journal of Philosophical Logic, 8: 477–478.
Ogihara, T., 2007, “Tense and Aspect in Truth-ConditionalSemantics”,Lingua, 117:392–418.
–––, 2011, “Tense”, in C. Maienborn,K. von Heusinger, and P. Portner (eds.),Semantics: AnInternational Handbook of Natural Language Meaning, de Gruyter,pp. 1463–1484.
Øhrstrøm, P., 2009, “In Defense of the ThinRed Line: A Case for Ockhamism”,Humana Mente, 8:17–32.
–––, 2019, “A Critical Discussion ofPrior’s Philosophical and Tense-Logical Analysis of the Ideas ofIndeterminism and Human Freedom”,Synthese, 196(1):69–85.
Øhrstrøm, P., and M. Gonzalez, 2022,“Prior’s Big Y and the Idea of Branching Time”,History and Philosophy of Logic, online first.
Øhrstrøm, P., and P. Hasle, 1995,TemporalLogic: From Ancient Ideas to Artificial Intelligence, Dordrecht:Kluwer Academic Publishers.
–––, 2006, “Modern Temporal Logic: ThePhilosophical Background”, inHandbook of the History ofLogic (Volume 7), pp. 447–498.
–––, 2019, “The Significance of theContributions of A.N. Prior and Jerzy Łoś in the EarlyHistory of Modern Temporal Logic”, in Blackburn et al. (2019),pp. 31–40.

Pani, A.K., and G.P. Bhattacharjee, 2001, “TemporalRepresentation and Reasoning in Artificial Intelligence: AReview”,Mathematical and Computer Modelling, 34:55–80.
Parsons, T., 1990,Events in the Semantics of English: A Studyin Subatomic Semantics, Cambridge: MIT Press.
Partee, B., 1973, “Some Structural Analogies between Tensesand Pronouns in English”,The Journal of Philosophy,70(18): 601–609.
Passy, S., and T. Tinchev, 1985. “Quantifiers in CombinatoryPDL: Completeness, Definability, Incompleteness”, inFundamentals of Computation Theory FCT 85 (Lecture Notes inComputer Science: Volume 199), Berlin: Springer, pp.512–519.
Pinto, J., and R. Reiter, 1995, “Reasoning about Time in theSituation Calculus”,Annals of Mathematics and ArtificialIntelligence, 14(2–4): 251–268.
Ploug, T., and P. Øhrstrøm, 2012, “BranchingTime, Indeterminism, and Tense Logic: Unveiling the Prior-KripkeLetters”,Synthese, 188(3): 367–379.
Pnueli, A., 1977, “The Temporal Logic of Programs”,Proceedings of the 18th IEEE Symposium on Foundations of ComputerScience, pp. 46–67.
Prior, A.N., 1957,Time and Modality, Oxford: OxfordUniversity Press.
–––, 1959, “Thank Goodness that’sover”,Philosophy, 34(128): 12–17.
–––, 1967,Past, Present and Future,Oxford: Oxford University Press.
–––, 1968,Papers on Time and Tense,Oxford: Oxford University Press. [New edition: P. Hasle et al. (eds.),Oxford: Oxford University Press, 2003.]
–––, 1968, “‘Now’”,Noûs, 2(2): 101–119.
Reichenbach, H., 1947,Elements of Symbolic Logic, NewYork: Macmillan.
Reichgelt H., and L. Vila, 2005, “Temporal Qualification inArtificial Intelligence”, in Fisher et al. (2005), pp.167–194.
Rescher, N., and A. Urquhart, 1971,Temporal Logic,Berlin: Springer.
Reynolds, M., 1994, “Axiomatizing U and S over IntegerTime”, in D.M. Gabbay, and H.J. Ohlbach (eds.),TemporalLogic, Proceedings of the First International Conference ICTL1994 (Lecture Notes in Artificial Intelligence: Volume 828),Berlin/Heidelberg: Springer, pp. 117–132.
–––, 1996, “Axiomatising First-OrderTemporal Logic: Until and Since over Linear Time”,StudiaLogica, 57(2–3): 279–302.
–––, 2001, “An Axiomatization of FullComputation Tree Logic”,Journal of Symbolic Logic, 66:1011–1057.
–––, 2002, “Axioms for BranchingTime”.Journal of Logic and Computation, 12(4):679–697.
–––, 2003, “An Axiomatization ofPrior’s Ockhamist Logic of Historical Necessity”, inBalbiani et al. (eds.),Advances in Modal Logic (Volume 4),London: College Publications, pp. 355–370.
–––, 2005, “An Axiomatization ofPCTL*”,Information and Computation, 201(1):72–119.
–––, 2007, “A Tableau for BundledCTL”,Journal of Logic and Computation, 17(1):117–132.
–––, 2010, “The Complexity of TemporalLogic over the Reals”,Annals of Pure and AppliedLogic, 161(8): 1063–1096.
–––, 2011, “A Tableau-Based DecisionProcedure for CTL*”,Formal Aspects of Computing,23(6): 739–779.
–––, 2014, “A Tableau for Temporal Logicover the Reals”, in Goré et al. (eds.),Advances inModal Logic (Volume 10), London: College Publications, pp.439–458.
Röper, P., 1980, “Intervals and Tenses”,Journal of Philosophical Logic, 9: 451–469.
Rumberg, A., 2016, “Transition Semantics for BranchingTime”,Journal of Logic, Language and Information,25(1): 77–108.
–––, 2019, “Actuality and Possibility inBranching Time: The Roots of Transition Semantics”, in Blackburnet al. (2019), pp. 145–161.
Rumberg, A., and A. Zanardo, 2019, “First-Order Definabilityof Transition Structures”,Journal of Logic, Language andInformation, 28(3): 459–488.
Segerberg, K., 1970, “Modal Logics with Linear AlternativeRelations”,Theoria, 36: 301–322.
–––, 1992, “Getting Started: Beginnings inthe Logic of Action”,Studia Logica, 51:347–378.
Shoham, Y., 1987, “Temporal Logic in AI: Semantical andOntological Considerations”,Artificial Intelligence,33: 89–104.
Steedman, M., 1997, “Temporality”, in J. van Benthem,and A. ter Meulen (eds.),Handbook of Logic and Language,Amsterdam: Elsevier, pp. 925–969.
Stirling, C., 1992, “Modal and Temporal Logics”, inHandbook of Logic in Computer Science (ComputationalStructures: Volume 2), Oxford, Clarendon Press, pp.477–563.
Thomason, R.H., 1970, “Indeterminist Time and Truth-ValueGaps”,Theoria, 36(3): 264–281.
–––, 1984, “Combinations of Tense andModality”, in D.M. Gabbay, and F. Guenther (eds.),Handbookof Philosophical Logic (Extensions of Classical Logic: Volume 2),Dordrecht: Reidel, pp. 135–165. [New edition in Gabbay andGuenthner (2002), pp. 205–234.]
Tkaczyk, M., and T. Jarmużek, 2019, “JerzyŁoś Positional Calculus and the Origin of TemporalLogic”,Logic and Logical Philosophy, (28):259–276.
Uckelman, S.L., and J. Uckelman, 2007, “Modal and TemporalLogics for Abstract Space-Time Structures”, inStudies inHistory and Philosophy of Science (Part B: Studies in History andPhilosophy of Modern Physics), 38(3): 673–681.
Vardi, M., 2007, “Automata-Theoretic Techniques for TemporalReasoning”, in Blackburn et al. (2007), pp. 971–989.
Vardi, M., and P. Wolper, 1994, “Reasoning about InfiniteComputations”,Information and Computation, 115:1–37.
Venema, Y., 1990, “Expressiveness and Completeness of anInterval Tense Logic”,Notre Dame Journal of FormalLogic, 31: 529–547.
–––, 1991, “A Modal Logic for ChoppingIntervals”,Journal of Logic and Computation, 1(4):453–476.
–––, 1993, “Completeness via Completeness:Since and Until”, in M. de Rijke (ed.),Diamonds andDefaults, Dordrecht: Kluwer, pp. 279–286.
–––, 2001, “Temporal Logic”, in L.Goble (ed.),Blackwell Guide to Philosophical Logic, Oxford:Blackwell Publishers.
Vila, L., 1994, “A Survey on Temporal Reasoning inArtificial Intelligence”,AI Communications, 7:4–28.
–––, 2005, “Formal Theories of Time andTemporal Incidence”, in Fisher et al. (2005), pp.1–24.
Wölfl, S., 1999, “Combinations of Tense and Modalityfor Predicate Logic”,Journal of Philosophical Logic,28: 371–398.
Wolper, P., 1985, “The Tableau Method for Temporal Logic: AnOverview”,Logique et Analyse, 28(110–111):119–136.
Wolter F., and M. Zakharyaschev, 2000, “TemporalizingDescription Logics”, in D.M. Gabbay, and M. de Rijke (eds.),Frontiers of Combining Systems II, New York: Wiley, pp.379–401.
–––, 2002, “Axiomatizing the MonodicFragment of First-Order Temporal Logic”,Annals of Pure andApplied Logic, 118(1–2): 133–145.
Xu, M., 1988, “On some U,S-Tense Logics”,Journalof Philosophical Logic, 17: 181–202.
Zanardo, A., 1985, “A Finite Axiomatization of the Set ofStrongly Valid Ockhamist Formulas”,Journal of PhilosophicalLogic, 14: 447–468.
–––, 1990, “Axiomatization of‘Peircean’ Branching-Time Logic”,StudiaLogica, 49: 183–195.
–––, 1991, “A Complete Deductive Systemfor Since-Until Branching Time Logic”,Journal ofPhilosophical Logic, 20: 131–148.
–––, 1996, “Branching-Time Logic withQuantification over Branches: The Point of View of Modal Logic”,Journal of Symbolic Logic, 61: 1–39.
–––, 1998, “Undivided andIndistinguishable Histories in Branching-Time Logics”,Journal of Logic, Language and Information, 7(3):297–315.
Zanardo, A., B. Barcellan, and M. Reynolds, 1999,“Non-Definability of the Class of Complete Bundled Trees”,Logic Journal of the IGPL (Special Issue on Temporal Logic),7(1): 125–136.

Academic Tools

How to cite this entry.
Preview the PDF version of this entry at theFriends of the SEP Society.
Look up topics and thinkers related to this entry at the Internet Philosophy Ontology Project (InPhO).
Enhanced bibliography for this entryatPhilPapers, with links to its database.

Other Internet Resources

Acknowledgments

The first version of this entry was written by Antony Galton in 1999,later revised in Galton (2008). In 2015 the entry was substantiallyre-written and extended by Valentin Goranko. The 2020 versionconstitutes a major revision and further extension of the 2015version, with Antje Rumberg as a new co-author, and builds the basisof the present version. We acknowledge Galton’s contribution tothe previous versions, and we are grateful to Johan van Benthem,Patrick Blackburn, Rob Goldblatt, Angelo Montanari, Yde Venema,Michael Zakharyaschev, Ed Zalta, Alberto Zanardo, as well as someattentive readers for helpful comments and suggestions on earlierversions.

Open access to the SEP is made possible by a world-wide funding initiative.
The Encyclopedia Now Needs Your Support
Please Read How You Can Help Keep the Encyclopedia Free

Browse

About

Support SEP

Mirror Sites

View this site from another server:

USA (Main Site)Philosophy, Stanford University

Info about mirror sites

Library of Congress Catalog Data: ISSN 1095-5054

	How to cite this entry.
	Preview the PDF version of this entry at theFriends of the SEP Society.
	Look up topics and thinkers related to this entry at the Internet Philosophy Ontology Project (InPhO).
	Enhanced bibliography for this entryatPhilPapers, with links to its database.

Movatterモバイル変換