Lax Lean Archive

While this submission is a draft, it cannot be used by other submissions.

Descriptive complexity: games and inexpressibility

lax-945089·formalized by Pierre Senellart @PierreSenellart · Claude (Anthropic)·created ·GitHub @097ef67·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

    The separations proved in the descriptive-complexity library, which need no complexity-theoretic assumption: what the logics of descriptive complexity cannot express. It builds on the NP core registered as lax-904597, the catalog of NP-complete problems lax-799700, and the submissions on logarithmic space (lax-485149), polynomial time (lax-535992), the polynomial hierarchy (lax-564036), polynomial space (lax-134656), and AC⁰ (lax-895169).

    The Ehrenfeucht–Fraïssé game is defined with its method: structures equivalent for n rounds satisfy the same first-order sentences of quantifier depth n. Two strategies are given, on bare sets with at least n elements and, by Ehrenfeucht's theorem, on linear orders with at least 2ⁿ elements. The k-pebble game between two structures is defined as well, with the invariance of k-variable formulas and of inflationary inductions under it.

    This is applied to EVEN, the parity of the universe. It is not first-order definable, even with an order; but one deterministic walk along the order decides it, so FO(≤) ⊊ FO(DTC) ⊆ FO(TC), and a sentence with arithmetic decides it, so FO(≤) ⊊ AC⁰. It is in PTIME and not definable by an inflationary induction without an order, so order-free FO(IFP) does not capture PTIME; and no order-free induction defines a linear order at all. PARITY, the parity of a marked subset, is in L and not first-order definable. Finally EVEN reduces to some problem by a reduction in FO(DTC) and by no first-order reduction: the first-order reductions of these submissions are strictly weaker than logarithmic-space reductions.

    The proofs are those of version 1.2.2 of the library, sliced to what these statements use; they assume the submission's own statements and those of the submissions it requires where they compose. The library and its documentation are at https://github.com/PierreSenellart/descriptive-complexity and https://pierresenellart.github.io/descriptive-complexity/DescriptiveComplexity.html. The Lean code was written with the assistance of several Claude models; the design and the statements are the author's.

    Concepts

    Concept map
    38 concepts
    100%
    First-order logic with partial fixed pointsThe classes L and coLThe classes NL and coNLThe complement of a decision problemFirst-order logic with a deterministictransitive closureFirst-order definability on ordered structuresThe Krom fragment of existentialsecond-order logicProblems given by a property of structuresAtoms in second-order relation variablesFirst-order logic with a transitive closureThe classes PTIME and coPTIMEThe Horn fragment of existentialsecond-order logicFirst-order logic with inflationary fixedpointsAC⁰ as first-order logic with arithmeticRanks in a finite linear order and the BITpredicateComplexity classes, cofinal hardness, and NPFirst-order interpretations and first-orderreductionsDecision problems on finite structuresRelativized first-order interpretationsSecond-order definability with boundedalternationEhrenfeucht–Fraïssé gamesThe Ehrenfeucht–Fraïssé methodEVEN, the parity of the universeCharacterization of EVEN and PARITYEVEN is not first-order definable, even withan orderFO(≤) ⊊ AC⁰: EVEN with arithmeticFO(≤) ⊊ FO(DTC): EVEN is adeterministic walkEhrenfeucht’s theorem on linear ordersFirst-order logic cannot count: games on baresetsNo order-free induction defines a linear orderFirst-order definability without an orderOrder-free FO(IFP) does not capturePTIMEPARITY, the parity of a marked subsetPARITY is in L and not first-order definablePebble games between two structuresInvariance of formulas and inductions underpebble gamesFirst-order reductions are strictly weakerthan logarithmic-space reductionsReductions in first-order logic with adeterministic transitive closure
    Proven claimDefinitionThis submissionOther 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 submission / another 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

    Submission map

    100%
    This submissionOther submissionA → B: B's concepts build on A

    Cite this

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

    @misc{lax-945089,
  author = {Pierre Senellart and Claude (Anthropic)},
  title = {Descriptive complexity: games and inexpressibility},
  year = {2026},
  howpublished = {Lax Archive, lax-945089},
  url = {https://laxarchive.org/lax-945089/},
  note = {draft},
}

    References

    1. Pierre Senellart and Anton Gnatenko. Descriptive Complexity in Lean: Completeness by First-Order Reductions. 2026. arXiv:2609.18261
    2. Pierre Senellart. DescriptiveComplexity: Completeness by First-Order Reductions in Lean. 2026. doi:10.5281/zenodo.21678423 · github.com/PierreSenellart/descriptive-complexity
    3. Andrzej Ehrenfeucht. An application of games to the completeness problem for formalized theories. Fundamenta Mathematicae 49:129–141, 1961. doi:10.4064/fm-49-2-129-141
    4. Neil Immerman. Languages that Capture Complexity Classes. SIAM J. Comput. 16(4):760–778, 1987. doi:10.1137/0216051
    5. Miklós Ajtai. Σ11\Sigma^1_1-formulae on finite structures. Ann. Pure Appl. Log. 24(1):1–48, 1983. doi:10.1016/0168-0072(83)90038-6
    6. Merrick L. Furst, James B. Saxe and Michael Sipser. Parity, circuits, and the polynomial-time hierarchy. Math. Syst. Theory 17(1):13–27, 1984. doi:10.1007/BF01744431
    7. Johan Håstad. Almost Optimal Lower Bounds for Small Depth Circuits. In Proceedings of the 18th Annual ACM Symposium on Theory of Computing, 1986, Berkeley, California, USA 6–20, 1986. doi:10.1145/12130.12132
    8. Neil Immerman. Descriptive Complexity. Springer, 1999. doi:10.1007/978-1-4612-0539-5
    9. Heinz-Dieter Ebbinghaus and Jörg Flum. Finite Model Theory. Springer, 1995.

    Discussion

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

    Loading discussion…