PaperlayerView exact revision on arXiv

Source-linked AI summary

Descriptive Complexity in Lean: Completeness by First-Order Reductions

Pierre Senellart, Anton Gnatenko

arXiv:2609.18261v1cs.LOcs.CC

TL;DR

Proof assistants provide limited support for computational complexity, while conventional machine-based proofs resist mechanization because reductions require resource-bound arguments. The library defines isomorphism-invariant problems on finite structures, logical complexity classes, definability witnesses, first-order reductions, and bridges to nondeterministic and deterministic machines. The library proves 73 completeness theorems across 14 classes, plus logical results including NL = coNL.

  • Problem

    Proof assistants provide limited support for computational complexity, while conventional machine-based proofs resist mechanization because reductions require resource-bound arguments.

  • Method

    The library defines isomorphism-invariant problems on finite structures, logical complexity classes, definability witnesses, first-order reductions, and bridges to nondeterministic and deterministic machines.

  • Results

    The library proves 73 completeness theorems across 14 classes, plus logical results including NL = coNL.

  • Takeaways & Limitations

    Descriptive complexity provides a productive formalization route in which membership and completeness become logical statements and machine models become theorems.

  • Takeaways & Limitations

    The descriptive approach cannot prove hierarchy theorems that require diagonalizing against clock-bounded machine models.

Abstract

from arXiv · show

We show that descriptive complexity can serve as a foundation for formalizing computational complexity results in a proof assistant, by constructing a Lean library centered around the following concepts: decision problems are isomorphism-invariant predicates on finite structures; complexity classes are defined by their logical characterization; membership is shown by definability witnesses; hardness is shown by first-order reductions from a known hard problem. We also establish bridges to traditional machine models such as (non)deterministic Turing machines. The library proves 73 completeness results, on 68 problems or problem families, over 14 different classes; relations between the classes established inside the logic and not by machine simulation, among them NL = coNL and the Abiteboul-Vianu theorem; and unconditional lower bounds, among them $\mathrm{FO}(\leq) \subsetneq \mathrm{FO}(\leq, \mathrm{TC})$ and the failure of order-free FO(IFP) to capture PTIME.

1 Introduction

The paper argues that descriptive complexity offers a more tractable foundation for formalizing computational complexity than machine-centered proofs. It develops a Lean library using logical definitions, first-order reductions, and bridges to machine models, yielding broad completeness and structural results.

  • Motivation and approach: Existing proof-assistant support formalizes few complexity results because machine-based reductions require separate bounded-resource proofs.The cited developments collectively contain only seven completeness theorems, with further proofs again depending on computational models.
  • Motivation and approach: Descriptive complexity sidesteps machine models and resource constraints by defining classes logically, proving membership through formulas, and proving hardness through first-order reductions.First-order reductions are stronger than Karp reductions and require only first-order logic already available in Mathlib.
  • Contributions: The library formalizes decision problems, logical complexity classes, first-order reductions, and encodings for translating user-defined instances into finite structures.Its framework is designed around isomorphism-invariant predicates, definability witnesses, and reductions by interpretation.
  • Contributions: It proves class relations inside logic, including NL = coNL, PSPACE = coPSPACE, fixed-point characterizations, the Abiteboul–Vianu theorem, and unconditional lower bounds.These results include FO(≤) ⊊ FO(≤, TC) and the failure of order-free FO(IFP) to capture PTIME.
  • Contributions: The library establishes machine bridges, including the equivalence between existential second-order NP and reductions to nondeterministic-machine acceptance.Machine configurations and computations are encoded in finite structures, with universe size bounding running time; Cook–Levin is proved in two forms.
  • Contributions: 73 completeness theorems across 14 classes are proved for concrete problems by first-order reductions.The library comprises 212k lines of Lean across 726 modules and is released with its source code.

2 Background

