Characterising $(aa)^*$ in first order logic

Question

In my descriptive complexity class, we've been asked to find a formula that characterises the language $(aa)^*$ (over the alphabet $\{a\}$) with a first order formula over the language $\{<, P_a\}$.

This was the first class, so I will recall what we've learned to be sure that I understood. To a $L$-formula $\phi$ we associate a language $\mathcal L(\phi)$ which is the class of all $L$-structures in which $\phi$ is valid.

In my case, we then are looking for a $\{<, P_a\}$-formula for which words of even length are models. I guess I have to say in $\phi$ that $<$ is a total order, so that I can interpret the models as words, and that $\forall x, P_a(x)$ to say that all points are labelled as 'a'. But how to say that there has to be an even number of points in the model? The definition of having an even number of points seems recursive, so I get the impression that a formula for $(aa)^*$ should be of infinite length in first-order logic..

Answer 1

Short answer. There is no such first-order formula, you need a monadic second order formula.

Details. This can be proved directly using an Ehrenfeucht-FraÏssé games argument if you want to stay inside logic, but the real answer to your question is the conjunction of three results.

[1] Büchi (1960): A language is monadic second order expressible iff it is regular.
[2] McNaughton-Pappert (1971): A language is first-order expressible iff it is star-free.
Counter-free Automata. Research Monograph 65. With an appendix by William Henneman. MIT Press. p. 48. ISBN 0-262-13076-9.
[3] Schützenberger (1965): A regular language is star-free if and only if its syntactic monoid is aperiodic. On finite monoids having only trivial subgroups

[3] gives an algorithm to decide whether a given regular language is star-free (and hence, first-order expressible, by [2]). Now, the syntactic monoid of $(aa)^*$ is the cyclic group of order $2$, which is not aperiodic. To get a monadic second order formula, you need first to have first order "macros" to express $\min$, $\max$ and $+1$ and then the following second order formula will do the job $$ \exists X\ \forall x\ (\min \in X \wedge \max \notin X) \wedge (x \in X \leftrightarrow x+1 \notin X) $$