Ehrenfeucht games, the composition method, and the monadic theory of ordinal words

When Ehrenfeucht introduced his game theoretic characterization of elementary equivalence in 1961, the first application of these “Ehrenfeucht games” was to show that certain ordinals (considered as orderings) are indistinguishable in first-order logic and weak monadic second-order logic. Here we review Shelah's extension of the method, the “composition of monadic theories”, explain it in the example of the monadic theory of the ordinal ordering (ω, <), and compare it with the automata theoretic approach due to Büchi. We also consider the expansion of ordinals by recursive unary predicates (which gives “recursive ordinal words”). It is shown that the monadic theory of a recursive ωn-word belongs to the 2n-th level of the arithmetical hierarchy, and that in general this bound cannot be improved.