Lax Lean Archive

Draft — mutable and not usable as a dependency; its citation marks the draft state.

Lax314295.AperiodicOfFO

First-order definable languages are aperiodic

concepts/Lax314295/AperiodicOfFO.lean · lax-314295

proven

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Concept map

    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    Evidence

    Each proof establishes this claim relative to its assumptions.

    In the paper

    Theorem

    Every language definable in first-order logic is recognised by an aperiodic deterministic automaton (Theorem C.4.11 of Transducers, the implication from definable to aperiodic). A first-order sentence of quantifier rank kk depends only on the kk-type of the string (Lemma C.4.13); the automaton whose states are the kk-types, which is finite and aperiodic by Lemma C.4.15, recognises the language.

    Lean source view on GitHub

    1import Lax765601.StateTransformations
    2import Lax314295.MSOLogic
    3
    4/-!
    5---
    6title: First-order definable languages are aperiodic
    7type: theorem
    8---
    9Every language definable in first-order logic is recognised by an aperiodic
    10deterministic automaton (Theorem C.4.11 of *Transducers*, the implication from
    11definable to aperiodic). A first-order sentence of quantifier rank kk depends
    12only on the kk-type of the string (Lemma C.4.13); the automaton whose states
    13are the kk-types, which is finite and aperiodic by Lemma C.4.15, recognises
    14the language.
    15
    16# Formalization notes
    17
    18A deterministic automaton is mathlib's `DFA`; it is aperiodic if its transition
    19function satisfies the stabilisation condition `TransAperiodic` of
    20`Lax765601.StateTransformations`. The alphabet is assumed finite.
    21-/
    22
    23namespace Lax314295.AperiodicOfFO
    24
    25open Lax765601.StateTransformations Lax314295.MSOLogic
    26
    27/-- A first-order definable language is recognised by an aperiodic dfa. -/
    28axiom exists_aperiodic_dfa_of_foDefinable {A : Type} [Finite A] {L : Language A}
    29 (hL : FODefinable L) :
    30 ∃ (σ : Type) (_ : Finite σ) (M : DFA A σ), TransAperiodic M.step ∧ M.accepts = L
    31
    32end Lax314295.AperiodicOfFO
    33
    Show Proof

    Formalization notes

    A deterministic automaton is mathlib's DFADFA; it is aperiodic if its transition function satisfies the stabilisation condition TransAperiodicTransAperiodic of Lax765601.StateTransformationsLax765601.StateTransformations. The alphabet is assumed finite.

    Builds on

    Used by

    none

    From Mathlib

    none

    Community review

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above; your ORCID profile must share a public name.

    0 comments

    Loading discussion…