7Temporal Logic

7.1Reasoning about time

It is currently raining in Edinburgh. But it wasn’t raining yesterday, and perhaps it won’t rain tomorrow. Let’s introduce some operators to formalize reasoning about the unfolding of events through time.

If we read \(r\) as ‘it is raining’, we will use \(\mathsf {F}\! r\) to express that is will be raining at some point in the future. We use \(\mathsf {P}\! r\) to express that it has been raining at some point in the past. In general:

\(\mathsf {F} A\) is true at a time \(t\) iff \(A\) is true at some time after \(t\).
\(\mathsf {P} A\) is true at a time \(t\) iff \(A\) is true at some time before \(t\).

The operators \(\mathsf {F}\) and \(\mathsf {P}\) can be nested. We can use \(\mathsf {F} \mathsf {P} r\) to express that at some point it will have rained, \(\mathsf {P}\mathsf {F} r\) to say that it was once going to rain, \(\mathsf {P}\mathsf {P} r\) to say that there was a time before which it rained, and \(\mathsf {F}\mathsf {F} r\) to say that there will come a time after which it will rain.

Unlike \(\Box \) and \(\Diamond \), \(\mathsf {F}\) and \(\mathsf {P}\) are not duals of each other: \(\neg \mathsf {P}\! A\) is not equivalent to \(\mathsf {F} \neg A\), and \(\neg \mathsf {F}\! A\) is not equivalent to \(\mathsf {P} \neg A\). But it is useful to have duals of \(\mathsf {F}\) and \(\mathsf {P}\). We therefore introduce two more operators. \(\mathsf {G}\) will be the dual of \(\mathsf {F}\), and \(\mathsf {H}\) the dual of \(\mathsf {P}\).

Intuitively, \(\mathsf {G} A\) means that \(A\) is always going to be the case. (Hence the symbol ‘G’.) If it is not the case that at some point in the future it will not rain (\(\neg \mathsf {F}\neg r\)), then it is always going to be the case that it will rain (\(\mathsf {G} r\)). Similarly, \(\mathsf {H} A\) means that \(A\) has always been the case. If it is not the case that at some point in the past it was not raining (\(\neg \mathsf {P}\neg r\)), then it has always been raining (\(\mathsf {H} r\)).

We can state the truth-conditions of \(\mathsf {G} A\) and \(\mathsf {H} A\) in parallel to the above truth-conditions for \(\mathsf {F} A\) and \(\mathsf {P} A\):

\(\mathsf {G} A\) is true at a time \(t\) iff \(A\) is true at all times after \(t\).
\(\mathsf {H} A\) is true at a time \(t\) iff \(A\) is true at all times before \(t\).

The language of standard propositional logic, extended by the four operators \(\mathsf {F},\mathsf {P},\mathsf {G},\mathsf {H}\) is known as the language of basic temporal logic. We will sometimes call it \(\mathfrak {L}_t\).

7.2Temporal models

A complete scenario for temporal logic needs to tell us what times there are, how they are ordered, and what is going on at each of them. We can represent such a scenario, together with an interpretation of \(\mathfrak {L}_{t}\)’s non-logical vocabulary, by a structure that settles (a) what times there are, (b) which times come before or after which others, and (c) which sentence letters are true at which times. This is enough to determine, for every \(\mathfrak {L}_{t}\)-sentence and every time, whether the sentence is true at that time.

We use ‘\(M, t \models A\)’ as a short-hand notation to express that sentence \(A\) is true at time \(t\) in model \(M\). The following definition formally specifies the truth-value of every \(\mathfrak {L}_T\)-sentence at every time in every model.

Clause (a) says that a sentence letter is true at a time in a model iff the model’s interpretation function specifies that the sentence letter is true at that time. Clauses (b)–(f) say that the truth-functional connectives have their normal truth-table meaning at each time. Clauses (g)–(j) formalize the truth-conditions for temporal sentences from the previous section.

