Ehrenfeucht games, the composition method, and the monadic theory of ordinal words. (English) Zbl 0888.03002

Mycielski, Jan (ed.) et al., Structures in logic and computer science. A selection of essays in honor of Andrzej Ehrenfeucht (65th birthday on August 8, 1997). Berlin: Springer. Lect. Notes Comput. Sci. 1261, 118-143 (1997).
The algorithmic decidability of the monadic second-order theories of natural numbers and words was shown by automata-theoretic methods, which were taken up by many researchers and turned out successful especially in the context of theoretical computer science, regarding areas like formal language theory, program verification, concurrency theory.
The deciding algorithms for monadic theories of ordinal numbers with linear order were found on the base of the set-theoretic Ehrenfeucht-Fraïssé technique called “composition method”.
In this article, the “composition” theorem of Shelah and Gurevich on monadic theories of concatenated orderings is proved in a new form. Shelah’s (automata-free) set-theoretical proof of Büchi’s theorem on the decidability of the second-order monadic theory of the natural numbers with linear order is recapitulated. It is shown that 1) even the monadic first-order theory of an ordinal ordering with \(n\) recursive unary predicates can be undecidable, 2) complexity of such a theory belongs to the \(2n\)-th level of the arithmetical Kleene-Mostowski hierarchy and this bound cannot be improved.
For the entire collection see [Zbl 0868.00014].
Reviewer: A.Nabebin (Moskva)


03B25 Decidability of theories and sets of sentences
03D05 Automata and formal grammars in connection with logical questions
03C07 Basic properties of first-order languages and structures
03B15 Higher-order logic; type theory (MSC2010)