| Pp | ≡ | Sp(p ¬p) |
| Fp | ≡ | Up(p¬p) |
version history
|
Stanford Encyclopedia of PhilosophyA | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z
|
last substantive content
change
|
Applications of Temporal Logic include its use as a formalism for clarifying philosophical issues about time, as a framework within which to define the semantics of temporal expressions in natural language, as a language for encoding temporal knowledge in artificial intelligence, and as a tool for handling the temporal aspects of the execution of computer programs.
The logical language of Tense Logic contains, in addition to the usual truth-functional operators, four modal operators with intended meanings as follows:
P "It has at some time been the case that …" F "It will at some time be the case that …" H "It has always been the case that …" G "It will always be the case that …"
P and F are known as the weak tense operators, while H and G are known as the strong tense operators. The two pairs are generally regarded as interdefinable by way of the equivalences
Pp ≡ ¬H¬p Fp ≡ ¬G¬p
On the basis of these intended meanings, Prior used the operators to build formulae expressing various philosophical theses about time, which might be taken as axioms of a formal system if so desired. Some examples of such formulae, with Prior's own glosses (from Prior 1967), are:
Gp→Fp "What will always be, will be" G(p→q)→(Gp→Gq) "If p will always imply q, then if p will always be the case, so will q" Fp→FFp "If it will be the case that p, it will be — in between — that it will be" ¬Fp→F¬Fp "If it will never be that p then it will be that it will never be that p"
Prior (1967) reports on the extensive early work on various systems of Tense Logic obtained by postulating different combination of axioms, and in particular he considered in some detail what light a logical treatment of time can throw on classic problems concerning time, necessity and existence; for example, "deterministic" arguments that have been advanced over the ages to the effect that "what will be, will necessarily be", corresponding to the modal tense-logical formula Fp→□Fp.
Of particular significance is the system of Minimal Tense Logic Kt, which is generated by the four axioms
together with the two rules of temporal inference:
p→HFp "What is, has always been going to be" p→GPp "What is, will always have been" H(p→q)→(Hp→Hq) "Whatever always follows from what always has been, always has been" G(p→q)→(Gp→Gq) "Whatever always follows from what always will be, always will be"
and, of course, all the rules of ordinary Propositional Logic. The theorems of Kt express, essentially, those properties of the tense operators which do not depend on any specific assumptions about the temporal order. This characterisation is made more precise below.
RH: From a proof of p, derive a proof of Hp RG: From a proof of p, derive a proof of Gp
Tense Logic is obtained by adding the tense operators to an existing logic; above this was tacitly assumed to be the classical Propositional Calculus. Other tense-logical systems are obtained by taking different logical bases. Of obvious interest is tensed predicate logic, where the tense operators are added to classical First-order Predicate Calculus. This enables us to express important distinctions concerning the logic of time and existence. For example, the statement A philosopher will be a king can be interpreted in several different ways, such as
The interpretation of such formulae is not unproblematic, however. The problem concerns the domain of quantification. For the second two formulae above to bear the interpretations given to them, it is necessary that the domain of quantification is always relative to a time: thus in the semantics it will be necessary to introduce a domain of quantification D(t) for each time t. But this can lead to problems if we want to establish relations between objects existing at different times, as for example in the statement "One of my friends is descended from a follower of William the Conqueror".
∃x(Philosopher(x) & F King(x)) Someone who is now a philosopher will be a king at some future time ∃xF(Philosopher(x) & King(x)) There now exists someone who will at some future time be both a philosopher and a king F∃x(Philosopher(x) & F King(x)) There will exist someone who is a philosopher and later will be a king F∃x(Philosopher(x) & King(x)) There will exist someone who is at the same time both a philosopher and a king
These problems are related to the so-called Barcan formulae of modal logic, a temporal analogue of which is
F∃xp(x)→∃xFp(x) ("If there will be something that is p, then there is now something that will be p")
For this formula to be true, we require the "domain cumulation" principle, which says that the whole domain of quantification D(t) at time t is included in all the domains D(t′) for times t′ later than t. For more on this and related matters, see van Benthem, 1995, Section 7.
The binary temporal operators S and U ("since" and "until"). These were introduced by Kamp (1968). The intended meanings are
It is possible to define the one-place tense operators in terms of S and U as follows:
Spq "q has been true since a time when p was true" Upq "q will be true until a time when p is true"
Pp ≡ Sp(p Fp ≡ Up(p
The importance of the S and U operators is that they are expressively complete with respect to first-order temporal properties on continuous, strictly linear temporal orders (which is not true for the one-place operators on their own).
Metric tense logic. Prior introduced the notation Fnp to mean "It will be the case the interval n hence that p". We do not need a separate notation Pnp since we can write F(-n)p for "It was the case the interval n ago that P". The case n=0 gives us the present tense. We can define the general, non-metric operators by
Pp ≡ ∃n(n<0 & Fnp) Fp ≡ ∃n(n>0 & Fnp) Hp ≡ ∀n(n<0→Fnp) Gp ≡ ∀n(n>0→Fnp)
The "next time" operator O. This operator assumes that the time series consists of a discrete sequence of atomic times. The formula Op is then intended to mean that p is true at the immediately succeeding time step. Given that time is discrete, it can be defined in terms of the "until" operator U by
Op ≡ Up(p&¬p)
which says that p will be true at some future time, between which and the present time nothing is true. This can only mean the time immediately following the present in a discrete temporal order.
In discrete time, the future-tense operator F is related to the next-time operator by the equivalence
Fp ≡ OpIndeed, F can here be defined as the least fixed point of the transformation which maps an arbitrary propositional operator X onto the operator λp.Op
OXp.
One could similarly define a past-time version of O; but since the main usefulness of this particular operator has been in relation to the logic of computer programming, where one is mainly interested in execution sequences of programs extending into the future, this has not so often been done.
from which it follows that the meanings of the strong operators are given by
Pp is true at t if and only if p is true at some time t′ such that t′<t Fp is true at t if and only if p is true at some time t′ such that t<t′
Hp is true at t if and only if p is true at all times t′ such that t′<t Gp is true at t if and only if p is true at all times t′ such that t<t′
We can now provide a precise characterisation of system Kt of Minimal Tense Logic. The theorems of Kt are precisely those formulae which are true at all times under all interpretations over all temporal frames.
Many tense-logical axioms have been suggested as expressing this or that property of the flow of time, and the semantics gives us a precise way of defining this correspondence between tense-logical formulae and properties of temporal frames. A formula p is said to characterise a set of frames F if
A first-order formula in < determines a class of frames, namely those in which the formula is true. A tense-logical formula p corresponds to a first-order formula q just so long as p characterises the class of frames for which q is true. Some well-known examples of such pairs of formulae are:
However, there are tense-logical formulae (such as GFp→FGp) which do not correspond to any first-order temporal frame properties, and there are first-order temporal frame properties (such as irreflexivity, expressed by ∀t¬(t<t)) which do not correspond to any tense-logical formula. For details, see van Benthem (1983).
Hp→Pp ∀t∃t′(t′<t) (unbounded in the past) Gp→Fp ∀t∃t′(t<t′) (unbounded in the future) Fp→FFp ∀t,t′(t<t′ → ∃t″(t<t″<t′)) (dense ordering) FFp→Fp ∀t,t′(∃t″(t<t″<t′) → t<t′) (transitive ordering) FPp → Pp ∀t,t′,t″((t<t″ & t′<t″) → (t<t′ (linear in the past) PFp → Pp ∀t,t′,t″((t″<t & t″<t′) → (t<t′ (linear in the future)
Kill(Brutus,Caesar,44BC).If we introduce into the first-order language a binary infix predicate < denoting the temporal ordering relation "earlier than", and a constant "now" denoting the present moment, then the tense operators can be readily simulated by means of the following correspondences, which not surprisingly bear more than a passing resemblance to the formal semantics for Tense Logic given above. Where p(t) represents the result of introducing an extra temporal argument place to the time-variable predicates occurring in p, we have:
Before the advent of Tense Logic, the method of temporal arguments was the natural choice of formalism for the logical expression of temporal information.
Pp ∃t(t<now & p(t)) Fp ∃t(now<t & p(t)) Gp ∀t(t<now → p(t)) Hp ∀t(now<t → p(t))
This kind of manoeuvre lies at the heart of hybrid temporal logics in which the standard apparatus of propositions and tense operators is supplemented by propositions which are true at unique instants, thereby effectively naming those instants without invoking philosophically dubious reification. This can give one some of the expressive power of a predicate-logic approach while retaining the modal character of the logic.
The method of state and event-type reification was introduced to cater for distinctions of this kind. It is an approach that has been especially popular in Artificial Intelligence, where it is particularly associated with the name of James Allen, whose influential paper (Allen 1984) is often cited in this connection. In this approach, state and event types are denoted by terms in a first-order theory; their temporal incidence is expressed using relational predicates "Holds" and "Occurs", as for example,
Holds(Asleep(Mary),(1pm,6pm))where terms of the form (t,t′) denote time intervals in the obvious way.
Occurs(Walk-to(John,Station),(1pm,1.15pm))
The homogeneity of states and inhomogeneity of events is secured by axioms such as
∀s,i,i′(Holds(s,i) & In(i′,i) → Holds(s,i′))where "In" expresses the proper subinterval relation.
∀e,i,i′(Occurs(e,i) & In(i′,i) → ¬Occurs(e,i′))
The key idea is that each event-forming predicate is endowed with an extra argument-place to be filled with a variable ranging over event-tokens, that is, particular dated occurrences. The inference above is then cast in logical form as
John saw Mary in London on Tuesday. Therefore, John saw Mary on Tuesday.
In this form, the inference does not require any additional logical apparatus over and above standard first-order predicate logic; on that basis, the validity of the inference is considered to be explained. This approach has also been used in a computational context in the Event Calculus of Kowalski and Sergot (1986).
∃e(See(John,Mary,e) & Place(e,London) & Time(e,Tuesday)), Therefore, ∃e(See(John,Mary,e) & Time(e,Tuesday)).
The rivalry between the modal and first-order approaches to formalising the logic of time reflects an important set of underlying philosophical issues related to the work of McTaggart. This work is especially well-known, in the context of temporal logic, for introducing the distinction between the "A-series" and the "B-series". By the "A-series" is meant, essentially, the characterisation of events as Past, Present, or Future. By contrast, the "B-series" involves their characterisation as relatively "Earlier" or "Later". A-series representations of time inescapably single out some particular moment as present; of course, at different times, different moments are present — a circumstance which, followed to what appeared to be its logical conclusion, led McTaggart to assert that time itself was unreal (see Mellor, 1981). B-series representations have no place for a concept of the present, instead taking the form of a synoptic view of all time and the (timeless) interrelations between its parts.
There is a clear affinity between the A-series and the modal approach and between the B-series and the first-order approach. In the terminology of Massey (1969), adherents of the former approach are called "tensers" while adherents of the latter are called "detensers". This issue is related in turn to the question of how seriously to take the representation of space-time as a single four-dimensional entity in which the four dimensions are at least in some respects on a similar footing. In view of the Theory of Relativity, it can be argued that this issue is not so much a matter for Philosophy as for Physics.
The choice of flow of time can be of philosophical significance. For example, one way of capturing the distinction between deterministic and non-deterministic theories is to model the former using a strictly linear flow of time, and the latter with a temporal structure which allows branching into the future. If we adopt the latter approach, then it is helpful in describing the semantics of tense and other operators to introduce the idea of a history, which is a maximal linearly-ordered set of instants. The branching future model will then stipulate that for any two histories there is an instant such that both histories share all the times up to and including that instant, but do not share any times after it. For each history containing a given instant, the times in that history which are later than the instant constitute a "possible future" for that instant.
In branching time semantics it is natural to evaluate formulae with respect to an instant and a history, rather than just an instant. With respect to the pair (h,t), we might interpret "Fp" to be true so long as "p" is true at some time in the future of t as determined by the history h. A separate operator ◊ can be introduced to allow, in effect, quantification over histories: "◊p" is true at (h,t) so long as there is some history h’ such that "p" is true at (h’,t). Then "◊Fp" says that "p" holds in some possible future, and "□Fp" (where "□" is the strong modal operator dual to "◊") says that "p" is inevitable (i.e., holds in all possible futures). Prior calls this kind of interpretation "Ockhamist".
Another interpretation (called "Peircean" by Prior) takes "Fp" to be equivalent to the Ockhamist "□Fp", i.e., "p" is true at some time in every possible future. Under this interpretation there is no formula equivalent to the Ockhamist "Fp"; hence Peircean tense logic is a proper fragment of Ockhamist tense logic. It was favoured by Prior on the grounds that future contingent propositions really do lack truth value: only if a future-tense proposition is inevitable (all possible futures) or impossible (no possible futures) can we ascribe a truth value to it now.
For Prior's discussion of these issues, see Prior 1967, Chapter VII. Further discussion can be found in Øhrstrøm, P. and Hasle, P., 1995, chapters 2.6 and 3.2.
Prior notes that Reichenbach's analysis is inadequate to account for the full range of tense usage in natural language. Subsequently much work has been done to refine the analysis, not only of tenses but also other temporal expressions in language such as the temporal prepositions and connectives ("before", "after", "since", "during", "until"), using the many varieties of temporal logic. For some examples, see Dowty (1979), Galton (1984), Taylor (1985), Richards et al. (1989).
Much of the work on temporal reasoning in AI has been closely tied up with the notorious frame problem, which arises from the necessity for any automated reasoner to know, or be able to deduce, not only those properties of the world which do change as the result of any event or action, but also those properties which do not change. In everyday life, we normally handle such facts fluently without consciously adverting to them: we take for granted without thinking about it, for example, that the colour of a car does not normally change when one changes gear. The frame problem is concerned with how to formalise the logic of actions and events in such a way that indefinitely many inferences of this kind are made available without our having to encode them all explicitly. A seminal work in this area is McCarthy and Hayes (1969). A useful recent reference for the frame problem is Shanahan, 1997.
Non-determinism is an important issue in computer science applications, and hence much use has been made of branching time models. Two important such systems are CTL (Computation Tree Logic) and a more expressive system CTL*; these correspond very nearly to the Ockhamist and Peircean semantics discussed above.
Further information may be found in Galton (1987), Goldblatt (1987), Kroger (1987), Bolc and Szalas (1995).
| Antony Galton A.P.Galton@exeter.ac.uk |
A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z