Existential quantification over regular predicates A regular language over an alphabet $\Sigma$ is a subset of the set of all words over $\Sigma$ that can be accepted by some finite automaton. A regular language identifies a certain property of strings of $\Sigma^*$.
One can then define a regular predicate over $\Sigma^*$
as an n-ary relation on $\Sigma^*$ such that by suitably coding n-tuples of words as single words (see for example Blumensath and Gradel) one obtains a regular language (over a new alphabet). If $R(x,y)$ is a regular binary predicate, what can be the status of the unary predicate $\exists x.R(x,y)$? (again regular, decidable, r.e., or what else?)
 A: That is a central point about automatic structures: By projection (“existential quantification”) you get another regular predicate, and regular predicates are also closed under intersection and complementation. Consequently, the first-order theories of automatic structures are decidable (because you can decide for a given automaton whether he accepts any word).
The proof is quite simple: You want to project $x$ away—just simulate every possible input for $x$ in parallel using sets of states of the old automaton as states for the new automaton (it remains a finite state machine, since the power set of a finite set is finite).
As conjectured above you can also prove it using the MSO translation, let me sketch it: You have regular predicate $R(x,y)$ defined using a MSO formula. This MSO formula uses relation symbols $X_{(a,b)}$ to refer to “the set of positions where $x$ has character $a$ and $y$ has character $b$”. For the projection add existential second-order quantifiers $\exists Q_1\ldots Q_n$ (where $\Sigma=\left\{1,\ldots,n\right\}$) and replace the occurencesof $X_{(a,b)}$ by $X_b\wedge Q_a$ and add an expression expressing that the sets $Q_a$ build a partition. This is not yet correct, because it does not consider different lengths of $x$ and $y$ and we have to deal with some trailing characters, but that is as easy. However–the whole MSO-based proof is much more complicated than constructing an automaton directly.
Notice that both proofs can be transfered to $\omega$-automata and finite and infinite tree-automata.
A: I think I found a reference for the answer. It should be in the following paper:
S. Eilemberg, C.C. Elgot, J.C. Shepherdson, Sets recognized by n-tape automata, Journal of Algebra, vol. 13, (1969), pp. 447-464. 
Unfortunately I cannot download it from the internet.
A: I believe that this is Theorem 1.4.6 (predicate calculus) in the book "Word processing in groups".  However, I find their discussion somewhat confusing -- I came here hoping for a better reference...