All this should remind you of our Kripke semantics for \(\mathfrak {L}_M\) in chapter 3. In fact, temporal models are Kripke models, as defined here. I have merely relabelled the set ‘\(W\)’ as ‘\(T\)’, and the relation ‘\(R\)’ as ‘\(<\)’. Definition 7.2 resembles definition 3.2 here, except that we have two box-like operators \(\mathsf {G}\) and \(\mathsf {H}\), and two diamond-like operators \(\mathsf {F}\) and \(\mathsf {P}\). The language of basic temporal logic is bi-modal, with forward-looking operators (\(\mathsf {F}\) and \(\mathsf {G}\)) and backward-looking operators (\(\mathsf {P}\) and \(\mathsf {H}\)). Unlike ordinary models for multi-modal languages (definition 5.1), temporal models have only a single accessibility relation. That’s because the accessibility relation for \(\mathsf {P}\) and \(\mathsf {H}\) is definable from the accessibility relation for \(\mathsf {F}\) and \(\mathsf {G}\): a time \(s\) is earlier than a time \(t\) iff \(t\) is later than \(s\).

Let’s look at an example of a temporal model. For the set of times \(T\), we use the set of natural numbers 0,1,2, etc. Let’s say that the precedence relation \(<\) holds between \(t\) and \(s\) iff \(t\) is less than \(s\). So \(0<1\) and \(1 < 25\). (We could just as well have stipulated that \(<\) holds between \(t\) and \(s\) iff \(t\) is greater than \(s\); we would then have \(1<0\) and \(25<1\). In temporal logic, the symbol ‘\(<\)’ means ‘earlier than’, not ‘less than’.) Finally, let’s say that the interpretation function assigns to \(p\) the set of all even numbers.

Let’s call this model \(M\). By definition 7.2, we can figure out the following facts, among others.

• \(M,0 \models p\) (because 0 is even);

• \(M,0 \models \mathsf {F} p\) (because there are even numbers greater than 0);

• \(M,0 \models \mathsf {G}\mathsf {F} p\) (because for every number there is a greater number that is even);

• \(M,0 \models \neg \mathsf {F}\mathsf {G} p\) (because there is no number for which all greater numbers are even).

Real times are, of course, not numbers. When I say that ‘it is raining’ is true now, I don’t mean that the sentence is true at a number. It isn’t obvious what kinds of things times are. Fortunately, this doesn’t matter for us, just as the nature of possible worlds doesn’t matter for the logic of possibility and necessity. As long as the formal structure of the times in a scenario matches the structure of the natural numbers, it does no harm to use numbers as times in a model of the scenario.

The formal structure of time in a temporal model is captured by the relevant frame: the pair \(\langle T,<\rangle \) of the set of times and the precedence relation. Frames in temporal logic are also called flows of time. Different applications of temporal logic often come with different assumptions about the flow of time.

In computer science, for example, the “times” \(T\) are often understood as possible states of a computational process; the precedence relation holds between states \(t\) and \(s\) iff the computation can lead from \(t\) to \(s\). If the computation is indeterministic, so that a given state can have different successors, the relevant flow of time will involve forks towards the future: we can have different “times” \(s\) and \(r\) such that \(t<s\) and \(t<r\) but neither \(s<r\) nor \(r<s\). Here the precedence relation cannot be modelled by the less-than relation on the natural numbers, because the structure of the less-than relation does not include forks.

In other applications, we may be interested in how the weather changes from day to day. Here we might identify the relevant times with days and the precedence relation with the earlier-later relation between days – even though intuitively a day is not a single time, but an interval comprising many times. For this application, the natural numbers might have the right formal structure.

For yet other applications, we may want to assume that time is dense, meaning that whenever \(t < s\) then there is another point of time lying between \(t\) and \(s\). This assumption is common in physics. The natural numbers, by contrast, have a discrete structure. There is no natural number between 2 and 3. For dense models, we could use real or rational numbers (fractions) instead of natural numbers.

