Definability and Regularity in Automatic Structures

Abstract

An automatic structure $\mathcal{A}$ is one whose domain A and atomic relations are finite automaton (FA) recognisable. A structure isomorphic to $\mathcal{A}$ is called automatically presentable. Suppose R is an FA recognisable relation on A. This paper concerns questions of the following type. For which automatic presentations of $\mathcal{A}$ is (the image of) R also FA recognisable? To this end we say that a relation R is intrinsically regular in a structure $\mathcal{A}$ if it is FA recognisable in every automatic presentation of the structure. For example, in every automatic structure all relations definable in first order logic are intrinsically regular. We characterise the intrinsically regular relations of some automatic fragments of arithmetic in the first order logic extended with quantifiers ∃ ^∞ interpreted as ‘there exists infinitely many’, and ∃ ⁽ⁱ⁾ interpreted as ‘there exists a multiple of i many’.