In this page we prove the implication from 2 to 3 in the Schützenberger theorem. This implication says that if a language is definable in first-order logic, then its syntactic monoid is aperiodic. The key lemma is given below.
Lemma 0. If is definable in first-order logic, then it is recognised by a morphism into a finite and aperiodic monoid.
From the above lemma it follows that if is definable in first-order logic, then its syntactic monoid is aperiodic. This is because, by Theorem 2 on syntactic monoids, the syntactic monoid is a homomorphic image of a submonoid of any monoid recognising . Since taking submonoids and homomorphic images preserves aperiodicity, Lemma 0 implies that the syntactic monoid of is aperiodic.
Types. Define the quantifier rank of a formula of first-order logic to be the nesting depth of quantifiers. Formulas of quantifier rank at most are closed under Boolean combinations, while applying a quantifier causes the rank to increase. For a natural number , define the -type of a word to be the set of sentences (i.e. formulas without free variables) of quantifier rank at most that are true in . By convention, we assume that all words have the same -type.
Theorem. For every alphabet and natural number , the function that maps a word to its -type is compositional.
Proof hint. One way to prove this would be using the Ehrenfeucht-Fraisse method, which can be found in Phokion Kolatis’ slides here, beginning with page 16.
Corollary. For every , there are finitely many different -types, and and have the same -type for every word .
Proof. Define the -profile of a word to be the set of triples such that there exists a decomposition where the -types of and are and , respectively. From compositionality of -types it follows that for every , the -type is determined by the -profile. The two statements in the corollary can then be proved by induction on . .
We can now prove Lemma 0. Suppose that is definable in first-order logic, by a formula of quantifier rank . Let be the set of -types. By the Theorem on compositionality above, and by the lemma on compositional mappings here, it follows that there is a monoid operation on such that the function which maps a word to its -type is a monoid morphism. Furthermore, by the corollary above, the monoid is finite and aperiodic.