# 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?)

-
The set '$\{ y : (\exists x)[R(x,y)] \}$' is also regular. This is a consequence of the more general fact that if $S$ is a regular set, then any set first-order definable from $S$ is regular. Indeed, all sets that are definable from $S$ in a first-order manner together with the quantifier "there exists infinitely many" and the quantifiers "there exist $k$-many mod $n$" is regular. –  Asher M. Kach Jun 28 '12 at 16:30
Asher, I would recommend you to post your comment as an answer, especially if you could sketch the proof (e.g. by mentioning how the pumping lemma allows you to cut the existential search down). –  Joel David Hamkins Jun 28 '12 at 19:04
Thank you for the answer. I don't know why I've never seen this kind of closure property being treated in a formal language/computability theory course, while it is always explained for the case of recursively enumerable predicates. @Joel: thanks for your point, I would like to see a sketch of the proof. Can it be found in some textbook? I think it would be nice to show this to students. –  Alberto Jun 28 '12 at 21:42
Can one not prove this from the equivalence of MSO with regular languages? –  Benjamin Steinberg Jun 29 '12 at 1:59
@Joel Why do you want to use the pumping lemma? Pumping arguments are used to prove that a language is not regular. In this case there is simply a straight-forward construction of an automaton for the projection of $R$ given an automaton for $R$. –  The User May 29 '13 at 23:36

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.

-

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.