Monadic Second-Order Logic

Origin. Büchi (1960) for automata theory. Second-order quantification over sets only. Decidable on trees (Rabin). Captures regular languages. Foundation for automata-logic connection.

Models. Quantify over unary predicates (sets). No quantification over relations. MSO on strings = regular languages. MSO on trees = recognizable tree languages.

Formalism.

Syntax: φ ::= x ∈ X | R(x̄) | ¬φ | φ∧ψ | ∃x.φ | ∃X.φ X: set variable, x: element variable.

MSO on strings: Signature: <, Suc, {Pₐ} ∃X(0 ∈ X ∧ ∀x(x ∈ X → Suc(x) ∈ X)) "Successor-closed set containing 0"

Büchi's theorem: MSO on ω-strings ≡ ω-regular languages ≡ Büchi automata.

Rabin's theorem: MSO on infinite binary trees ≡ tree automata. Decidable (but non-elementary).

Weak MSO (WMSO): Quantify only over finite sets. WMSO on ω-strings = ω-regular (same power).

MSO₁ vs MSO₂ (graphs): MSO₁: quantify over vertex sets. MSO₂: quantify over edge sets too. Different on graphs.

Courcelle's theorem: MSO-definable properties decidable in linear time on bounded treewidth graphs.

Symbols.

Symbol	Unicode	Name	Meaning
X, Y	—	Set variables	Range over subsets of the domain; the only second-order variables
x, y	—	Element variables	Range over the domain
∈	U+2208	Element of	Membership of an element in a set variable
∃	U+2203	Existential quantifier	Applied to element or set variables
∀	U+2200	Universal quantifier	Applied to element or set variables
¬	U+00AC	Negation	Boolean connective
∧	U+2227	Conjunction	Boolean connective
≡	U+2261	Identical to	Equi-expressiveness of logic and automaton class
<	U+003C	Less-than sign	Order on positions of a word
Suc	—	Successor	Successor on positions
Pₐ	—	Letter predicate	"Position x carries the letter a"
MSO	—	Monadic second-order logic	The logic as a whole
MSO₁, MSO₂	—	Graph variants	Quantification over vertex sets; over vertex and edge sets
WMSO	—	Weak MSO	Set quantifiers restricted to finite sets
S1S, S2S	—	Monadic theories	Of one successor; of two successors

Metatheory. The organizing result is the Büchi–Elgot–Trakhtenbrot theorem: over finite words, MSO defines exactly the regular languages, and the translation runs both ways, so logic and automaton are interchangeable presentations. Büchi (1962) extended this to infinite words, proving S1S decidable and MSO-definability equivalent to ω-regularity, and Rabin (1969) proved S2S — the monadic theory of the infinite binary tree — decidable, the deepest result of the family, from which decidability of many modal and temporal logics follows by interpretation. Decidability is not feasibility: Meyer (1975) showed already the weak theory WS1S has a non-elementary lower bound, so no decision procedure runs in time bounded by any fixed tower of exponentials. Composition theorems of Feferman–Vaught type let MSO truth in a structure be computed from truth in its parts, which is what underlies Courcelle's theorem (1990): every MSO₂-definable graph property is decidable in linear time on graphs of bounded treewidth. Seese (1991) supplies the converse direction — a class of graphs with decidable MSO₂ theory has bounded treewidth — so tree-likeness is not merely sufficient for decidability but necessary.

Applies to. Automata theory. Verification (trees). Model checking. Graph algorithms. Regular languages.

Limitations. Decidability is a fact about particular structures, not about the logic: MSO validity over arbitrary structures is not recursively enumerable, and there is no completeness theorem. It collapses as soon as the structure leaves the tree-like case — the MSO theory of (ℕ, +) is undecidable, the MSO theory of the infinite grid is undecidable, and Shelah (1975) proved the monadic theory of the real order undecidable. Seese's theorem says this is not a gap in the techniques: unbounded treewidth means undecidable MSO₂. Where decidability does hold, the non-elementary lower bound means it is unusable except on small formulas, and the linear-time constant in Courcelle's theorem is itself non-elementary in the formula, so the theorem classifies rather than computes. Expressively, only unary second-order variables are available: binary relations cannot be quantified, equicardinality of two sets is not expressible, and MSO₁ and MSO₂ genuinely differ — Hamiltonicity is definable with edge-set quantification and not with vertex-set quantification alone.