Proof of `MSO-definable languages are regular`
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
An mso-definable language is regular (Theorem C.4.1, Büchi's theorem, the easy implication): the automaton of a sentence, by induction on the formula (, right to left).
Proof strategy
The source builds, for every formula, the automaton of the annotated strings that satisfy it (Lemma C.4.2, ) and projects the annotation away for a sentence (). The concept's formulas are the source's through the bijection /, along which satisfaction is transported (), so transfers by .
Attribution
Theorem C.4.1 of Transducers, Part C; formalised by Aristotle (Harmonic), , .