Temporal logics, as their name suggests, are logics that involve time. They form a very large and important class of modal logics, but here we will, to start with, only look at some simple cases. Temporal logics are very closely related to tense logic?s.
First the basic temporal language is built with two binary model operators, which instead of being denoted ‘box’ and ‘diamond’, are written and . The intended interpretation of these are:
is will be true at some future time;
is was true at some past time.
The reason for the notation and should be clear.
The dual of is , so . This means that we read as ‘at no future time is not true’, i.e., is always going to be true. ( for ‘going’.)
The dual of is written , whence and interprets as ‘ has always been true’. ( is for ‘has’ - which is a bit weak, but that is life!)
If for all we have , then whatever has happened will always have happened, which seems reasonable so this might be a suitable ‘general truth’ we might want a temporal logic to contain.
If we had in our logic that , then this would means that if is true at some future time, then at some future time it will be true that will be true at some future time, so between any two instants there must be a third, and the general truth of this would say something about the ‘internal structure’ of time as modelled by such a logic.
This basic temporal language does not yet really constitute a sensible logic that could model important features of ‘time’. but we can still look at models so as to see what properties of the models can be identified as corresponding to seemingly feasible formulae in the language.
A frame for BTL will be a set, , with two binary relations and . We have reads that ‘at , is in the future’ - but, in the ordinary common sense meaning of words, this should mean and conversely. In other words should be the converse or opposite relation of .
(In general, if is a binary relation on a set , then its opposite relation is defined by
A frame of the form is called a bidirectional frame.
If we have any model with a valuation, , then we can interpret BTL in terms of it by specifying the interpretation of in terms that of . explicitly we define
if and only if
if and only if ,
but, of course, this is still a long way from having a logic that looks as if it captures ‘time-like’ behaviour. We could have models with ‘circular time’, and ‘branching time’. Both of these correspond to various situations in computational applications so should be kept in mind, both to be able to identify their occurrence and to build them in or to avoid them in the logics.
One condition it would be natural to impose is transitivity of , since if is true at some future time, then clearly, itself must also be true at some future time, i.e., later on still! This leads one to ask that
should be in our logic, (and similarly for , but that will hold in the bidirectional models since if is transitive then so will be ).
Consider a category , and an internal category given by . Here we understand elements of as time intervals, and and as marking their beginning and end points. We may choose to impose additional structure on , e.g., that it be an internal poset, or a linear order.
Then we find two adjunctions and , e.g.,
Now consider for the moment that and are propositions. Then means “there is some interval beginning now and such that is true at its end”, i.e. ; while means “for all intervals ending now, is true at their beginning”, i.e. . Hence our adjunction is . Similarly, interchanging and , we find . Note that we don’t have to assume the classical principle and .
In the setting of dependent type theory, we do not need to restrict to propositions, but can treat the temporal operators on general time-dependent types. So if is the type of people alive at , is the type of people alive at a point in the future of , and is a function from future times to people alive at that time, e.g., an element of this is ‘The oldest person alive(t)’.
Since is a category, we have in addition to the two projections , composition . This allows us to express more subtle temporal expressions, such as ‘ has been true since a time when was true’, denoted .
(note ). That is, there is a subinterval ending now such that was true at its beginning and was true at all points inside it. Similarly, ‘ will be true until a time when is true’ is
Temporal logicians have debated the relevant advantages of instant-based and interval-based approaches. Some have also considered hybrid approaches (Balb11). The analysis of this section suggests that working with intervals and instants together in the form of an internal category allows for a natural treatment via adjoint logic.
One of the consequences of taking as an internal category is that the future includes the present, so that could be true now and at no other instant but we would have that is true when it is supposed to say “ will be true at some Future time”. Similarly, we would have that holds now if and both hold now (in general, as defined above it requires to still hold at the instant when becomes true).
If we wish to change these consequences, we could let be the -intervals instead of the -ones. In other words, we could take to be a semicategory. While this accords with standard practice, the original alternative has been proposed:
The most common practice in temporal logic is to regard time as an irreflexive ordering, so that “henceforth”, meaning “at all future times”, does not refer to the present moment. On the other hand, the Greek philosopher Diodorus proposed that the necessary be identified with that which is now and will always be the case. This suggests a temporal interpretation of that is naturally formalised by using reflexive orderings. The same interpretation is adopted in the logic of concurrent programs to be discussed. (Gold92, p. 44)
On the other hand, some temporal logicians look to represent both forms of ‘henceforth’.
Generally this entry is based on
but see also:
Balbiani, P., Goranko, V. and Sciavicco, G., 2011, ‘Two-sorted Point-Interval Temporal logics’, in Proc. of the 7th International Workshop on Methods for Modalities (M4M7) (Electronic Notes in Theoretical Computer Science: Volume 278), pp. 31–45.