If we want to take seriously what physics tells us about time, it is not enough to assume that time is dense. We also need to reconceptualize the set \(T\). According to the theory of special relativity, whether a point in time is earlier or later than another is relative to a spatial frame of reference. An adequate model of relativistic time must therefore include a representation of space. In these spacetime models (or Minkowski models), the set \(T\) consists of spacetime points \(\langle x_1,x_2,x_3,t \rangle \) with three spatial and one temporal coordinate; \((x_1,x_2,x_3,t) < (y_1,y_2,y_3,s)\) holds iff the second point can be reached from the first without travelling faster than the speed of light.

7.3Logics of time

Let’s define the minimal temporal logic K\(_t\) as the set of \(\mathfrak {L}_{t}\)-sentences that are true at all times in all temporal models. Since temporal models are just Kripke models, proof methods for the minimal modal logic K are easily adapted to K\(_{t}\). The main novelty is that the rules for the box and the diamond can be used twice over, once for the forward-looking operators \(\mathsf {F}\) and \(\mathsf {G}\), and once for the backward-looking \(\mathsf {P}\) and \(\mathsf {H}\).

In the tree method for K\(_{t}\), we have all the K-rules, with \(\mathsf {G}\) as the box and \(\mathsf {F}\) as the diamond. In addition, we have rules for \(\mathsf {H}\) as the box and \(\mathsf {P}\) as the diamond with a reversed perspective on the accessibility (or precedence) relation:

In the axiomatic approach, we have two versions of the (K) schema, one for the forward-looking box \(\mathsf {G}\) and one for the backward-looking box \(\mathsf {H}\):

(GK)

\(\mathsf {G}(A\to B) \to (\mathsf {G} A \to \mathsf {G} B)\)

(HK)

\(\mathsf {H}(A\to B) \to (\mathsf {H} A \to \mathsf {H} B)\)

We also have two versions of Necessitation, and two versions of (Dual):

(GDl)

\(\neg \mathsf {F} A \leftrightarrow \mathsf {G}\neg A\)

(HDl)

\(\neg \mathsf {P} A \leftrightarrow \mathsf {H}\neg A\)

(GNec)

\(\text {If $A$ occurs in a proof, $\mathsf {G} A$ may be appended.}\)

(HNec)

\(\text {If $A$ occurs in a proof, $\mathsf {H} A$ may be appended.}\)

In addition, we need two interaction principles, reflecting the fact that the accessibility relation for \(\mathsf {F}\) and \(\mathsf {G}\) is the inverse of the accessibility relation for \(\mathsf {P}\) and \(\mathsf {H}\):

(Con1)

\(A \to \mathsf {G}\mathsf {P} A\)

(Con2)

\(A \to \mathsf {H}\mathsf {F} A\)

These axioms and rules, added to those of classical propositional logic, define an axiomatic calculus that is sound and complete for K\(_{t}\). (Completeness is easily proved with the canonical model technique.)

For most applications, K\(_{t}\) is too weak. We will want to impose further restrictions on the relevant temporal models. For example, definition 7.1 allows for cases in which \(t < s\) and \(s < r\) without \(t < r\). But if a time \(t\) is earlier than \(s\), and \(s\) is earlier than \(r\), then surely \(t\) must be earlier than \(r\). For almost every application of temporal logic, we assume that the precedence relation is transitive. This corresponds to the (4)-schema for \(\mathsf {G}\). It also corresponds to the (4)-schema for \(\mathsf {H}\).

(4G)

\(\mathsf {G} A \to \mathsf {G}\mathsf {G} A\)

(4H)

\(\mathsf {H} A \to \mathsf {H}\mathsf {H} A\)

Another plausible condition is that no time is earlier than itself. Formally, \(<\) should be irreflexive, so that no element of \(T\) is \(<\)-related to itself. We know that reflexivity corresponds to the (T)-schema, whose (forward-looking) temporal analogue would be \(\mathsf {G} A \to A\). What corresponds to irreflexivity? The following observation reveals the answer: nothing.