The background develops finite-structure semantics, logical characterizations of complexity classes, and the first-order interpretations used as reductions. It also situates these definitions within Mathlib and explains their classical computational meaning.

  • Descriptive complexity: Descriptive complexity characterizes classes through logics such as existential second-order logic, fixed-point logics, transitive closure, and ordered fragments.Fagin’s theorem identifies NP with properties definable in existential second-order logic.
  • Finite structures and logics: First-order logic evaluates formulas over structures, while complexity statements restrict attention to finite universes rather than changing satisfaction semantics.The framework includes transitive and deterministic transitive closure, least and inflationary fixed points, partial fixed points, and second-order fragments.
  • Finite structures and logics: Second-order fragments are organized by quantifier alternation and syntactic restrictions such as Horn and Krom clauses, with ordered variants allowing the relation ≤.Value-inventing existential second-order logic extends the universe with finitely many fresh elements under explicit resource bounds.
  • Complexity classes: The library defines classes by logical capture and records equivalent characterizations and representative complete problems in its class table.The table notes that PH has no complete problem unless the hierarchy collapses, while GI is a degree not captured by a logic.
  • First-order reductions: A first-order interpretation constructs an output structure from tagged tuples of fixed dimension, with formulas defining its relations; explicit tags avoid requiring ordered inputs.The interpreted universe consists of tagged copies of admitted tuples, and relation formulas are evaluated on their coordinates.
  • First-order reductions: First-order reductions are computable in polynomial time and therefore imply Karp reductions, while FO(≤) is strictly weaker than FO(≤, BIT) and lies inside AC0.The library proves the polynomial-time implication using the FO(≤, LFP) characterization of PTIME.
  • Lean infrastructure: Mathlib’s Set.Definable concerns subsets of one fixed structure, whereas this library retains formulas defining isomorphism-invariant decision problems across finite structures.That distinction is required by capture theorems and the logical fragments developed in the library.

3 The Reduction Framework

The reduction framework represents decision problems as isomorphism-invariant predicates and reductions as first-order interpretations over finite structures. It supports composition, definability transfer, and faithful encodings between concrete inputs and structures.

  • Decision problems: Decision problems are isomorphism-invariant predicates on structures, with finiteness imposed only by later membership and hardness notions.Behavior on infinite structures is invisible to the theory because the relevant class fields compare problems only on finite structures.
  • Interpretations: An interpretation maps an input structure to a tagged product of fixed-dimensional tuples whose relations are defined by first-order formulas.The Lean implementation stores relation formulas directly and can leave unintended tagged tuples isolated instead of using definable subtypes.
  • Interpretations: Interpretation semantics are illustrated by creating left and right copies of every graph vertex and defining cross-copy edges through the original edge relation.With two tags and dimension one, each output element is a tagged input vertex.
  • Reduction properties: First-order reductions preserve correctness on finite nonempty inputs, and formula pullback preserves satisfaction from the interpreted structure to the source structure.Correctness is restricted to nonempty inputs because fixed-dimensional interpretations cannot produce nonempty outputs from empty sources.
  • Reduction properties: Reductions compose by pulling formulas back through interpretations, with structural isomorphisms resolving Lean’s flattened-tuple versus tuple-of-tuples carrier mismatch.The resulting relation is transitive and, together with the identity interpretation, forms a preorder; definability transfers backward along reductions.
  • Reduction properties: Ordered and relativized ordered reductions extend the framework with input orders and domain formulas while retaining composition and backward definability transfer.These variants support reductions whose interpretations explicitly restrict the output universe.
  • Encodings: Encodings connect concrete data to finite structures using polynomial size bounds in both directions and a separate faithfulness condition.Both bounds prevent padding or compression from distorting complexity, while decoding and well-formed restrictions are needed for hardness transfer.

4 Complexity Classes, Logically Defined

The library defines complexity classes through logical characterizations and first-order-reduction closure, then proves class relations and separations within the logic.

  • 4.1 Defining a complexity class: Complexity classes are constructed from membership predicates that are stable under first-order reductions and determined by finite structures.A pullback lemma supplies reduction stability for each defining logic.
  • 4.2 A catalog of classes: First-order reductions preserve definability by translating target relation variables into tagged blocks over the source structure, retaining Horn and Krom fragments.This construction supports closure proofs for PTIME and NL without leaving their defining fragments.
  • 4.1 Defining a complexity class: The library defines classes from standard logical characterizations spanning LOGSPACE, NL, PTIME, NP, the polynomial hierarchy, PSPACE, exponential classes, and RE.Some higher classes are obtained through exponential expansion or second-order fixed-point logics.
  • 4.3 Relations between classes: The library derives inclusions such as LOGSPACE ⊆ NL and NL ⊆ PTIME, with the latter obtained through the NL-complete problem 2-sat and its Horn definability.The polynomial hierarchy is handled uniformly, and QBF supplies completeness at every level.
  • 4.4 Unconditional lower bounds: Logical reasoning establishes NL = coNL, fixed-point capture theorems, the Abiteboul–Vianu equivalence, and unconditional separations involving transitive closure and order-free fixed points.Specifically, FO(≤) ⊊ FO(≤, TC), while order-free FO(IFP) does not capture PTIME.

