Proof of `First-order definable languages are aperiodic`
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 first-order definable language is recognised by an aperiodic dfa (Theorem C.4.11, the first implication): the automaton of -types (, left to right).
Proof strategy
The source takes a first-order sentence of quantifier rank defining , recognises by the dfa whose states are the -types (Lemma C.4.13 says the type determines satisfaction, Lemma C.4.15 that the types form an aperiodic congruence, ). The bridge transports along ; unfolds identically.
Attribution
Theorem C.4.11 of Transducers, Part C; formalised by Aristotle (Harmonic), , , .