# Using logic to prove non-regularity of a language

A language $L$ is regular if and only if it is definiable by a sentence in monadic second order logic (MSO) over strings (J.R. Buchi, Weak second-order arithmetic and Finite automata; Z. Math. Logik Grundlagen Math. 6 (1960) 66-92).

1. Are there proofs of non-regularity of a language $L$ (e.g. $L = \{ a^n b^n \}$) that are based on the non expressibility in MSO of $L$?
2. What are the (logic) techniques (if any) that can be used?

I googled a little bit, but didn't find anything relevant (but I'm not an expert, so I'm probably using the wrong terms).

• Everything I've found (in a non-exhaustive search) goes the other way - using non-regularity to show inexpressibility in MSO. Even Ebbinghaus & Flum's "Finite Model Theory" only has examples in that direction (if you have it handy, Chapter 7, pp. 112-113, 2nd Ed.). Jan 19, 2016 at 0:33
• I agree with @luke-mathieson . All examples I know go the other way. If that helps, note that, over strings, MSO = $\exists$MSO. Thus it would suffice to prove non expressibility in $\exists$MSO. Jan 19, 2016 at 18:38
• The usual way to directly show something is not expressible in descriptive complexity/finite model theory is to use some variation of Ehrenfeucht-Fraisse games. Feb 8, 2016 at 12:57
• But in a way also Büchi was working the other way. Not per sé interested in the regualr languages, but in applying their decidability to MSO logic? Mar 18, 2016 at 16:54
• This essay defines EF games for MSO definable formulas. While it shows only that the class of finite structures is not MSO-definable (which doesn't correspond to a non-regular language), perhaps an argument can be made to show that $\{ 0^n 1^n \mid n \in \mathbb{N}\}$ is not MSO-definable, just by showing the duplicator wins the $n$-turn game on strings $0^n 1^n$ and $0^{n+1} 1^{n+1}$. Apr 12, 2017 at 9:02