Given transitivity, irreflexivity is closely related to asymmetry. Recall from the previous chapter that \(<\) is asymmetric if whenever \(t<s\) then not \(s<t\). There is no modal schema that corresponds to asymmetry.

In the previous chapter, I mentioned that transitive and irreflexive relations are called (strict) partial orders. The name reflects the fact that such orders need not order everything. In a model of branching time, for example, we can have \(t<s\) and \(t<r\) but neither \(s<r\) nor \(r<s\); in that case, \(r\) and \(s\) are not ordered by the precedence relation.

We can rule out such cases by imposing the requirement of connectedness, also known as completeness or totality. This demands that for any points \(t\) and \(s\), either \(t < s\) or \(t=s\) or \(s < t\). An irreflexive, transitive, and connected relation is called a (strict) linear order (or a strict total order).

For some applications, we may want linearity in only one direction. Many philosophers have been attracted to a branching-future conception of time, where a point in time may have more than one future, but only one past. In such models, we would only require backward-linearity: that if \(s < t\) and \(r < t\), then either \(s < r\) or \(s=r\) or \(r < s\).

An axiom schema corresponding to backward-linearity is (BL): \begin {equation} \tag {BL}\mathsf {F}\mathsf {P} A \to (\mathsf {F} A \lor A \lor \mathsf {P} A) \end {equation} Forward-linearity – the assumption that if \(t < s\) and \(t < r\), then either \(s < r\) or \(s=r\) or \(r < s\) – corresponds to (FL): \begin {equation} \tag {FL}\mathsf {P}\mathsf {F} A \to (\mathsf {P} A \lor A \lor \mathsf {F} A) \end {equation} The conjunction of (BL) and (FL) is valid on a frame iff the frame’s precedence relation does not branch in either direction. This is not quite the same as connectedness, because it allows for frames with parallel time lines. There is no schema that corresponds to connectedness.

The tree rules for backward-linearity and forward-linearity directly reflect the definition of the two properties.

These rules create three branches. The “identity nodes” \(\nu = \upsilon \) on the middle branch state that two world/time labels refer to the same thing. (This must be taken into account when reading off countermodels from open branches.) We need two further rules to deal with identity nodes. Both of these rules are called ‘Identity’.

The precedence relation in relativistic spacetime is neither backward-linear nor forward-linear. But it has a weaker property: convergence. A spacetime point \(p_1\) can precede two points \(p_2\) and \(p_3\) neither of which precedes the other, but these two points will always precede a common later point \(p_4\). Convergence corresponds to the (G)-schema. In temporal logic, we have one (G)-schema for future convergence and one for past convergence:

(FG)

\(\mathsf {F}\mathsf {G} A \to \mathsf {G}\mathsf {F} A\)

(PG)

\(\mathsf {P}\mathsf {H} A \to \mathsf {H}\mathsf {P} A\)

7.4Branching time

In section 1.5 we looked at the idea that the future is “open” while the past is “settled”. We can still influence (say) whether we will exercise tomorrow, but not whether we have exercised yesterday. Some have argued that the openness of the future calls for a non-linear model of time, with multiple branches into the future. On one branch, we would exercise tomorrow, on another we would not.

This line of thought appears to conflate temporal and modal considerations. The precedence relation in models of time is normally understood as a purely temporal relation – as the earlier-later relation. The fact that we can bring about a world in which we exercise tomorrow and a world in which we don’t exercise does not entail that both kinds of tomorrow take place here in the actual world.

If we want to make explicit the connections between settledness and time, it is better to use a multi-modal language with circumstantial operators for settledness and openness in addition to the purely temporal operators \(\mathsf {F}, \mathsf {G}, \mathsf {P}, \mathsf {H}\). We could then say things like \(\mathsf {P} A \to \Box \mathsf {P} A\) to formalize the claim that if \(A\) has happened then it is settled that \(A\) has happened.

