A language is definable in second-order monadic logic if and only if it is regular.

Proof

Regular → Second-order monadic

Let L be a regular language with associated DFA D = (Q, q₁, δ, F). We construct a formula Φ describing an accepting run of D on a string (Φ is true iff there is an accepting run of D on the string).

Let Q = {q₁, q₂,..., q_n).

Φ can be described as: ∃C₁∃C₂...∃C_n: ∀x: ( should be in some state) ∧ ( can be in only 1 state) ∧ (zero(x) → start at q₁) ∧ ( follow the right transitions) ∧ (last(x) → end at a final state)

• should be in some state: [C₁(x) ∨ C₂(x) ∨ ... ∨ C_n(x)]
• can be in only 1 state: for every pair of states q_i, q_j, add the following: [C_i(x) → ¬C_j(x)]. Connect these together with ∧.
• start at q₁: C₁(x)
• follow the right transitions: for every transition δ(q_i, a) = q_j, add the following: [(C_i(x) ∧ I_a(x)) → C_j(x+1)]. Connect these together with ∧.
• end at a final state: for every transition δ(q_i, a) = q_j such that q_j∈F, add the following: [I_a(x) ∧ C_i(x)]. Connect these together with ∨.

Second-order monadic → Regular

-- SvorotnI - 2012-04-22