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
If we have a formula with variables x, y, A, B, we can mark a string w with them. Each x and y can mark 1 position in w. A and B can mark sets of positions.
Let string w satisfy formula Φ with free variables x, y, A, B.
Assume a DFA M_{Φ} decides (w, x, y, A, B) satisfies Φ.
- Build an NFA M'_{Φ} that decides (w, y, A, B) satisfies ∃x:Φ. Non-deteministically guess which position is marked by x. Then run M_{Φ} on the input with guessed x.
- Build an NFA M'_{Φ} that decides (w, x, y, B) satisfies ∃A:Φ. For each position non-deterministically guess if it is marked by A. Then run M_{Φ} on the input with guessed A's.
- Build a DFA M'_{Φ} that decides (w, y, A, B) satisfies ∀x:Φ. Check each possible marking with x using M_{Φ}.
- Build a DFA M'_{Φ} that decides (w, x, y, B) satisfies ∀A:Φ. Check each possible marking with A's using M_{Φ}.
Base case: Booleans, (x ≤ y), I
_{a}(x), A(x) are all regular.
-- SvorotnI - 2012-04-22