MPI-I-92-214

The report is a draft version of the first six chapters of a book which is attempting to supply a comprehensive coverage of the mathematical and computational aspects of temporal logic. The first chapter introduces temporal logic and gives a fairly detatiled preview of the issues which will be covered in the rest of the whole book. These include expressive power, fixed point temporal languages and applications in computing. Chapter 2 develops the basic idea of a language built from connectives whose semantics is appropriate to some class of underlying ``models" of time: for example linear or branching time. Chapter 3 introduces Hilbert style axiomatizations of such logics and contains some simple completeness proofs. The incomplete chapter 4 considers the generally incomplete predicate temporal languages and gives examples of some of the variety of choices of language here. In Chapter 5 we debate the merits of using classical first order logic to talk about temporal structures from the ``outside" instead of using temporal languages ``inside" the structure. We also consider the possibility of using temporal logic itself as a metalanguage. Finally, in chapter 6 we present a general theory of axiomatization of temporal logics. This examines and uses the irreflexivity rule of Gabbay to provide very general techniques. Feferman has proposed a system, as an alternative framework for encoding logics and also for reasoning about those encodings. We have implemented a version of this framework and performed experiments that show that it is practical. Specifically, we describe a formalisation of predicate calculus and the development of an admissible rule that manipulates formulae with bound variables. This application will be of interest to researchers working with frameworks that use mechanisms based on substitution in the lambda calculus to implement variable binding and substitution in the declared logic directly. We suggest that meta-theoretic reasoning, even for a theory using bound variables, is not as difficult as is often supposed, and leads to more powerful ways of reasoning about the encoded theory.