Proof of `Regular languages are MSO-definable`
What this proof establishes
no assumptions
Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.
Description
A regular language is mso-definable (Theorem C.4.1, Büchi's theorem, the converse implication): the sentence guessing an accepting run of a dfa as a tuple of sets of positions (, left to right).
Proof strategy
The source writes down the sentence "there are sets , one per state, partitioning the positions, consistent with the transition function at every step and accepting at the end" (); the bridge transports along ().
Attribution
Theorem C.4.1 of Transducers, Part C; formalised by Aristotle (Harmonic), , .