A Gandy Theorem for Abstract Structures and Applications to First-Order Definability

We establish a Gandy theorem for a class of abstract structures and deduce some corollaries, in particular the maximal definability result for arithmetical structures in the class. We also show that the arithmetical structures under consideration are biinterpretable (without parameters) with the standard model of arithmetic. As an example we show that for any k >= 3 a predicate on the quotient structure of the h-quasiorder of finite k-labeled forests is definable iff it is arithmetical and invariant under automorphisms.