The pseudofinite monadic second order theory of words

TL;DR

This paper studies the pseudofinite monadic second order theory of words, providing an axiomatisation and exploring its interaction with concatenation, with implications for recognisable languages and profinite monoids.

Contribution

It offers a new axiomatisation of the pseudofinite monadic second order theory of words within a first-order framework and links it to recognisable languages via Stone duality.

Findings

Equivalence of words under MSO formulas of bounded quantifier depth is a congruence for concatenation.

Provided an alternative proof connecting recognisable languages and profinite monoids.

Analyzed the interaction between concatenation and monadic second order logic.

Abstract

We analyse the pseudofinite monadic second order theory of words over a fixed finite alphabet. In particular we present an axiomatisation of this theory, working in a one-sorted first order framework. The analysis hinges on the fact that concatenation of words interacts nicely with monadic second order logic. More precisely, give a signature under which 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. We use our analysis 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.