The pseudofinite monadic second order theory of finite words

We analyse the pseudofinite monadic second order theory of words over a fixed alphabet. That is we consider the shared monadic second order theory of finite words over a fixed alphabet. In particular we give a straightforward human readable theory which axiomatises the shared monadic second order theory of such words, working in a one-sorted first order framework. To each finite word w we attach a first order structure M(w) expanding the Boolean algebra of subsets of the linear order underlying w. The analysis hinges on the fact that concatenation of finite words interacts nicely with monadic second order logic, particularly for the signature which we adopt. More precisely, we heavily exploit the fact working over this signature, for each natural number k, equivalence of (monadic second order versions of) words with respect to formulas of quantifier depth at most k is a congruence for concatenation. The central result of the paper is a proof that the theory theory which we introduced is indeed an axiomatisation for the pseudofinite monadic second order theory of words. As an application, the property of concatenation described above is then further exploited to present an alternative proof of a theorem connecting recognisable languages and finitely generated free profinite monoids via extended Stone duality, due to Gehrke, Grigorieff, and Pin. Our proof makes no appeals to heavy machinery from duality theory.