Abstract
We give a new proof showing that it is not possible to define in monadic second-order logic (MSO) a choice function on the infinite binary tree. This result was first obtained by Gurevich and Shelah using set theoretical arguments. Our proof is much simpler and only uses basic tools from automata theory. We discuss some applications of the result concerning unambiguous tree automata and definability of winning strategies in infinite games. In a second part we strengthen the result of the non-existence of an MSO-definable well-founded order on the infinite binary tree by showing that every infinite binary tree with a well-founded order has an undecidable MSO-theory. © Springer-Verlag Berlin Heidelberg 2007.
Cite
CITATION STYLE
Carayol, A., & Löding, C. (2007). MSO on the infinite binary tree: Choice and order. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4646 LNCS, pp. 161–176). Springer Verlag. https://doi.org/10.1007/978-3-540-74915-8_15
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
