Lax Lean Archive

Descriptive complexity: L, NL and transitive closure

lax-485149·formalized by Pierre Senellart @PierreSenellart · Claude (Anthropic)·registered·created ·GitHub @eee50ee·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

    Logarithmic space as two logically defined classes, from the descriptive-complexity library, built on the NP core registered as lax-904597. NL is the class of decision problems on finite structures definable in the Krom fragment of existential second-order logic, and L the class of those definable in first-order logic with a deterministic transitive closure, both on ordered structures and invariantly in the order; these are the logics that capture nondeterministic and deterministic logarithmic space, by theorems of Grädel and Immerman. No machine model enters the definitions.

    The central result is the Immerman–Szelepcsényi theorem in logical form: first-order logic with a transitive closure, FO(TC), is closed under complement, by a walk that counts inductively the tuples reachable from the sources. Two translations relate the Krom fragment to FO(TC), each exchanging a problem with its complement, so that NL = FO(TC) and NL = coNL. L is closed under complement as well, without inductive counting, and FO(≤) ⊆ FO(DTC) ⊆ FO(TC), whence L ⊆ NL; NL ⊆ NP.

    Five problems are complete under the core's first-order reductions: reachability in directed graphs, its complement and the satisfiability of CNF formulas of width two for NL, by generic reductions that build the graph of a transitive closure or instantiate a Krom program; deterministic reachability, along the edges that are alone in leaving their source, and its complement for L.

    Both classes are then related to a machine model: a problem is in NL exactly when it is accepted by a two-way multihead automaton on ordered structures, with quantifier-free tests and no work tape, and in L exactly when the automaton can be taken deterministic.

    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
    40 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-485149,
  author = {Pierre Senellart and Claude (Anthropic)},
  title = {Descriptive complexity: L, NL and transitive closure},
  year = {2026},
  howpublished = {Lax Archive, lax-485149},
  url = {https://laxarchive.org/lax-485149/},
}

    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. Neil Immerman. Nondeterministic Space is Closed Under Complementation. SIAM J. Comput. 17(5):935–938, 1988. doi:10.1137/0217058
    4. Róbert Szelepcsényi. The Method of Forced Enumeration for Nondeterministic Automata. Acta Informatica 26(3):279–284, 1988. doi:10.1007/BF00299636
    5. Erich Grädel. Capturing Complexity Classes by Fragments of Second-Order Logic. Theor. Comput. Sci. 101(1):35–57, 1992. doi:10.1016/0304-3975(92)90149-A
    6. Neil Immerman. Languages that Capture Complexity Classes. SIAM J. Comput. 16(4):760–778, 1987. doi:10.1137/0216051
    7. Neil D. Jones. Space-Bounded Reducibility among Combinatorial Problems. J. Comput. Syst. Sci. 11(1):68–85, 1975. doi:10.1016/S0022-0000(75)80050-X
    8. 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…