Choice functions and well-orderings over the infinite binary tree

Arnaud Carayol; Christof Löding; Damian Niwinski; Igor Walukiewicz

Open Mathematics (2010)

  • Volume: 8, Issue: 4, page 662-682
  • ISSN: 2391-5455

Abstract

top
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 show how the result can be used to prove the inherent ambiguity of languages of infinite trees. 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.

How to cite

top

Arnaud Carayol, et al. "Choice functions and well-orderings over the infinite binary tree." Open Mathematics 8.4 (2010): 662-682. <http://eudml.org/doc/269264>.

@article{ArnaudCarayol2010,
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 show how the result can be used to prove the inherent ambiguity of languages of infinite trees. 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.},
author = {Arnaud Carayol, Christof Löding, Damian Niwinski, Igor Walukiewicz},
journal = {Open Mathematics},
keywords = {Monadic second-order logic; Definability; Choice function; monadic second-order logic; definability; choice function},
language = {eng},
number = {4},
pages = {662-682},
title = {Choice functions and well-orderings over the infinite binary tree},
url = {http://eudml.org/doc/269264},
volume = {8},
year = {2010},
}

TY - JOUR
AU - Arnaud Carayol
AU - Christof Löding
AU - Damian Niwinski
AU - Igor Walukiewicz
TI - Choice functions and well-orderings over the infinite binary tree
JO - Open Mathematics
PY - 2010
VL - 8
IS - 4
SP - 662
EP - 682
AB - 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 show how the result can be used to prove the inherent ambiguity of languages of infinite trees. 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.
LA - eng
KW - Monadic second-order logic; Definability; Choice function; monadic second-order logic; definability; choice function
UR - http://eudml.org/doc/269264
ER -

References

