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	Unary predicates
∈	U+2208	Membership	Element of set
∃X	—	Set quantifier	Over sets
MSO	—	Monadic SO	Fragment

Metatheory. Decidable on trees (Rabin). Regular language equivalence. Non-elementary complexity. Composition theorems. Courcelle's theorem.

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

Limitations. Non-elementary complexity. Only unary predicates. Full SO undecidable. Graphs without structure hard.