There are nonetheless good reasons to consider branching models of time. I already mentioned that such models are widely used in computer science, where the “times” represent states of a computational process and the precedence relation has a semi-modal interpretation, holding between two states iff the first can lead to the second. I also mentioned that the precedence relation in relativistic spacetime allows for branching, although diverging spacetime branches ultimately reconverge. A more classical form of branching (without reconvergence) has been argued to follow from a certain interpretation of quantum physics. On this interpretation, what are normally understood to be chance events are really branching events in which all possible outcomes actually take place.

Another way to motivate a branching conception of time arises from a metaphysical view called presentism. According to presentism, only the present is real; all truths that seem to concern other times are reducible to more fundamental truths about the present. If, for example, it is true that there was a sea battle yesterday, then according to presentism this must ultimately be explained by what is true now; there must be facts about the present state of the world that entail (and explain) yesterday’s sea battle. Perhaps the relevant facts about the present specify the distribution of physical particles and fields etc. together with the general laws of nature. If the laws are deterministic, then the complete truth about the present distribution of particles and fields etc. together with the laws fixes all truths about the past and about the future. But suppose the laws are indeterministic towards the future: they merely settle that if the present physical state of the world is so-and-so, then the future is either like this or like that. In that case, the presentist will regard both of these futures as equally actual.

Let’s assume, then, that we want to reason about branching time. This is less straightforward than it might at first appear.

Two pieces of terminology will be useful. First, let’s define a history in a model \(\langle T,<,V \rangle \) as a maximal linearly ordered subset of \(T\). That is, a history is a collection of times \(H\) such that

• (i) for all \(t\) and \(s\) in \(H\), either \(t<s\) or \(t=s\) or \(s<t\), and

• (ii) no further member of \(T\) could be added to \(H\) without making (i) false.

The model (or rather, frame) depicted on the right contains two histories: \(\{ t_1, t_2, t_3 \}\) and \(\{ t_1, t_2, t_4 \}\).

For the second piece of terminology, let \(t\) be any time in any model. Any maximal linearly ordered set of times later than \(t\) will be called a future of \(t\). In the model on the right, \(t_1\) has two futures: \(\{ t_2, t_3 \}\) and \(\{ t_2, t_4 \}\).

If you look back at definition 7.2, you can see that in the standard semantics for temporal logic, \(\mathsf {G} p\) is true at \(t\) iff \(p\) is true at all times in all futures of \(t\); \(\mathsf {F} p\), on the other hand, is true at \(t\) iff \(p\) is true at some time in at least one future of \(t\). This ensures that \(\mathsf {G}\) and \(\mathsf {F}\) are duals, but it is often thought to be problematic if we want \(\mathsf {F} p\) to translate ‘it will be the case that \(p\)’.

To illustrate, suppose I’m about to toss a coin. In one future (let’s assume), the coin will land heads, in another it will land tails. By definition 7.2, both \(\mathsf {F} h\) and \(\mathsf {F} t\) are true. But should we say that the coin will land heads and also that it will land tails?

We could adopt an alternative semantics for \(\mathsf {F}\) according to which \(\mathsf {F} p\) is true at \(t\) iff \(p\) is true at some time in all futures of \(t\):

\(M,t \models \mathsf {F} A \;\text {iff every future of $t$ contains some $s$ such that $M,s \models A$}.\)

This is known as the Peircean interpretation of \(\mathsf {F}\) (after Charles S. Peirce; the name is due to Arthur Prior).

On the Peircean account, \(\mathsf {F} p\) is false whenever \(p\) only takes place in one of several futures. If we keep the classical interpretation of \(\mathsf {G}\), both \(\mathsf {F} p\) and \(\mathsf {G} \neg p\) can be false; the two operators are no longer duals. The dual of \(\mathsf {F}\) is a strange operator that applies to a sentence \(A\) iff there is some future in which \(A\) is always true.

