Proof of `Aperiodic automata recognise first-order definable languages`
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
The language of an aperiodic dfa is first-order definable (Theorem C.4.11, the converse implication): the aperiodic Krohn–Rhodes decomposition into flip-flops (, right to left).
Proof strategy
The source turns the dfa into an aperiodic Mealy machine, decomposes it by Theorem A.2.13 into flip-flops and letter-to-letter maps, describes each prime in first-order logic and composes the descriptions by substitution of formulas (, ). The bridge transports along .
Attribution
Theorem C.4.11 of Transducers, Part C; formalised by Aristotle (Harmonic), , , .