Fishwick P.A. (editor) Handbook of Dynamic System Modeling
Подождите немного. Документ загружается.
20
Temporal Logic
Antony Galton
University of Exeter
20.1 Propositional Logic ......................................................20-1
20.2 Introducing Temporal Logic .......................................20-3
20.3 Syntax and Semantics ..................................................20-5
20.4 Models of Time ............................................................20-6
Transitivity
•
Reflexivity
•
Irreflexivity
•
Linearity
•
Boundedness
•
Density and Discreteness
•
Combinations of Properties
20.5 Further Extensions to the Formal Language .............. 20-11
20.6 Illustrative Examples ....................................................20-11
A System with an Attractor
•
Application to Reasoning
about Programs
•
Other Applications
20.7 Conclusion ...................................................................20-14
20.8 Further Reading ...........................................................20-14
In this chapter, we introduce temporal logic (TL), a logical formalism for reasoning about domains in
which the truth or falsity of statements can vary over time. These statements could include formulae
representing states of a dynamical system, which brings TL clearly within the scope of this handbook.
Since TL is an extension of propositional logic, we believe that the reader will best be in a position to
appreciate the former if we first provide a brief introduction to the latter; readers already familiar with
propositional logic can skip directly to Section 20.2.
20.1 Propositional Logic
Propositional logic is a basic system of formal logic that underlies most logical systems. Its purpose is to
enable the formalization of certain types of reasoning, such as
If the power supply is on, and the light-switch is down, and the bulb is not blown, then the light is on.
The light-switch is down and the light is not on.
Therefore, either the bulb is blown or the power supply is not on.
This piece of reasoning takes the form of an inference or argument; it consists of a set of premises (the
first two statements) followed by a conclusion (flagged by “therefore”), the idea being that the conclusion
is supposed to follow logically from the premises. An inference is said to be valid if the conclusion does
indeed logically follow from the premises; this means that the truth of the premises is sufficient to guarantee
the truth of the conclusion, i.e., in any situation in which the premises are all true, the conclusion must be
true as well. Propositional calculus (PC) is a formal system by which the process of determining whether
an inference is valid or not may be effectively mechanized.
20-1
20-2 Handbook of Dynamic System Modeling
PowerOn SwitchDown BulbBlown LightOn Premise 1 Premise 2 Conclusion
T
T
T
T
T
T
T
T
F
F
F
F
F
F
F
F
T
T
T
T
F
F
F
F
T
T
T
T
F
F
F
F
T
T
F
F
T
T
F
F
T
T
F
F
T
T
F
F
T
F
T
F
T
F
T
F
T
F
T
F
T
F
T
F
T
T
T
F
T
T
T
T
T
T
T
T
T
T
T
T
F
T
F
T
F
F
F
F
F
T
F
T
F
F
F
F
T
T
F
F
T
T
F
F
T
T
T
T
T
T
T
T
FIGURE 20.1 Truth table used for determining validity of an inference.
Writing PowerOn, SwitchDown, BulbBlown, and LightOn to stand for “The power supply is on,” “The
light-switch is down,” “The bulb is blown,” and “The light is on” respectively, the above inference can be
formalised as
PowerOn ∧SwitchDown ∧¬BulbBlown → LightOn
SwitchDown ∧¬LightOn
BulbBlown ∨¬PowerOn
Here, the symbol “∧,” known as conjunction, is read “and”; “∨” (disjunction) as “or,” “→” (material
implication) as “if …, then …,” and “¬” (negation) as “not” (or “it is not the case that”). An additional
symbol commonly used is “↔” (material equivalence), read “if and only if.”
1
The specific interpretations
of these symbols are provided by the following semantic rules, in which α and β stand for arbitrary
propositions:
•
α ∧β is true if and only if both α and β are true.
•
α ∨β is true if and only if at least one of α and β is true.
•
α → β is true if and only if it is not the case that α is true and β is false.
•
α ↔ β is true if and only if α and β are either both true or both false.
•
¬α is true if and only if α is false.
Because the meanings of these symbols are defined purely in terms of truth values, they are known as
truth-functional connectives; they are also known as Boolean connectives, in honor of George Boole who
first introduced a system recognizable as the PC in his Laws of Thought (1854).
Using these rules,we can show that the inference aboveis valid. A mechanical, if sometimes unnecessarily
complicated, way of doing this is through the construction of a truth table, as shown in Figure 20.1. Here,
every possible combination of truth values for the four atomic propositions occurring in the inference is
listed; for each combination, we use the semantic rules for the connectives to compute the truth values of
1
Commonly used alternative versions of some of these symbols include ⊃ for material implication, ≡for material
equivalence, and ∼for negation. In some contexts, these symbols are used in addition to the ones given in the main
text, with different meanings. Note also the bracket-dropping convention: α ∧ β → γ is understood to be implicitly
grouped as (α ∧β) → γ, and in general both ∧and ∨ are regarded as binding their arguments more closely than →
and ↔, unless this is explicitly overridden by brackets, as in α ∧ (β → γ).
Temporal Logic 20-3
the premises and conclusion of the inference. That the inference is valid is shown by the fact that every
combination of truth values which makes both the premises true also makes the conclusion true (lines 2,
10, and 12 of the table).
Within PC it is possible to establish the validity or invalidity of any pattern of inference that can be
expressed using the truth-functional connectives. Many types of reasoning, however, cannot be expressed
in this way, and for this reason the PC has been extended to produce various more expressive formalisms.
The most well known of these is the first-order predicate calculus, or first-order logic (FOL).
2
However,
the TL described in this chapter represents an alternative extension of PC.
20.2 Introducing Temporal Logic
In the PC inference discussed above, no reference is made to time, and this is true of the classical forms
of logic generally. The truth or falsity of each of the propositions is implicitly referred to a particular,
unstated time, so it is not possible to use PC to reason about propositions which refer to different times.
TL was introduced to remedy this deficiency.
An inference requiring some form of TL for its formulation is
The light is only ever on if the battery is charged.
Whenever the battery is charged, at a later time it will not be charged.
Therefore, the light will not always be on.
A TL formulation of this inference is as follows:
2(LightOn → BatteryCharged)
2(BatteryCharged → 3¬BatteryCharged)
¬2LightOn
(20.1)
Here, the symbols “2” and “3” may be read “always” and “eventually,” respectively. More exactly, their
meanings are expressed by the following semantic rules:
•
2α is true at time t
0
if and only if α is true at every time t ≥ t
0
.
•
3α is true at time t
0
if and only if α is true at at least one time t ≥ t
0
.
Note that if
2¬α is true at t
0
, then ¬α must be true at every time t ≥ t
0
, which means that there cannot
be any time t ≥ t
0
at which α is true; hence 3α must be false at t
0
.Conversely,if2¬α is false then 3α
must be true. For this reason, we can affirm that the formulae ¬
2¬α and 3α are always equivalent, and
this is usually captured by defining
3 in terms of 2 as follows:
3α =
def
¬2¬α (Def3)
The validity of inference (Eq. [20.1]) may be demonstrated informally by a reductio ad absurdum
argument. Suppose that, at t
0
, the premises are both true but the conclusion is false. At t
0
, therefore, we
have
2(LightOn → BatteryCharged), 2(BatteryCharged → 3¬BatteryCharged), and 2LightOn. By the
semantic rule for
2, this means that at t
0
(and indeed at every time t ≥ t
0
), we have
LightOn → BatteryCharged (20.2)
BatteryCharged →
3¬BatteryCharged (20.3)
LightOn (20.4)
2
An account of FOL can be found in almost any textbook on formal logic, for example, Hodges (2001) and
Jeffrey (2006).
20-4 Handbook of Dynamic System Modeling
By PC reasoning, from Eq. (20.4) and Eq. (20.2) we also have
BatteryCharged (20.5)
at t
0
and hence also from Eq. (20.5) and Eq. (20.3)
3¬BatteryCharged (20.6)
By the semantic rule for
3, this means that there is a time t ≥t
0
at which ¬BatteryCharged is true (note
that since BatteryCharged is true at t
0
, we must in fact have t > t
0
). Moreover, since t ≥t
0
, we know from
our earlier deductions that both Eq. (20.2) and Eq. (20.4) are true at t; and these imply that BatteryCharged
is true at t as well. This contradicts our earlier deduction that ¬BatteryCharged is true then. Hence, the
supposition that the premises could be true and the conclusion false is absurd, and we conclude that if the
premises are true, the conclusion must be true too—i.e., the inference is valid.
Although we referred to individual times (t
0
, t) in this reasoning, TL allows us to work purely at the
level of the
2, 3 language used in the formulae, with no explicit reference to times. To illustrate this, we
shall prove the above inference in a TL in which the following formulae are posited as axioms:
3
2(α → β) → (2α → 2β)(AxK)
2α → α (AxT)
and the following rules of inference are introduced:
4
From α and α → β infer β (MP)
From α infer
2α (R2)
If α is a theorem of PC, infer α (PCT)
Here “ α” means that α is a theorem, i.e., considered proved. All the axioms count as theorems, and
anything that can be inferred from the axioms using the rules of inference is also a theorem.
To establish the validity of the inference above, we make use of three PC theorems, not proved here:
(α → β) ∧(β → γ) → (α → γ) (20.7)
(α → β) ∧(¬α → β) → β (20.8)
(α → β) ↔ (¬β →¬α) (20.9)
Starting with the two premises
2(LightOn → BatteryCharged)
2(BatteryCharged → 3¬BatteryCharged)
we can use (PCT), Eq. (20.7), and (AxK) to give
2(LightOn → 3¬BatteryCharged), and hence by (AxT)
LightOn →
3¬BatteryCharged (20.10)
Premise 1 also gives, by (AxK),
2LightOn → 2BatteryCharged. Using Eq. (20.9), this can be rewritten as
¬
2BatteryCharged →¬2LightOn, and hence, by (Def3), as
3¬BatteryCharged →¬2LightOn (20.11)
3
K and T are the labels conventionally given to these axioms; as far as I am aware, these letters do not “stand for”
anything.
4
See Section 20.3 for a general explanation of axioms and rules of inference. “MP” here stands for Modus Ponens,
the Latin name given to this pattern of inference in the logical tradition.
Temporal Logic 20-5
From Eq. (20.10) and Eq. (20.11), using Eq. (20.7) and (AxK), we now have
LightOn →¬
2LightOn (20.12)
By (AxT), we also have
2LightOn → LightOn, which using Eq. (20.9) gives
¬LightOn →¬
2LightOn (20.13)
Finally, from Eq. (20.12) and Eq. (20.13), using Eq. (20.8) we infer the desired conclusion ¬
2LightOn.
20.3 Syntax and Semantics
The preceding section introduced a particular, rather simple, variety of TL, and in the next section we will
examine some other varieties. To prepare the way for this, it is necessary to say a few words about what a
logical system consists of and how it is structured.
At the heart of the system is a formal language. This is defined as a set of well-formed formulas (wffs),
each of which is a legitimate concatenation of symbols taken from some predefined vocabulary. Which
concatenations are legitimate is determined by the rules of formation of the language, which define its
syntax (or formal grammar).
For the TL in Section 20.2, the vocabulary consists of the logical constants “¬,” “ ∧,” “ ∨,” “ →,” “ ↔,” “
2,”
and “
3” together with a set of literals to represent elementary propositions; these may be tailored to the
application context by taking a form suggestive of their intended meanings (e.g., LightOn, BatteryCharged),
but in more general application-independent treatments it is convenient to use simple letters (e.g., A, B,
C, …) instead. Finally, parentheses “(” and “)” are used to help articulate the structure of formulae.
The wffs of this system are defined by the following rules of formation:
1. Any literal is a wff.
2. If α and β are wffs then so are ¬α,(α ∧β), (α ∨ β), (α → β), (α ↔ β),
2α, and 3α.
This is a recursive definition; by repeated applications of these rules we can build up complex wffs such as
2(2A → B) ∨2(2B → A).
5
Thus far, all we have defined is a set of symbol-concatenations which we have dignified with the name
of wff; these wffs do not, on their own, possess any meaning. Wffs can be made meaningful in two ways:
1. Explicitly, by specifying how they are to be interpreted.
2. Implicitly, by specifying their logical relationships to other wffs.
The former method gives rise to what is known as model theory, and the latter to proof theory.
Consider the symbol “∧.” Its semantic rule, given above, states that a wff α ∧ β is true if and only if
both α and β are true. But a formula such as α can be given many different interpretations, in some of
which it stands for a true statement, in others for a false one; an interpretation in which α stands for a true
statement is said to satisfy α. The meaning of “∧” is specified by stipulating that an interpretation satisfies
α ∧β if and only if it satisfies both α and β. The other semantic rules in Section 20.1 are to be understood
analogously.
Given a collection of wffs, we may or may not be able to find an interpretation, consistent with the
semantic rules, in which all the wffs are true; any such interpretation is called a model for that set of wffs.
Model theory is thus the way of specifying the meanings of formulae by laying down what counts as an
interpretation of the formal language, and what it is for an interpretation to satisfy a formula. For our TL,
this was what is provided, in part, by the semantic rules given above.
5
Strictly speaking this should be (2(2A → B) ∨ 2(2B → A)), but it is conventional to omit the outer pair of
brackets in cases such as this (see also footnote 1).
20-6 Handbook of Dynamic System Modeling
Recall the semantic rule for “2”: 2α is true at time t
0
if and only if α is true at every time t ≥t
0
. This
is not telling us about the truth of
2α absolutely, but its truth at a particular time; moreover, the rule
specifies the truth of
2α at one time in terms of the truth of α at other times—thus t
0
is just one of a set of
times, elements of which can be compared using the relation ≥(where t
1
≥t
0
means that t
1
is later than
or equal to t
0
). From these observations we see that an interpretation of a TL formula must be considered
as relative to a time taken from some ordered system of times.
Let T be the set of times, and let ≺ denote the ordering relation on T (this may be read as “precedes,”
with the caveat that in some models, a time may precede itself). Together, these constitute a temporal frame
(T, ≺). We write
(T, ≺, t) |= α
to mean that the wff α is true at time t in the temporal frame (T, ≺). With this notation, the semantic
rules for
2 and 3 can be reformulated as
6
•
(T, ≺, t) |= 2α if and only if, for every t
∈T,ift ≺ t
then (T, ≺, t
) |= α.
•
(T, ≺, t) |= 3α if and only if, for at least one t
∈T, t ≺ t
and (T, ≺, t
) |= α.
Proof theory offers a completely different approach to specifying meanings. We characterize the meaning
of a logical symbol by stating logical properties of formulae containing that symbol. One way of doing
this is in terms of inference rules. For conjunction,“∧,” the inference rules most commonly given are
(∧-introduction) From α and β, derive α ∧ β.
(∧-elimination) From α ∧ β, derive both α and β.
Introduction and elimination rules, some more complex than these, can be given for the other connectives.
We havealreadymet some inference rules for TL (MP,R
2, and PCT). A“natural deduction”system provides
a proof theory consisting entirely of inference rules; an axiom system includes in addition a set of formulae,
called axioms, which are stipulated to be true (e.g., AxK and AxT).
Logic is concerned with making valid inferences. The meaning of validity is generally defined in terms of
a model theory: an inference is valid if and only if every model for the premises satisfies the conclusion. This
corresponds to the intuitive idea that in a valid inference,if the premises are true then the conclusion cannot
fail to be true as well. The model-theoretic definition sets the standard which the proof theory, as a practical
set of inferential procedures, should live up to. A proof theory is sound with respect to a given model theory
if every inference validated by the former is indeed valid according to the latter; and it is complete with
respect to the model theory if every inference valid according to the latter is validated by the former. The
ideal is a proof theory that is both sound and complete with respect to the model theory corresponding
to the intended application of the logic. In some cases this can be achieved, but in others it cannot.
20.4 Models of Time
An interpretation of TL is defined by specifying a temporal frame (T, ≺ ), a reference time t
0
(“now”),
and, for each literal L in the language, its truth value at each time t ∈T. The semantic rules for the logic
then determine the truth value of each formula at each time, and in particular at the reference time t
0
.
The temporal frame obviously plays an essential role in all this, and the truth values of formulae in
the logic can depend critically on the properties of the frame. The frame in effect encapsulates a model of
time. In this section, we look at some of the key frame properties that are used in different applications,
and the impact they can have on the truth values of different formulae. As a side effect of this survey, we
shall also be led to indicate extensions to the logical vocabulary which have been introduced to enhance
the expressive power of the logic with respect to different models of time.
6
The semantic rules for the Boolean connectives, when considered as forming part of TL, can likewise be written in
this style, e.g., for conjunction: (T, ≺, t) |= α ∧β if and only if (T, ≺, t) |= α and (T, ≺, t) |= β.
Temporal Logic 20-7
Of the two components required to specify a frame, i.e., the set T and the relation ≺, the latter will play
a major role in what follows. As far as the former is concerned, nothing depends on what the elements
of T actually are: essentially they can be regarded as abstract elements that are taken to represent “times,”
but there is little need here for a philosophical discussion on what we actually mean by “a time.” The only
exception to this concerns whether we regard times as durationless instants or extended intervals. Most
developments of TL opt for the former understanding, but the latter also has had its advocates, especially
when TL is used to specify the semantics of temporal expressions in natural language.
7
Here we shall
assume that times are effectively point-like, so that no change can take place within a time; thus each
formula has a single truth value at each time. That apart, the only feature of T that is relevant for TL is its
cardinality, e.g., whether it is finite, countably infinite, or uncountable.
We now embark on the survey of frame properties. These will be expressed in both English and FOL.
Readers unfamiliar with the latter should be able to understand the properties from the English description
alone.
20.4.1 Transitivity
It is natural to regard the ordering of times as transitive, as implied by the use of the word “ordering.” It
means that if one time precedes a second, which in turn precedes a third, then the first time must also
precede the third; in symbols
∀t∀t
∀t
(t ≺ t
∧t
≺ t
→ t ≺ t
) (Trans)
Transitive temporal frames can be characterized by the fact that in any interpretation over such a frame,
for any TL formula α, the formula
2α → 22α (Ax4)
is true at every t ∈ T. This is often postulated as an axiom, thereby restricting the allowed interpretations
to transitive frames.
One way of describing transitivity is that the future of the future already counts as future now—this
corresponds to the formula
33α → 3α which can be proved to be equivalent to (Ax4). A nontransitive
frame thus requires the notion of “future” to be qualified in some way which leads to a breakdown in
transitivity, e.g., the “near” future (“within the next 10 years,” say).
20.4.2 Reflexivity
A temporal order is reflexive if every time is regarded as “preceding” itself, i.e.,
∀t(t ≺ t)(Refl)
In effect, this means that the precedence relation ≺ is interpreted not as “precedes” but as “precedes or
equals” (i.e., “not later than” rather than “earlier than”). This was, in fact, the interpretation used in our
example in Section 20.2, where the semantic rules used “t ≥t
0
” for “t
0
≺t.”
Reflexive temporal frames are characterized by the schema (AxT) which we discussed in Section 20.2.
An equivalent formulation is α →
3α.
20.4.3 Irreflexivity
A nonreflexive frame satisfies ¬∀t(t ≺t) (“not every time precedes itself”), but for a frame to count as
irreflexive it must satisfy the stronger condition
∀t¬(t ≺ t)(Irref)
7
Examples are, in the context of reasoning about programs (Moszkowski, 1986) and in the context of analyzing
natural language (Dowty, 1979).
20-8 Handbook of Dynamic System Modeling
i.e., no time precedes itself. This is satisfied by our normal understanding of “precedes” as “earlier than.”
However, there is no TL formula that exactly characterizes irreflexive frames in the way (AxT) characterizes
reflexive ones.
20.4.4 Linearity
The reader has probably assumed in the foregoing that the temporal structure is linear, i.e., that the times
are as it were strung out along a single line, in keeping with our ordinary notion of a “time line.” However,
such linearity is by no means entailed by any of the properties mentioned above, all of which are compatible
with a wide range of branching or network-like structures. If we wish our time line to be linear, then this
has to be built in explicitly.
The property of linearity is expressed by the formula
∀t∀t
(t ≺ t
∨t = t
∨t
≺ t) (Lin)
which says that either the times t and t
are the same time (t =t
) or one precedes the other (t ≺t
∨t
≺t).
The TL we have used so far cannot express this notion of linearity. The best we can do is
3α ∧3β → 3(α ∧ β) ∨(α ∧ 3β) ∨(3α ∧ β)
which captures the idea that of any two future times, either they coincide or one precedes the other. This
characterizes time as “linear in the future,”
8
but does not rule out “alternative pasts” whose times do not
stand in any direct temporal relation to each other. Future-linearity is expressed by the formula
∀t∀t
∀t
(t
≺ t ∧ t
≺ t
→ t ≺ t
∨t = t
∨t
≺ t) (FLin)
For linear time we also require past-linearity (or “left-linearity”), i.e.,
∀t∀t
∀t
(t ≺ t
∧t
≺ t
→ t ≺ t
∨t = t
∨t
≺ t) (PLin)
and this cannot be expressed using the operators
2 and 3, since these operators are future-directed,
describing the present in terms of the future. To express past-linearity, and hence full linearity, we need
past-directed operators as well.
The usual notation, when both sets of operators are used, is to write F and G for the future-directed
operators (i.e., our earlier
3 and 2), and P and H for the past-directed ones, as captured by the following
mnemonics:
FAAwill be true sometime in the Future
GAAis always Going to be true
PAAwas true sometime in the Past
HAAHas always been true
The operators F, G, P, and H are called tense operators, and a TL that uses both sets of operators is called
a tense logic. Historically, tense logics were the first kind of TL to be developed, arising from the work of
the philosopher A. N. Prior in the 1950s and 1960s (Prior, 1967, 1968).
Backward and forward linearity are expressed by the tense logic formulae
Pα ∧Pβ → P(α ∧ β) ∨(α ∧ Pβ) ∨(Pα ∧ β)
Fα ∧Fβ → F(α ∧ β) ∨(α ∧ Fβ) ∨(Fα ∧ β)
but with both past- and future-tense operators available the same properties can be more simply
expressed by
FPα → Pα ∨α ∨Fα
PFα → Pα ∨α ∨Fα
8
Often called “right-linear,” presupposing a picture in which time flows from left to right!
Temporal Logic 20-9
The first formula says that anything that will be past is either already past, present, or still future. This
rules out the possibility of separate past time lines converging on a common time. Similarly the second
formula likewise rules out separate future time lines diverging from a common time.
One might expect that (PLin) and (FLin) together would suffice for full linearity (Lin), but this is not so,
since they allow two or more “parallel” time lines between which there are no temporal relations. Indeed,
it is not possible to rule out this latter kind of model by means of any tense logic formula.
While for many purposes it is natural to demand that the model of time is linear, this is not always the
case. If TL is used to model the evolution of a nondeterministic dynamical system, one way of incorporating
the indeterminacy is to model the full set of possible histories by means of a temporal frame which branches
into the future—and hence lacks future-linearity. It is usual even in this case to retain past-linearity, so
as to rule out convergent time lines. Then each point in time has a unique past but may have more than
one future. This kind of structure was introduced in the context of reasoning about nondeterministic
computations by Lamport (1980).
For reasoning about such future-branching models, an extension to TL called computation tree logic
(CTL) has been introduced. In addition to temporal operators such as
2 and 3, CTL uses the “path
operators” A and E to describe properties as true for respectively all or some of the futures diverging
from the time at which a formula is evaluated. For example, the CTL axiom A
2α →¬E3¬α says that
if α is true throughout all possible futures then there is no possible future in which α is at any time
false. CTL was introduced (Emerson and Clarke, 1982) as a method for deriving the “synchronization
skeleton” of a concurrent computer program from a high-level specification. The specification, in CTL,
expresses the temporal constraints which must be satisfied by any execution of the program, and the
synchronization skeleton that is derived from it is “an abstraction of the actual program where detail
irrelevant to synchronization is suppressed.” Subsequently, more expressive extensions of CTL such as
CTL*, ECTL, and ECTL
+
were introduced (see (Emerson, 1990), for references).
20.4.5 Boundedness
A model of time is bounded in the past if it has a start time, that is, a time which is not preceded by any
other time; and it is bounded in the future if it has an end time which is not followed by any other time. So
long as time is linear, there can be at most one of each, but in a nonlinear temporal frame there can be many
possibilities, for example, some branches might have an end time but others not. For reasoning about a
dynamic system that is set up at a particular time and then allowed to evolve, it is natural to include a
start time, but not an end time, in the temporal model. For reasoning about natural systems which may be
regarded as having histories extending indefinitely far into the past as well as into the future, it may be better
to drop the start time as well. In that case, we have an unbounded temporal frame. The first-order formulae
∀t∃t
(t
≺ t) (PUnb)
∀t∃t
(t ≺ t
) (FUnb)
express unboundedness in the past and future, respectively. Corresponding tense logic axioms are
Hα → Pα and Gα → Fα. The first says that a formula true at every past time is true at some past
time, and hence there must be at least one past time; for this to hold universally, it must be that for every
time there is an earlier time, as expressed by (PUnb). The second axiom may be explained similarly. The
conjunction of (PUnb) and (FUnb) may be designated (Unb).
20.4.6 Density and Discreteness
The transitivity axiom, discussed in Section 20.4.1, says that whenever t precedes t
and t
precedes t
, then
t precedes t
. An important question for a model of time is whether the converse holds, i.e., if t precedes
t
must there be a time t
such that t precedes t
and t
precedes t
. A temporal frame that satisfies this
condition is called dense. The first-order formulation of density is
∀t∀t
(t ≺ t
→∃t
(t ≺ t
∧t
≺ t
)) (Dens)