Buchi's Theorem
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_{1}, δ, 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_{1}, q_{2},..., q_{n}).
Φ can be described as: ∃C_{1}∃C_{2}...∃C_{n}: ∀x: ( should be in some state) ∧ ( can be in only 1 state) ∧ (zero(x) → start at q_{1}) ∧ ( follow the right transitions) ∧ (last(x) → end at a final state)
- should be in some state: [C_{1}(x) ∨ C_{2}(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_{1}: C_{1}(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 ∨.
zero(x) - x is the beginning of the string,
(x+1), and
last(x) - x is the end of the string, can be easily described in first-order logic.
Second-order monadic → Regular
-- SvorotnI - 2012-04-22