In this thesis, we establish the connection between recognizable languages and monadic second-order logic over the successor signature, denoted by $\textbf{MSO}[\mathcal{L}_S]$. We introduce the basic concepts of formal language theory, regular expressions and finite automata, and present monadic second-order logic together with its interpretation over words.
Using Arden's lemma and the closure properties of recognizable and regular languages, we prove Kleene's theorem, which states that the classes of regular and recognizable languages coincide. Büchi's theorem establishes the equivalence between recognizable languages and the languages definable in $\textbf{MSO}[\mathcal{L}_S]$. In the proof, we first show that every recognizable language can be described by a sentence of monadic second-order logic. Conversely, we associate each formula with free variables with a language of marked words over an extended alphabet and prove, by induction on the structure of the formula, that all such languages are regular. Regularity for atomic formulas is verified directly, while for logical connectives and quantifiers we use the closure of regular languages under union, intersection, complement, and homomorphisms. Hence every language definable in $\textbf{MSO}[\mathcal{L}_S]$ is recognizable.
This yields a complete characterization of recognizable languages in terms of formulas of monadic second-order logic, which is one of the fundamental results in the theory of formal languages and automata.
|