5 Machine Bridges

Machine bridges connect logically defined classes to canonical acceptance problems while encoding computations as finite structures and proving completeness through definability and reductions.

  • 5.1 Machine encodings: NP equals the degree of nondeterministic machine acceptance, with instances asking whether a described machine accepts within a universe-sized step bound.The equivalence is proved as mem_NP_iff_le_ntmAccept.
  • 5.1 Machine encodings: Finite structures encode tape positions, time steps, transitions, states, symbols, ordering, and input, so acceptance becomes a structural property.Deterministic and space-bounded variants modify the acceptance condition and resource bound.
  • 5.2 Recovering the machine classes: NTMAccept is NP-complete because SAT reduces to it and accepting runs are expressed by an existential second-order sentence; DTMAccept similarly enters PTIME through Horn derivability.Determinism makes the DTMAccept run unique, enabling a Horn description.
  • 5.3 Other machine bridges: Below PTIME, LOGSPACE and NL are captured by two-way multi-head automata, while AC0 is characterized by constant-alternation logarithmic time; RE is characterized through unbounded existential value invention and halting reductions.The RE result is stated in Mathlib’s REPred framework.
  • 5.2 Recovering the machine classes: The bridges extend upward: space-bounded nondeterministic and deterministic acceptance are complete for PSPACE, alternating space acceptance reaches EXPTIME, and wide machines yield NEXPTIME and EXPSPACE completeness.The wide-machine universe supports exponentially many tape and clock positions.
  • 5.4 Cook–Levin: Cook–Levin is proved both ways: NTMAccept reduces to SAT via an existential second-order encoding and Tseitin clauses, while SAT reduces to NTMAccept through machine simulation.The result is packaged as interreducibility and as SAT completeness for the machine-defined NP class.

6 A Catalog of Complete Problems

The catalog contains dozens of completeness results linked by first-order reductions, extends completeness to classes and problems beyond the standard NP list, and assigns graph isomorphism its own degree.

  • 6.4 Cost of the catalog: Adding a catalog problem costs a median of 869 lines of problem-specific modules, with quartiles of 521 and 1 192.These are incremental source-line costs beyond the base library, excluding machine-model modules.
  • 6.1 NP- and coNP-complete problems: Figure 5 records NP-complete problems as nodes and proved first-order reductions as arrows, with Karp’s 21 problems highlighted.The catalog also includes machine problems, common hardness starting points, and query-evaluation or graph-crawling problems.
  • 6.1 NP- and coNP-complete problems: NP hardness enters once through the reduction from existential second-order definability to SAT, after which other problems inherit hardness by composing first-order reductions from SAT.Membership is established separately by a definability witness, explaining why the reduction graph is not strongly connected.
  • 6.1 NP- and coNP-complete problems: Reduction variants are selected by gadget requirements: ordered reductions encode numerical weights, while relativized ordered reductions restrict spanning gadgets to meaningful output vertices.Most reductions are order-free, using tags to simulate the role of order in fixed-copy gadgets.
  • 6.2 Other classes: Completeness for other classes follows recurring patterns involving defining problems, complements, and classical complete problems such as CVP and reach.CVP and reach are complete under order-invariant first-order reductions, strengthening their classical logarithmic-space statements.
  • 6.3 The GI degree: Graph isomorphism fits none of the logically defined classes because it is in NP, is not known NP-complete or in PTIME, and lacks a logical characterization for completeness.The degree construction nevertheless makes graph-iso, digraph-iso, and dag-iso complete for the same downward-closure degree.
  • 6.3 The GI degree: Isomorphism reductions are substantially more laborious because correctness must exclude every accidental automorphism; the digraph-to-graph gadget requires about 750 lines.Translation gadgets are cheaper when correctness follows directly from the construction.

7 Related Work

