Skip to main content
Log in

An axiomatization for until and since over the reals without the IRR rule

  • Published:
Studia Logica Aims and scope Submit manuscript

Abstract

We give a Hilbert style axiomatization for the set of formulas in the temporal language with Until and Since which are valid over the real number flow of time. The axiomatization, which is orthodox in the sense of only having the usual temporal rules of inference, is complete with respect to single formulas.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Similar content being viewed by others

References

  1. Johan van Benthem, The Logic of Time, Reidel, Dordrecht, 1982.

    Google Scholar 

  2. J.P. Burgess, Axioms for tense logic I: “Since” and “Until”, Notre Dame J. Formal Logic 23 no.2 (1982) 367–374.

    Google Scholar 

  3. J.P. Burgess and Y. Gurevich, The decision problem for linear temporal logic, Notre Dame J. Formal Logic 26 no. 2 (1985) 115–128.

    Google Scholar 

  4. Kees Doets, Completeness and Definability, Dissertation, Mathematical Institute, Univ. of Amsterdam, 1987.

  5. Kees Doets, Monadic II 11 -theories ofII 11 -properties, Notre Dame J. Formal Logic 30 no. 2 (1989), 224–240.

    Google Scholar 

  6. D.M. Gabbay, An irreflexivity lemma, in: Aspects of Philosophical Logic, ed U. Monnich, Reidel, Dordrecht, 1981, 67–89.

    Google Scholar 

  7. D.M. Gabbay in collaboration with I.M. Hodkinson and M.A. Reynolds, Temporal Logic: Mathematical Foundations and Computational Aspects, O.U.P. to be published 1992.

  8. D.M. Gabbay and I.M. Hodkinson, An axiomatization of the temporal logic with Until and Since over the real numbers, J. Logic and Computation 1 (1990) 229–259.

    Google Scholar 

  9. D.M. Gabbay, I.M. Hodkinson and M.A. Reynolds, Temporal expressive completeness in the presence of gaps, in Proceedings ASL European Meeting, 1990, Helsinki, vol 1 of Lecture Notes in Logic, Springer-Verlag 1991.

  10. D.M. Gabbay, A. Pnueli, S. Shelah and J. Stavi, On the temporal analysis of fairness, 7th ACM Symposium on Principles of Programming Languages, Las Vegas, 1980, 163–173.

  11. D.M. Gabbay and M.A. Reynolds, Inheriting expressive completeness, Logic and Computation Research Report, Dept Comp., Imperial College, in preparation.

  12. I.M. Hodkinson, Notes on the irreflexivity rule, Logic and Computation Research Report, Dept Comp., Imperial College, in preparation.

  13. J.A.W. Kamp, Tense Logic and the theory of linear order, Ph.D. Thesis, University of California, 1968.

  14. S. Kuhn, The domino relation: flattening a two-dimensional logic, Journal of Philosophical Logic, 18 (1989) 173–195.

    Google Scholar 

  15. J.G Rosenstein, Linear Orderings, Academic Press, New York, 1982.

    Google Scholar 

  16. Y. Venema, Modal derivation rules, ITLI prepublication, Instit. for Lang., Logic and Information, University of Amsterdam., 1991.

  17. Y. Venema, Completeness via Completeness: Since and Until, in: Colloquium on Modal Logic 1991, ed. M. de Rijke, ITLI-Network Publication, Instit. for Lang., Logic and Information, University of Amsterdam., to appear.

  18. M. Xu, On some U, S-tense logics, J. of Philosophical Logic 17 (1988) 181–202.

    Google Scholar 

  19. A. Zanardo, A complete deductive system for Since-Until branching time logic, J. of Philosophical Logic 20 (1991) 131–148.

    Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Additional information

The author would like to thank Dov Gabbay, Yde Venema, the referee and especially Ian Hodkinson for helpful comments during the development of this work. The work was supported by the U.K. Science and Engineering Research Council under the Metatem project (GR/F/28526).

Rights and permissions

Reprints and permissions

About this article

Cite this article

Reynolds, M. An axiomatization for until and since over the reals without the IRR rule. Stud Logica 51, 165–193 (1992). https://doi.org/10.1007/BF00370112

Download citation

  • Received:

  • Issue Date:

  • DOI: https://doi.org/10.1007/BF00370112

Keywords

Navigation