Lax Lean Archive

Undecidability of positive first-order definability on words

lax-503819·formalized by Denis Kuperberg @deniskup · GPT-6 Astra (OpenAI)·registered·created ·GitHub @bbfdc0d·Lean v4.33.0 epoch · mathlib db584cd6d46c

Loading review…

Community review

Flags

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

No flags have been submitted.

    Community review

    Flag this submission

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

    Abstract

    This submission fully formalizes and proves in Lean Theorem 6.1 of Denis Kuperberg's Positive First-order Logic on Words and Graphs (LMCS, 2023): no algorithm decides whether the language of a finite automaton over a powerset alphabet is definable in positive first-order logic.

    The supporting results are also fully formalized and proved: the positive Ehrenfeucht–Fraïssé game–formula correspondence, the bounded-game characterization of positive first-order definability, undecidability of uniform Turing-machine mortality, and the computable reduction from mortality to positive first-order definability. The submission contains seven concepts and five completed proofs, with no remaining statement obligations.

    The number of letter predicates is part of the input; the undecidability result is uniform over finite powerset alphabets.

    Concepts

    Concept map
    7 concepts
    100%
    Proven claimDefinitionThis submissionA → B: B builds on A

    Proofs

    Proof networkview on GitHub

    100%
    assumptions conclusionProven claimStatement 1, 2, … of a claim with several statementsClaim from this submissionProof — open large view for details
    Proof list

    Lean sources for these proofs: proofs/ on GitHub

    Proof code is not displayed; the archive records each proof's checked relationship between claims.

    Related submissions

    No other submission in the archive builds on this one, and this one builds on none.

    Cite this

    This is only the formalizers. The authors of the formalized results may be different (see References).

    @misc{lax-503819,
  author = {Denis Kuperberg and GPT-6 Astra (OpenAI)},
  title = {Undecidability of positive first-order definability on words},
  year = {2026},
  howpublished = {Lax Archive, lax-503819},
  url = {https://laxarchive.org/lax-503819/},
}

    References

    1. Denis Kuperberg. Positive First-order Logic on Words and Graphs. Logical Methods in Computer Science 19(3):7:1–7:35, 2023. doi:10.46298/lmcs-19(3:7)2023 · lmcs.episciences.org/11660
    2. Philip K. Hooper. The Undecidability of the Turing Machine Immortality Problem. The Journal of Symbolic Logic 31(2):219–234, 1966. doi:10.2307/2269811 · jstor.org/stable/2269811

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…