Abstract
A natural framework for real-time specification is monadic first-order logic over the structure (ℝ, < , + 1)—the ordered real line with unary + 1 function. Our main result is that (ℝ, < , + 1) has the 3-variable property: every monadic first-order formula with at most 3 free variables is equivalent over this structure to one that uses 3 variables in total. As a corollary we obtain also the 3-variable property for the structure (ℝ, < ,f) for any fixed linear function f:ℝ → ℝ. On the other hand, we exhibit a countable dense linear order (E, < ) and a bijection f:E → E such that (E, < ,f) does not have the k-variable property for any k.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Dawar, A.: How many first-order variables are needed on finite ordered structures? In: We Will Show Them! Essays in Honour of Dov Gabbay, vol. 1, pp. 489–520. College Publications (2005)
Gabbay, D.M.: Expressive functional completeness in tense logic. In: Mönnich, U. (ed.) Aspects of Philosophical Logic, pp. 91–117. Reidel, Dordrecht (1981)
Gabbay, D.M., Pnueli, A., Shelah, S., Stavi, J.: On the temporal basis of fairness. In: POPL, pp. 163–173. ACM Press (1980)
Grohe, M., Schweikardt, N.: The succinctness of first-order logic on linear orders. Logical Methods in Computer Science 1(1) (2005)
Hirshfeld, Y., Rabinovich, A.: Continuous time temporal logic with counting. Inf. Comput. 214, 1–9 (2012)
Hirshfeld, Y., Rabinovich, A.M.: Timer formulas and decidable metric temporal logic. Inf. Comput. 198(2), 148–178 (2005)
Hodges, W.: A Shorter Model Theory. Cambridge University Press, New York (1997)
Hodkinson, I., Simon, A.: The k-variable property is stronger than H-dimension k. Journal of Philosophical Logic 26(1), 81–101 (1997)
Hunter, P.: When is metric temporal logic expressively complete? In: CSL. LIPIcs, vol. 23, pp. 380–394. Schloss Dagstuhl (2013)
Hunter, P., Ouaknine, J., Worrell, J.: Expressive completeness for metric temporal logic. In: LICS, pp. 349–357. IEEE Computer Society Press (2013)
Immerman, N.: Upper and lower bounds for first order expressibility. J. Comput. Syst. Sci. 25(1), 76–98 (1982)
Immerman, N., Kozen, D.: Definability with bounded number of bound variables. Inf. Comput. 83(2), 121–139 (1989)
Kamp, H.: Tense Logic and the Theory of Linear Order. PhD thesis, University of California (1968)
Poizat, B.: Deux ou trois choses que je sais de L n . J. Symb. Log. 47(3), 641–658 (1982)
Rossman, B.: On the constant-depth complexity of k-clique. In: STOC, pp. 721–730. ACM (2008)
Venema, Y.: Expressiveness and completeness of an interval tense logic. Notre Dame Journal of Formal Logic 31(4), 529–547 (1990)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Antonopoulos, T., Hunter, P., Raza, S., Worrell, J. (2015). Three Variables Suffice for Real-Time Logic. In: Pitts, A. (eds) Foundations of Software Science and Computation Structures. FoSSaCS 2015. Lecture Notes in Computer Science(), vol 9034. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-46678-0_23
Download citation
DOI: https://doi.org/10.1007/978-3-662-46678-0_23
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-662-46677-3
Online ISBN: 978-3-662-46678-0
eBook Packages: Computer ScienceComputer Science (R0)