From Automatic Structures to Borel Structures

We study the classes of Buchi and Rabin automatic structures. For Buchi (Rabin) automatic structures their domains consist of infinite strings (trees), and the basic relations, including the equality relation, and graphs of operations are recognized by Buchi (Rabin) automata. A Buchi (Rabin) automatic structure is injective if different infinite strings (trees) represent different elements of the structure. The first part of the paper is devoted to understanding the automata- theoretic content of the well-known Lowenheim-Skolem theorem in model theory. We provide automata-theoretic versions of Lowenheim-Skolem theorem for Rabin and Buchi automatic structures. In the second part, we address the following two well-known open problems in the theory of automatic structures: Does every Buchi automatic structure have an injective Buchi presentation? Does every Rabin automatic structure have an injective Rabin presentation? We provide examples of Buchi structures without injective Buchi and Rabin presentations. To answer these questions we introduce Borel structures and use some of the basic properties of Borel sets and isomorphisms. Finally, in the last part of the paper we study the isomorphism problem for Buchi automatic structures.