Abstract
Kamp’s theorem established the expressive completeness of the temporal modalities Until and Since for the First-Order Monadic Logic of Order (FOMLO) over real and natural time flows. Over natural time, a single future modality (Until) is sufficient to express all future FOMLO formulas. These are formulas whose truth value at any moment is determined by what happens from that moment on. Yet this fails to extend to real time domains: here no finite basis of future modalities can express all future FOMLO formulas. Almost future formulas extend future formulas; they depend just on the very near past, and are independent of the rest of the past. For almost future formulas finiteness is recovered over Dedekind complete time flows. In this paper we show that there is no temporal logic with finitely many modalities which is expressively complete for the almost future fragment of FOMLO over all linear flows.
Dedicated to Yuri Gurevich on the occasion of his 75th birthday.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
A more detailed analysis which relies on Ehrenfeucht-Fraïssé games shows that \(\mathcal {C}^i\equiv _n\mathcal {C}^n\) for every \(i\ge n\).
References
Ehrenfeucht, A.: An application of games to the completeness problem for formalized theories. Fundam. Math. 49, 129–141 (1961)
Gabbay, D., Hodkinson, I., Reynolds, M.: Temporal logic: Mathematical Foundations and Computational Aspects. Oxford University Press, Cary (1994)
Gurevich, Y.: Monadic second order theories. In: Barwise, J., Feferman, S. (eds.) Model Theoretic Logics, pp. 479–506. Springer, Heidelberg (1985)
Gabbay, D., Pnueli, A., Shelah, S., Stavi, J.: On the temporal analysis of fairness. In: POPL 1980, pp. 163–173 (1980)
Hirshfeld, Y., Rabinovich, A.: Future temporal logic needs infinitely many modalities. Inf. Comput. 187, 196–208 (2003)
Kamp, H.W.: Tense logic and the theory of linear order. Ph.D. thesis. University of California, Los Angeles (1968)
Pnueli, A.: The temporal logic of programs. In: Proceeding of IEEE 18th Annual Symposium on Foundations Computer Science, pp. 46–57, New York (1977)
Pardo (Ordentlich), D., Rabinovich, A.: A finite basis for ‘almost future’ temporal logic over the reals. In: Rovan, B., Sassone, V., Widmayer, P. (eds.) MFCS 2012. LNCS, vol. 7464, pp. 740–751. Springer, Heidelberg (2012)
Rabinovich, A.: A Proof of Kamp’s Theorem. Log. Methods Comput. Sci. 10(1) (2014)
Acknowledgments
I am very grateful to Dorit Pardo for numerous insightful discussions and to the anonymous referee for his helpful suggestions.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this chapter
Cite this chapter
Rabinovich, A. (2015). On Almost Future Temporal Logics. In: Beklemishev, L., Blass, A., Dershowitz, N., Finkbeiner, B., Schulte, W. (eds) Fields of Logic and Computation II. Lecture Notes in Computer Science(), vol 9300. Springer, Cham. https://doi.org/10.1007/978-3-319-23534-9_16
Download citation
DOI: https://doi.org/10.1007/978-3-319-23534-9_16
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-23533-2
Online ISBN: 978-3-319-23534-9
eBook Packages: Computer ScienceComputer Science (R0)