The main result of this paper states that the isomorphism problem for ω-automatic trees of finite height is at least has hard as second-order arithmetic and therefore not analytical. This strengthens a recent result by Hjorth, Khoussainov, Montalbán, and Nies showing that the isomorphism problem for ω-automatic structures is not in . Moreover, assuming the continuum hypothesis CH, we can show that the isomorphism problem for ω-automatic trees of finite height is recursively equivalent with second-order arithmetic. On the way to (...) our main results, we show lower and upper bounds for the isomorphism problem for ω-automatic trees of every finite height: It is decidable , for height 1 , -hard and in for height 3, and - and -hard and in for height . All proofs are elementary and do not rely on theorems from set theory. (shrink)

The first-order theory of a string automatic structure is known to be decidable, but there are examples of string automatic structures with nonelementary first-order theories. We prove that the first-order theory of a string automatic structure of bounded degree is decidable in doubly exponential space (for injective automatic presentations, this holds even uniformly). This result is shown to be optimal since we also present a string automatic structure of bounded degree whose first-order theory is hard for 2EXPSPACE. We prove similar (...) results also for tree automatic structures. These findings close the gaps left open in [28] by improving both the lower and the upper bounds. (shrink)

We investigate the extension of monadic second-order logic of order with cardinality quantifiers "there exists uncountably many sets such that... " and "there exists continuum many sets such that... ". We prove that over the class of countable linear orders the two quantifiers are equivalent and can be effectively and uniformly eliminated. Weaker or partial elimination results are obtained for certain wider classes of chains. In particular, we show that over the class of ordinals the uncountability quantifier can be effectively (...) and uniformly eliminated. Our argument makes use of Shelah's composition method and Ramsey-like theorem for dense linear orders. (shrink)