top
  1. [1] Arnold A., Rational ω-languages are nonambiguous, Theoret. Comput. Sci., 1983, 26(1–2), 221–223 http://dx.doi.org/10.1016/0304-3975(83)90086-5[Crossref] 
  2. [2] Büchi J.R., On a decision method in restricted second order arithmetic, In: Proceedings of International Congress on Logic, Methodology and Philosophy of Science, Stanford University Press, Stanford, 1962, 1–11 Zbl0147.25103
  3. [3] Büchi J.R., Landweber L.H., Solving sequential conditions by finite-state strategies, Trans. Amer. Math. Soc., 1969, 138, 295–311 Zbl0182.02302
  4. [4] Carayol A., Wöhrle S., The Caucal hierarchy of infinite graphs in terms of logic and higher-order pushdown automata, In: Proceedings of the 23rd Conference on Foundations of Software Technology and Theoretical Computer Science, FST TCS 2003, Lecture Notes in Computer Science, 2914, Springer, Berlin, 2003, 112–123 Zbl1205.03022
  5. [5] Carayol A., Löding C., MSO on the infinite binary tree: choice and order, In: Proceedings of the 16th Annual Conference of the European Association for Computer Science Logic, CSL 2007, Lecture Notes in Computer Science, 4646, Springer, Berlin, 2007, 161–176 Zbl1179.03016
  6. [6] Caucal D., On infinite terms having a decidable monadic theory, In: Proceedings of the 27th International Symposium on Mathematical Foundations of Computer Science, MFCS 2002, Lecture Notes in Computer Science, 2420, Springer, Berlin, 2002, 165–176 Zbl1014.68077
  7. [7] Church A., Logic, Arithmetic and Automata, In: Proceedings of the International Congress of Mathematicians (Stockholm 1962), Inst. Mittag-Leffler, Djursholm, 1963, 23–35 
  8. [8] Dawar A., Grädel E., The descriptive complexity of parity games, In: Proceedings of the 17th Annual Conference on Computer Science Logic, CSL 2008, Lecture Notes in Computer Science, 5213, Springer, Berlin, 2008, 354–368 [Crossref] Zbl1157.68032
  9. [9] Ebbinghaus H.-D., Flum J., Finite Model Theory, Perspectives in Mathematical Logic, Springer, Berlin, 1995 Zbl0841.03014
  10. [10] Grädel E., Thomas W., Wilke T., Automata, Logics, and Infinite Games, Lecture Notes in Computer Science, 2500, Springer, Berlin, 2002 
  11. [11] Gurevich Y., Shelah S., Rabin’s uniformization problem, J. Symbolic Logic, 1983, 48(4), 1105–1119 http://dx.doi.org/10.2307/2273673[Crossref] Zbl0537.03007
  12. [12] Kähler D., Wilke T., Complementation, disambiguation, and determinization of Büchi automata unified, In: Proceedings of the 35th International Colloquium on Automata, Languages and Programming, ICALP 2008, Part I, Lecture Notes in Computer Science, 5125, Springer, Berlin, 2008, 724–735 Zbl1153.68032
  13. [13] Lifsches S., Shelah S., Uniformization, choice functions and well orders in the class of trees, J. Symbolic Logic, 1996, 61(4), 1206–1227 http://dx.doi.org/10.2307/2275812[Crossref] Zbl0872.03005
  14. [14] Lifsches S., Shelah S., Uniformization and Skolem functions in the class of trees, J. Symbolic Logic, 1998, 63(1), 103–127 http://dx.doi.org/10.2307/2586591[Crossref] Zbl0899.03010
  15. [15] Löding C., Automata and Logics over Infinite Trees, Habilitationsschrift, RWTH Aachen, 2009 
  16. [16] McNaughton R., Testing and generating infinite sequences by a finite automaton, Information and Control, 1966, 9(5), 521–530 http://dx.doi.org/10.1016/S0019-9958(66)80013-X[Crossref] Zbl0212.33902
  17. [17] Monti A., Peron A., Systolic tree ω-languages: the operational and the logical view, Theoret. Comput. Sci., 2000, 233(1–2), 1–18 http://dx.doi.org/10.1016/S0304-3975(97)00257-0[Crossref] Zbl0952.68081
  18. [18] Mostowski A.W., Regular expressions for infinite trees and a standard form of automata, In: Computation Theory, Lecture Notes in Computer Science, 208, Springer, Berlin, 1984, 157–168 
  19. [19] Rabin M.O., Decidability of second-order theories and automata on infinite trees, Trans. Amer. Math. Soc., 1969, 141, 1–35 Zbl0221.02031
  20. [20] Rabin M.O., Automata on Infinite Objects and Church’s Problem, American Mathematical Society, Boston, 1972 Zbl0315.02037
  21. [21] Rabinovich A., On decidability of monadic logic of order over the naturals extended by monadic predicates, Inform. and Comput., 2007, 205(6), 870–889 http://dx.doi.org/10.1016/j.ic.2006.12.004[WoS][Crossref] Zbl1115.68100
  22. [22] Safra S., On the complexity of ω-automata, In: Proceedings of the 29th Annual Symposium on Foundations of Computer Science, FoCS 1988, IEEE Computer Society Press, Los Alamitos, 1988, 319–327 http://dx.doi.org/10.1109/SFCS.1988.21948[Crossref] 
  23. [23] Seidl H., Deciding equivalence of Finite tree automata, SIAM J. Comput., 1990, 19(3), 424–437 http://dx.doi.org/10.1137/0219027[Crossref] 
  24. [24] Semenov A.L., Decidability of monadic theories, In: Proceedings of the 11th International Symposium on Mathematical Foundations of Computer Science, MFCS 1984, Lecture Notes in Computer Science, 176, Springer, Berlin, 1984, 162–175 Zbl0553.03005
  25. [25] Siefkes D., The recursive sets in certain monadic second order fragments of arithmetic, Arch. Math. Logik Grundlagenforsch., 1975, 17(1–2), 71–80 http://dx.doi.org/10.1007/BF02280817[Crossref] Zbl0325.02033
  26. [26] Stearns R.E., Hunt H.B., On the equivalence and containment problems for unambiguous regular expressions, regular grammars and finite automata, SIAM J. Comput., 1985, 14(3), 598–611 http://dx.doi.org/10.1137/0214044[Crossref] Zbl0577.68074
  27. [27] Thomas W., Automata on infinite objects, In: Handbook of Theoretical Computer Science, B: Formal Models and Semantics, Elsevier, Amsterdam, 1990, 133–191 
  28. [28] Thomas W., On the synthesis of strategies in infinite games, In: Proceedings of the 12th Annual Symposium on Theoretical Aspects of Computer Science, STACS’ 95, Lecture Notes in Computer Science, 900, Springer, Berlin, 1995, 1–13 
  29. [29] Thomas W., Languages, automata, and logic, In: Handbook of Formal Language Theory, 3, Springer, Berlin, 1997, 389–455 
  30. [30] Thomas W., Church’s problem and a tour through automata theory, In: Pillars of Computer Science, Essays Dedicated to Boris (Boaz) Trakhtenbrot on the Occasion of His 85th Birthday, Lecture Notes in Computer Science, 4800, Springer, Berlin, 2008, 635–655 

NotesEmbed ?

top

You must be logged in to post comments.

To embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.

Only the controls for the widget will be shown in your chosen language. Notes will be shown in their authored language.

Tells the widget how many notes to show per page. You can cycle through additional notes using the next and previous controls.

    
                

                
Note: Best practice suggests putting the JavaScript code just before the closing </body> tag.