The related-work comparison positions the library against prior mechanized complexity developments and reports descriptive complexity as a scalable alternative, while cautioning that line counts are imperfect comparisons.

  • 7.1 Prior mechanizations: Existing Lean libraries provide computability tools and Turing machines but no complexity classes, resource-bounded reductions, or completeness results.The authors identify only four prior developments that define complexity classes.
  • 7.1 Prior mechanizations: Prior developments prove few completeness theorems, and one reduction catalog leaves the root NP-hardness step admitted.The comparison excludes projects whose headline results were admitted, vacuous, or based on opaque axioms.
  • 7.2 Comparison by formalization cost: Cook–Levin closure sizes range from 6 262 to 43 946 lines across developments, while the two Lean rows compare at 6 262 versus 29 693 lines.The authors warn that scopes, inputs, provers, and imported libraries differ, making line counts a weak measure.
  • 7.3 Relation to adjacent work: The library extends prior mechanized work on reductions, finite relations, fixpoint semantics, and logic–automata connections, while adding formalized capture theorems and Ehrenfeucht–Fraïssé games.The authors report no prior mechanization of the fixed-point and transitive-closure logics or these capture results.

8 Design Decisions and Limitations

The library uses first-order reductions over finite structures to establish completeness results while exposing explicit trade-offs against traditional string-based complexity models. This approach preserves classical hardness transfer and broad coverage, but omits cost-sensitive and hierarchy results because it has no resource-cost model.

  • 8.1 First-order vs. Karp reductions: Every first-order reduction is also a polynomial-time Karp reduction, so first-order hardness transfers directly to the classical notion.First-order reductions are strictly weaker than Karp reductions, making hardness proved through them the stronger statement.
  • 8.1 First-order vs. Karp reductions: The library proves that the converse fails already for logarithmic-space reductions: a deterministic ordered reduction exists where no first-order reduction does.The separating reduction walks once along the order, showing why the weaker first-order notion yields a stronger completeness statement.
  • 8.1 First-order vs. Karp reductions: 73 completeness results across 14 classes use first-order reductions, with no catalog problem dropped because of the restriction.The library reaches partition through an ordered first-order reduction from nae-sat when the usual subset-sum route does not fit the logic.
  • 8.2 Finite structures vs. strings: Finite structures replace ordered strings: machines become data inside structures, and polynomial budgets come from reduction dimension rather than explicit arithmetic.Order-invariance becomes an explicit variant, enabling results about Abiteboul–Vianu and order-free FO(IFP), while string-style cost functions and hierarchy theorems are lost.
  • 8.2 Finite structures vs. strings: Encoding concrete data requires polynomial size bounds and faithfulness, but the encoding computation itself is uncosted, so transported completeness inherits an unmeasured cost.The same issue arises when machines first write graphs or formulas as strings before running.
  • 8.3 What the descriptive approach cannot do: Without a cost model, the library cannot express fine-grained complexity or prove hierarchy theorems such as separating DTIME(f) from DTIME(2f).There is no clock or diagonalization target corresponding to the machine model carried by traditional complexity libraries.

9 Conclusion

The paper presents descriptive complexity as a foundation for Lean formalization by making membership, completeness, and class relations logical statements rather than machine simulations. The resulting library reaches broad completeness coverage, while identifying locality, counting, and quantifier-free composition as promising extensions.

  • 9 Conclusion: The library formalizes decision problems as isomorphism-invariant finite-structure properties, classes as definability predicates, and hardness as first-order reduction.Membership becomes a sentence, hardness a reduction, and completeness the combination of both, with machine models treated as theorems.
  • 9 Conclusion: 73 completeness theorems across 14 classes were reached, with a median of 869 lines in each problem’s own modules.The paper reports 68 problems or problem families in its abstract context.
  • 9 Conclusion: Future extensions would add locality-based inexpressibility results, counting logic for #P, and quantifier-free composition toward first-order projections.The proposed extensions preserve the library’s logical idiom while broadening the catalog.
  • 9 Conclusion: The library is publicly available under the Apache 2.0 license, and the reported measurements use release 1.2.2.The repository is hosted at github.com/PierreSenellart/descriptive-complexity.

A How Often the Literature Proves a Hardness Result

The paper measures how often 2025 theoretical-computer-science arXiv papers claim new hardness or completeness results, then describes the logical representations used in its Lean library.

  • Measurement: The seven selected theoretical-computer-science categories range from 6.0% to 24.8%, whereas all cs.* would yield only 0.5% because machine-learning papers dominate the archive.The category choice therefore materially affects the measured proportion.
  • Caveats: The survey’s claim that hardness results are usually established by reductions is supported only by a full-text sample, in which 35 of 40 counted papers used explicit reduction language.The paper also cautions that arXiv is not the whole literature and that authors choose their primary categories.
  • Lean representation: The Lean library represents complexity classes as definability predicates, using first-order syntax, ordered expansions, second-order quantifier blocks, and fixed-point or closure specifications.Its second-order framework folds relation-variable blocks into vocabularies and realizes alternating quantification over first-order formulas.
  • Lean representation: Horn and Krom fragments, least and partial fixed points, inflationary fixed points, transitive closure, and pebble games are encoded as structured data or semantic predicates.These representations separate the logical objects from their Lean declarations while retaining the intended semantic witnesses.