A different line is taken by (what Prior called) the Ockhamist approach. According to Ockhamism, if there are several futures then it doesn’t make sense to say – without qualification – that \(p\) will be the case, or that \(p\) won’t be case. To talk about what will or won’t be the case we must specify which future we have in mind.

Formally, in Ockhamist semantics, the truth-value of every sentence is evaluated at a pair consisting at a time and a history. Histories are linear by definition, so the problems raised by multiple futures disappear. To say that \(p\) is the case in some history, or in all histories, Ockhamists add new operators \(\Diamond \) and \(\Box \) that quantify over histories. The Peircean \(\mathsf {F}\) operator is equivalent to \(\Box \mathsf {F}\) in Ockhamism. \(\Box \mathsf {F} p\) says that every future contains a time at which \(p\) is true; \(\Diamond Fp\), by contrast, would say that some future contains a time where \(p\) is true.

Here is the full Ockhamist semantics.

A sentence is valid in Ockhamist semantics if it is true at all times \(t\) on all histories \(H\) (containing \(t\)) in all models. As always, we can get stronger conceptions of validity – stronger logics – by adding further constraints on the precedence relation.

There is something odd about the Ockhamist approach. Consider a scenario in which there are multiple futures; one future holds a sea battle, another holds no sea battle. Let \(p\) translate ‘there is a sea battle’. Is \(\mathsf {F} p\) is true in this scenario (under the given interpretation of \(p\))? What about \(\mathsf {F}(p \lor \neg p)\)? Or \(Gp \to GGp\)?

Ockhamism refuses to give an answer. In Ockhamism, sentences are only true or false relative to a model and a time and a history. A branching-time scenario, however, does not fix a particular history. We’d like to know which sentences are true today if there are multiple futures. Ockhamism only tells us which sentences are true relative to each of the different futures. Relative to a history that contains a sea battle, \(\mathsf {F} p\) is true. Relative to other histories, \(\mathsf {F} p\) is false.

If we insist that logical validity should formalize the idea of truth in all scenarios under all interpretations of non-logical vocabulary then we can’t accept the official definition of validity in Ockhamist semantics. We have to extend the Ockhamist semantics to specify under what conditions a sentence is true in a model at a time, without fixing a history. Then we can say that a sentence is valid iff it is true at all times in all models.

A simple way to do this is to stipulate that a sentence is true at time in an (Ockhamist) model iff it is true relative to all histories that contain the time: \begin {align*} M,t \models A & \;\text {iff $M,H,t \models A$ for all histories $H$ that contain $t$}. \end {align*}

This is known as a supervaluationist semantics.

Supervaluationism is often used when a formal semantics defines truth relative to an “extra” parameter that doesn’t correspond to any feature of a conceivable scenario. In Ockhamist semantics, that parameter is the history \(H\). For a different application, consider vagueness. If \(p\) translates ‘it is warm’, and the temperature is borderline warm, it is not clear what we should say about the truth-value of \(p\), and about various complex sentences containing \(p\). One popular approach to vagueness is to first define truth relative to a sharpening of vague expressions. Relative to a sharpening on which temperatures above 15.0 degrees Celsius are warm, \(p\) has a clear truth-value in any conceivable scenario, as do complex sentences containing \(p\). Since an actual scenario does not fix a particular sharpening, this semantics contains an extra parameter. We can define a notion of truth without that parameter by saying that a sentence is true in a scenario iff it is true in that scenario relative to every eligible sharpening.

Supervaluationist accounts tend to have some non-classical features. Suppose we live in a branching world in which one future contains a sea battle and another doesn’t. Let \(p\) express that a sea battle takes place. According to supervaluationist Ockhamism, neither \(\mathsf {F} p\) nor \(\neg \mathsf {F} p\) is true in that scenario. Both are true relative to some but not relative to all histories. So neither is simply true. Assuming that a sentence is false if its negation is true, \(\mathsf {F} p\) is neither true nor false!

