Lax Lean Archive

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

NP and PTIME on bit strings: the descriptive-complexity library against Fagin and Immerman–Vardi

lax-832283·formalized by Pierre Senellart @PierreSenellart · Claude (Anthropic)·created ·GitHub @f06e25b·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 classes NP and PTIME of the descriptive-complexity library, which are defined by logics on finite structures, are the textbook classes on bit strings. Over a vocabulary with finitely many relation symbols, a decision problem is in NP exactly when the language of the binary encodings of its yes-instances has polynomially bounded certificates checked in polynomial time by a Mathlib Turing machine (FinTM2); it is in PTIME exactly when such a machine decides that language in polynomial time. The encodings and the machine classes are those of Szymon Toruńczyk's lax-988886 (Fagin's theorem) and lax-751879 (the Immerman–Vardi theorem), required here, and each machine statement is one application of a registered capture theorem.

    The content of this submission is the logical side, which assumes neither theorem: the library's second-order definition of NP agrees with the existential second-order logic of lax-988886, and the library's definition of PTIME with the FO(LFP) of lax-751879. The second agreement carries the proofs. Going to the archive's syntax turns one simultaneous least fixed point into nested ones, by Bekić's principle. Coming back turns nested, negated, and parameterized fixed points into one inflationary induction, by a construction that iterates a program in a relation it reads, its rounds being the tuples of the universe, each round starting from empty relations and opening once the previous round has converged.

    Concepts

    Concept map
    40 concepts
    100%
    The classes L and coLThe classes NL and coNLThe complement of a decision problemFirst-order logic with a deterministictransitive closureThe Krom fragment of existentialsecond-order logicProblems given by a property of structuresAtoms in second-order relation variablesFirst-order logic with a transitive closureThe circuit value problemThe classes PTIME and coPTIMEAcceptance by deterministic Turing machinesGAME, alternating reachabilityThe Horn fragment of existentialsecond-order logicSatisfiability of Horn formulasHORN-SAT is PTIME-completeFirst-order logic with inflationary fixedpointsFirst-order logic with least fixed pointsPolynomial-time evaluation of fixed-pointqueriesSemantics and definability in FO(LFP)First-order logic with least fixed pointsThe Immerman–Vardi theoremLeast fixed points on finite relationsFinite ordered relational structures andqueriesPolynomial-time queries on orderedstructuresBinary encodings of ordered structures andtuplesNP and PTIME against the logics of the twoentriesNP and PTIME are the textbook classes onbit stringsDecision problems of the core on bit stringsComplexity classes, cofinal hardness, and NPThe Cook–Levin theorem, by first-orderreductionsFirst-order interpretations and first-orderreductionsNondeterministic Turing machines as finitestructuresDecision problems on finite structuresRelativized first-order interpretationsSAT, propositional satisfiabilitySecond-order definability with boundedalternationExistential second-order logicFagin’s theoremFinite relational structures and theirpropertiesNP through polynomially boundedcertificates
    Proven claimDefinitionThis submissionOther submissionA → B: B builds on A

    Proofs

    Proof networkview on GitHub

    100%
    premise files concept fileProven claimClaim from this submission / another submissionAll proofs of one concept — hover for individual statements and proofs
    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-832283,
  author = {Pierre Senellart and Claude (Anthropic)},
  title = {NP and PTIME on bit strings: the descriptive-complexity library against Fagin and Immerman–Vardi},
  year = {2026},
  howpublished = {Lax Archive, lax-832283},
  url = {https://laxarchive.org/lax-832283/},
  note = {draft},
}

    References

    1. Pierre Senellart and Anton Gnatenko. Descriptive Complexity in Lean: Completeness by First-Order Reductions. 2026. arXiv:2609.18261
    2. Ronald Fagin. Generalized first-order spectra and polynomial-time recognizable sets. In Complexity of Computation 7:43–73, 1974.
    3. Moshe Y. Vardi. The Complexity of Relational Query Languages (Extended Abstract). In Proceedings of the 14th Annual ACM Symposium on Theory of Computing, May 5-7, 1982, San Francisco, California, USA 137–146, 1982. doi:10.1145/800070.802186
    4. Neil Immerman. Relational Queries Computable in Polynomial Time. Inf. Control. 68(1-3):86–104, 1986. doi:10.1016/S0019-9958(86)80029-8
    5. Hans Bekić. Definable Operations in General Algebras, and the Theory of Automata and Flowcharts. In Programming Languages and Their Definition – Hans Bekić (1936-1982) 177:30–55, 1984. doi:10.1007/BFb0048939

    Discussion

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

    Loading discussion…