C What the Machine Characterization Costs at Each Level

The library measures machine-characterization costs as declaration closures and finds that most classes require substantially less infrastructure than the exceptional wide-machine rows.

  • Cost accounting: The marginal column measures new declarations relative to the already-paid baseline, rather than subtracting aggregate line totals.For most rows the baseline is the class’s complete problem; at exponential classes the machine comes first.
  • Overall cost: Every machine characterization from PTIME through EXPTIME, and RE above them, closes below 19,658 lines, with the smallest Cook–Levin closure among the compared libraries.The cost measure counts transitively reached declarations in the library’s own modules.
  • Additional machines: Adding a second machine characterization is comparatively cheap: 124 lines for nondeterministic space, 55 for deterministic wide machines, and 442 for one-block alternation.These results transfer from an existing machine characterization rather than rebuilding the logical foundation.
  • Wide machines: The two wide-machine rows cost 40,832 and 47,007 lines, versus 12,641 for EXPTIME, because their reductions quantify over exponential instance expansions.Their hardness half alone requires 46,161 lines and must write the machine program inside the logic.

D Complete Problems per Class

The catalog contains 73 completeness theorems covering 68 distinct problems or problem families across 14 classes, with counting rules that distinguish forms, classes, and restatements.

  • Catalog scope: 73 completeness theorems cover 68 distinct problems or problem families across 14 classes.The count is by theorem, so one problem can contribute separate theorems for multiple classes or variants.
  • Counting rules: Problem families contribute once per complete form, while a problem complete for two equal classes contributes a theorem to each class.Restatements that merely instantiate an already-counted theorem are not counted twice.

E What a Complete Problem Costs

The paper distinguishes framework costs from per-problem costs and illustrates the workflow with subgraph isomorphism, whose completeness proof combines a logical witness with a first-order reduction.

  • Cost accounting: The catalog costs each problem by the nonblank source lines in its own modules, while machine-model costs are excluded and counted separately.The framework closures in Tables 3 and 4 are paid once beneath theorems, whereas problem costs measure incremental modules.
  • Cost accounting: Table 4 counts declaration closures for machine-characterization proofs, with overlapping membership, hardness, and completeness closures that therefore do not sum.The table also distinguishes captures from complete problems and marks second-machine results as additions to existing rows.
  • Catalog scope: 61 of the 73 completeness theorems are costed as problem modules, while the remaining 12 belong to machine models.Some problem modules carry several theorems, so theorem and problem counts are not identical.
  • Subgraph isomorphism: The subgraph-isomorphism example follows seven steps: vocabulary, semantics, invariance, membership, hardness, completeness, and encoding or decoding.Its 474 lines include the problem definition, reduction and correctness proof, definability witness, and concrete-data interface.
  • Subgraph isomorphism: Subgraph isomorphism uses a two-graph vocabulary with unary pattern and host marks plus separate adjacency relations, allowing deliberate junk elements outside both graphs.The predicate requires an injective homomorphism, not an induced subgraph, so pattern non-edges are unconstrained.
  • Subgraph isomorphism: Membership is established by an existential second-order definability witness, while hardness reduces marked-graph clique to subgraph isomorphism through a tagged dimension-one interpretation.The resulting pair yields the stated NP-completeness theorem without introducing a machine model.

G How the Closures of Table 3 Are Computed

The closure counts declarations reached through theorem statements and proof terms, mapping their source ranges to merged module spans and counting substantive lines. Rocq and Isabelle use analogous prover-specific dependency traversals.

  • Lean closure: Lean closure follows declarations mentioned by a theorem’s proof term, recursively traversing statements and proof terms alike.Each declaration is mapped to its source range before coverage is measured.
  • Measurement: Overlapping source ranges are merged per module, and lines count only when they contain more than whitespace, comments, or docstrings.This line-counting convention is reused for every measurement in the paper.
  • Cross-prover comparison: Rocq and Isabelle use their own dependency machinery: coq-dpdgraph’s kernel-level graph and Isabelle’s Proofterm.fold_body_thms traversal.These prover-specific procedures produce the corresponding rows under the same measurement convention.
Loading 2609.18261v1…