Logics in which a sentence can have a third status besides (mere) truth and (mere) falsity are called three-valued. Three-valued approaches to branching time are sometimes defended by the intuition that if a sea battle occurs on some but not all branches of the future, then one can’t truly assert that a battle will occur nor that it won’t occur.

The Polish logician Jan Łukasiewicz argued that statements about the future are either true, false, or “indeterminate”. To accommodate this third truth-value, he proposed three-valued truth-tables specifying how the truth-value of complex sentences are determined by the truth-value of their parts. For example, he suggested that if two sentences \(A\) and \(B\) are indeterminate, then their conjunction \(A \land B\), disjunction \(A \lor B\), and negations \(\neg A, \neg B\) are also indeterminate.

In the sea battle scenario, Łukasiewicz’s account renders \(\mathsf {F} s \,\lor \neg \mathsf {F} s\) indeterminate, assuming \(\mathsf {F} s\) is indeterminate. This is often regarded as problematic: even if we shouldn’t assert that there will be a sea battle, it is argued that we are justified to assert that there either will or there won’t be a sea battle. The supervaluationist form of Ockhamism, while also three-valued, avoids this problem. On the supervaluationist interpretation, \(\mathsf {F} s\) and \(\neg \mathsf {F} s\) are neither true nor false in the sea battle scenario, but \(\mathsf {F} s \,\lor \neg \mathsf {F} s\) is true.

7.5Extending the language

The expressive resources of standard modal and temporal logic are weak. There are many things we might want to say about the unfolding of events in time that can’t be said with \(\mathsf {F}, \mathsf {G}, \mathsf {P}\), and \(\mathsf {H}\). The Ockhamist history quantifiers are one way of adding expressive power to the basic language of temporal logic. In this section, we will look at some others.

A useful operator for logics of discrete and linear time is the “next” operator \(\mathsf {X}\) (also written ‘\(\bigcirc \)’). Informally, \(\mathsf {X} A\) means that \(A\) is true at the next point in time. Formally: \begin {align*} M,t \models \mathsf {X} A \;\text {iff} & \;\text {$M,s \models A$ for some $s$ such that (i) $t<s$ and (ii) $s<r$ for all $r$}\\[-0.5mm] & \;\text {such that $r\not =s$ and $t<r$.} \end {align*}

With the help of \(\mathsf {X}\), we can also say that \(A\) is true in two units of time (\(\mathsf {X}\mathsf {X} A\)), in three units of time (\(\mathsf {X}\mathsf {X}\mathsf {X} A\)), and so on. The corresponding operator for talking about the previous point in time is usually written \(\mathsf {Y}\).

A more powerful extension of \(\mathfrak {L}_T\) adds binary operators for “since” and “until”, which can be used to translate sentences like (1) and (2).

• (1) Ever since we left the house it has been raining.

• (2) It will be raining until we go back inside.

Informally, \(A\mathsf {S} B\) is true iff \(B\) was true at some time in the past and \(A\) has always been true since then; \(A \mathsf {U} B\) is true iff \(B\) will be true at some time in the future and \(A\) will always be true until then. Formally:

\begin {align*} M,t \models A \mathsf {S} B \;\text {iff} &\; \text {there is some $s$ with $s < t$ for which $M,s \models B$, and for all $r$}\\[-0.5mm] &\;\text {with $s < r < t$, we have $M, r \models A$.} \end {align*}

\begin {align*} M,t \models A \mathsf {U} B \;\text {iff} &\; \text {there is some $s$ with $t < s$ for which $M,s \models B$, and for all $r$}\\[-0.5mm] &\;\text {with $t < r < s$, we have $M, r \models A$.} \end {align*}

The operators \(\mathsf {F}, \mathsf {G},\mathsf {P},\) and \(\mathsf {H}\) can all be defined in terms of \(\mathsf {S}\) and \(\mathsf {U}\). For example, \(\mathsf {P} A\) is equivalent to \((p\lor \neg p)\mathsf {S} A\). And \(\mathsf {F} A\) is equivalent to \((p \lor \neg p)\mathsf {U} A\).

