Abstract
Since the work of Rabin [9], it has been known that any monadic second order property of the (labeled) binary tree with successor functions (and not the prefix ordering) is a monadic Δ3 property. In this paper, we show this upper bound is optimal in the sense that there is a monadic Σ2 formula, stating the existence of a path where a given predicate holds infinitely often, which is not equivalent to any monadic Σ2 formula. We even show that some monadic second order definable properties of the binary tree are not definable by any boolean combination of monadic Σ2 and Σ2 formulas.
These results rely in particular on applications of Ehrenfeucht-Fraïssé like game techniques to the case of monadic Σ2 formulas.
supported by a TMR-GETGRATS grant of the University of Bordeaux I
supported by a by a TMR-Marie Curie grant of the EU
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
Preview
Unable to display preview. Download preview PDF.
References
H.D. Ebbinghaus, J. Flum, and W. Thomas. Mathematical Logic. Undergraduate Texts in Mathematics. Springer-verlag, 1984.
E. Emerson. Temporal and modal logic. In J. Van Leeuwen, editor, Handbook of Theor. Comp. Science (vol. B), pages 995–1072. Elsevier, 1990.
R. Fagin. Generalized first-order spectra and polynomial-time recognizable sets. In Complexity of Computation, volume 7. SIAM-AMS, 1974.
R. Fagin. Comparing the power of monadic NP games. Mathematical Logic Quarterly, 43(4):431–455, 1997.
T. Hafer. On the boolean closure of Büchi tree automaton definable sets of ω-trees. Technical report, Aachener Infor. Ber. Nr. 87-16, RWTH Aachen, 1987.
W. Hanf. Model-theoretic methods in the study of elementary logic. In L. Henkin J. Addison and A. Tarski, editors, The theory of models, pages 132–145, Amsterdam, 1965. North Holland.
D. Kozen. Results on the propositional μ-calculus. Theoretical Comp. Science, 27:333–354, 1983.
G. Lenzi. The Mu-calculus and the Hierarchy Problem. PhD thesis, Scuola Normale Superiore, Pisa, 1997.
M. O. Rabin. Decidability of second order theories and automata on infinite trees. Trans. Amer. Math. Soc., 141, 1969.
M. O. Rabin. Weakly definable relations and special automata. In Mathematical Logic and Foundation of Set Theory. North Holland, 1970.
J. R. Shoenfield. Mathematical Logic. Addison-Wesley, Reading, Mass., 1967.
W. Thomas. Automata on infinite objects. In J. Van Leeuwen, editor, Handbook of Theor. Comp. Science (vol. B), pages 133–191. Elsevier, 1990.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Janin, D., Lenzi, G. (1999). On the Structure of the Monadic Logic of the Binary Tree. In: Kutyłowski, M., Pacholski, L., Wierzbicki, T. (eds) Mathematical Foundations of Computer Science 1999. MFCS 1999. Lecture Notes in Computer Science, vol 1672. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48340-3_28
Download citation
DOI: https://doi.org/10.1007/3-540-48340-3_28
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66408-6
Online ISBN: 978-3-540-48340-3
eBook Packages: Springer Book Archive