Tags:
, view all tags
Buchi's Theorem

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

Proof

Let L be a regular language with associated DFA D = (Q, q1, δ, 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 = {q1, q2,..., qn).

Φ can be described as: ∃C1∃C2...∃Cn: ∀x: ( should be in some state) ∧ ( can be in only 1 state) ∧ (zero(x) → start at q1) ∧ ( follow the right transitions) ∧ (last(x) → end at a final state)

• should be in some state: [C1(x) ∨ C2(x) ∨ ... ∨ Cn(x)]
• can be in only 1 state: for every pair of states qi, qj, add the following: [Ci(x) → ¬Cj(x)]. Connect these together with ∧.
• start at q1: C1(x)
• follow the right transitions: for every transition δ(qi, a) = qj, add the following: [(Ci(x) ∧ Ia(x)) → Cj(x+1)]. Connect these together with ∧.
• end at a final state: for every transition δ(qi, a) = qj such that qj∈F, add the following: [Ia(x) ∧ Ci(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.   Edit Attach 