Another noteworthy addition to temporal logic is the “Now” operator \(\mathsf {N}\). To see the point of this operator, consider the following multi-modal statement.

• (3) We already knew yesterday that there would be a test today.

Using \(\mathsf {Y}\) for ‘yesterday’, we might try to translate (3) as \(\mathsf {Y} \mathsf {K} p\), where \(p\) translates ‘there is a test’. But that’s wrong. By the semantics for \(\mathsf {Y}\), \(\mathsf {Y} \mathsf {K} p\) is true today iff \(\mathsf {K} p\) is true yesterday (using days as temporal units). Since \(\mathsf {K} p\) entails \(p\), it follows that \(\mathsf {Y} \mathsf {K} p\) is true today only if \(p\) is true yesterday. But the test takes place today, not yesterday.

Intuitively, the problem is that ‘today’ in (3) refers to the present day, even though it occurs in the scope of the ‘yesterday’ operator. The same thing happens in the quantified statement (4).

• (4) One day everyone who is now rich will be poor.

Here, ‘now’ refers to the present time, even though it is in the scope of the \(\mathsf {F}\) operator ‘one day’.

With the “Now” operator \(\mathsf {N}\), we can translate (3) as \(\mathsf {Y} \mathsf {K} \mathsf {N} p\), and (4) as \(\mathsf {F} \forall x (\mathsf {N} Rx \to Px)\). (We will have a closer look at quantified modal logic in later chapters.)

Intuitively, the \(\mathsf {N}\) operator allows us to look outside the scope of an embedding operator. \(\mathsf {P} \mathsf {N} p\), for example, is true if there is some time in the past such that \(p\) is true not at that time, but at the present. How does this work formally?

By the semantics of \(\mathsf {P}\),\begin {align*} M,t \models \mathsf {P} \mathsf {N} p \;\text {iff} \;\text {$M,s \models \mathsf {N} p$ for some time $s < t$}. \end {align*}

Now we want \(M,s\models \mathsf {N} p\) to be true iff \(p\) is true at the original time \(t\). So we need to keep track of the original time at which we evaluate a sentence, even if a temporal operator shifts the time at which a subsentence is evaluated.

The simplest way to achieve this is to define truth relative to pairs of times. One of the times is shifted by the temporal operators, the other is held fixed.

Like the Ockhamist semantics from the previous section, this semantics has an extra parameter. An ordinary scenario is represented by a single time in a model, not by a pair of times. So we need to specify under what conditions a sentence is true at a (single) time. Here, the standard approach is not supervaluation but “diagonalization”: \begin {align*} M,t \models A & \;\text {iff $M,t,t \models A$}. \end {align*}

This “two-dimensional” semantics correctly predicts that \(\mathsf {P}\mathsf {N} p\) entails \(p\).

1.

Assume \(M,t \models \mathsf {P}\mathsf {N} p\).

2.

Then \(M,t,t \models \mathsf {P}\mathsf {N} p\), by the definition of truth at a time in a model.

3.

Then \(M,t,s \models \mathsf {N} p\) for some \(s<t\), by clause (i) of definition 7.4.

4.

Then \(M,t,t \models p\), by clause (k) of definition 7.4.

5.

Then \(M,t \models p\), by the definition of truth at a time in a model.

The presence of a “Now” operator has far-reaching consequences for the logic of time. For example, \(\mathsf {N} p \to p\) is valid, in the sense that it is true at all times in all models. But \(\mathsf {G}(\mathsf {N} p \to p)\) is invalid. If \(p\) is true at \(t\) and false at some time after \(t\), then \(\mathsf {G}(\mathsf {N} p \to p)\) is false at \(t\). So we must give up the forward and backward Necessitation rules. The fact that something is logically true does not entail that it will always be true!