The isomorphism problem for ω-automatic trees

The main result of this paper is that the isomorphism problem for ω-automatic trees of finite height is at least as hard as second-order arithmetic and therefore not analytical. This strengthens a recent result by Hjorth, Khoussainov, Montalbán, and Nies [9] showing that the isomorphism problem for ω-automatic structures is not ∑_2^1. 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: (i) It is decidable (∏1^0-complete, resp.) for height 1 (2, resp.), (ii) (∏1^1-hard and in (∏2^1 for height 3, and (iii) (∏(n-3)^1- and (∏(n-3)^1-hard and in (∏(2n-4)^1(assuming CH) for all n ≥ 4. All proofs are elementary and do not rely on theorems from set theory. Complete proofs can be found in [18].