Axiomatising First-Order Temporal Logic:

Until and Since over Linear Time

Mark Reynolds1

February 17, 1995

Abstract

We present an axiomatisation for the first-order temporal logic with connectives Until and Since over the class of all linear flows of time. Completeness of the axiom system is proved.
We also add a few axioms to find a sound and complete axiomatisation for the first-order temporal logic of Until and Since over rational numbers time.

1 Introduction

We present an axiomatisation for the first-order temporal logic with Until and Since over linear time. This is a very natural logic to reason in and is sufficiently expressive to be practically useful for formalising reasoning about changes over time. The slightly novel form of completeness proof used here may also be of interest.

There are many axiomatisations for temporal logics. As a glance through [van Benthem, 1982] will show, there are many for propositional logics with the Priorean connectives of F , for `will be in the future', and P , for `was in the past'. Recently more interest has been shown in Kamp's connectives Until, U , and Since, S, with axiomatisation results in [Burgess, 1982], [Xu, 1988], [Gabbay and Hodkinson, 1990], [Reynolds, 1992b], [Venema, 1991] and [Zanardo, 1991]. As shown in [Gabbay et al., 1994], this language is able to express more and so is more useful. For applications in computer science see, for example, [Gabbay et al., 1980], [Manna and Pnueli, 1992] and [Gabbay et al., 1994].

However, to be really expressive and useful we must turn to first-order temporal logic { where instead of a propositional world existing at each time point we have a full first-order structure. Such logics are ideal for describing the behaviour of computer programs (see for example, [Andr?eka et al., 1993] and [Szalas, 1987b]) but the move introduces at least two problems. First, we have to contend with a bewildering variety of ways of formalising such

1The author would like to thank Dov Gabbay and Ian Hodkinson for helpful discussions on this material. The work was supported by the U.K. Science and Engineering Research Council under the Metatem project (GR/F/28526).