Lax Lean Archive

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

Descriptive complexity: PSPACE, partial fixed points and the Abiteboul–Vianu theorem

lax-134656·formalized by Pierre Senellart @PierreSenellart · Claude (Anthropic)·created ·GitHub @9337cd3·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

    Polynomial space as a logically defined class, from the descriptive-complexity library, built on the NP core registered as lax-904597, the classes of logarithmic space and polynomial time, lax-485149 and lax-535992, and the polynomial hierarchy. PSPACE is the class of decision problems on finite structures definable in second-order logic with a transitive closure, SO(TC): a walk on the assignments of a block of relation variables, each step a first-order condition on two consecutive assignments. No machine model enters the definition.

    Unlike the logics of the classes below, SO(TC) does not need an order: a walk can guess one into its own state, so the order-free logic defines the same class. PSPACE is closed under complement, which is not syntactic and goes through the deterministic walk that evaluates a quantified Boolean formula; and it contains the polynomial hierarchy, level by level.

    First-order logic with partial fixed points defines the same problems on ordered structures, FO(≤, PFP) = SO(TC) = PSPACE, and contains the inflationary logic. With the capture of polynomial time by inflationary fixed points this gives the Abiteboul–Vianu theorem on ordered structures, and the theorem itself is proved as well: on finite structures without an order, the inflationary and the partial fixed-point logics define the same problems exactly when PTIME = PSPACE.

    Four problems are complete under the core's first-order reductions: quantified Boolean formulas, reachability in a succinctly described transition system, and acceptance by a Turing machine in bounded space, deterministic or not; every problem of the class reduces to the deterministic machine problem, so that PSPACE = NPSPACE in this setting.

    The proofs are those of version 1.2.2 of the library, sliced to what these statements use; they assume the core's hardness laws and the submission's own statements 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
    36 concepts
    100%
    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-134656,
  author = {Pierre Senellart and Claude (Anthropic)},
  title = {Descriptive complexity: PSPACE, partial fixed points and the Abiteboul–Vianu theorem},
  year = {2026},
  howpublished = {Lax Archive, lax-134656},
  url = {https://laxarchive.org/lax-134656/},
  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. Serge Abiteboul and Victor Vianu. Fixpoint Extensions of First-Order Logic and Datalog-Like Languages. In Proceedings of the Fourth Annual Symposium on Logic in Computer Science (LICS '89), Pacific Grove, California, USA, June 5-8, 1989 71–79, 1989. doi:10.1109/LICS.1989.39160
    4. Serge Abiteboul and Victor Vianu. Generic Computation and Its Complexity. Proceedings of the 23rd Annual ACM Symposium on Theory of Computing (STOC '91), New Orleans, Louisiana, USA, May 5-8, 1991 209–219, 1991. doi:10.1145/103418.103444
    5. Anuj Dawar, Steven Lindell and Scott Weinstein. Infinitary Logic and Inductive Definability over Finite Structures. Inf. Comput. 119(2):160–175, 1995. doi:10.1006/INCO.1995.1084
    6. Heinz-Dieter Ebbinghaus and Jörg Flum. Finite Model Theory. Springer, 1995.
    7. Walter J. Savitch. Relationships Between Nondeterministic and Deterministic Tape Complexities. J. Comput. Syst. Sci. 4(2):177–192, 1970. doi:10.1016/S0022-0000(70)80006-X
    8. Larry J. Stockmeyer and Albert R. Meyer. Word Problems Requiring Exponential Time: Preliminary Report. In Proceedings of the 5th Annual ACM Symposium on Theory of Computing (STOC) 1–9, 1973. doi:10.1145/800125.804029
    9. 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
    10. Neil Immerman. Descriptive Complexity. Springer, 1999. doi:10.1007/978-1-4612-0539-5

    Discussion

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

    Loading discussion…