Lax Lean Archive

Descriptive complexity: coNP, DP and the polynomial hierarchy

lax-564036·formalized by Pierre Senellart @PierreSenellart · Claude (Anthropic)·registered·created ·GitHub @646a3b4·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 polynomial hierarchy as a family of logically defined classes, from the descriptive-complexity library, built on the NP core registered as lax-904597, the catalog of NP-complete problems lax-799700, and the classes of logarithmic space and polynomial time, lax-485149 and lax-535992. Above polynomial time, the level Σₖ is the class of decision problems on finite structures definable by a second-order sentence with k alternating blocks of quantifiers, existential first, and Πₖ the class of those definable with a universal first block: the levels of the hierarchy by the theorems of Fagin and Stockmeyer. coNP is Π₁, PH is the union of the levels, and DP is the class of conjunctions of an NP and a coNP condition. No machine model enters the definitions.

    Πₖ is the class of complements of Σₖ, the levels are nested and contained in PH, polynomial time is at the bottom, inside NP ∩ coNP, and NP ∪ coNP ⊆ DP ⊆ Σ₂ ∩ Π₂. coNP and DP are closed under first-order reductions.

    Complete problems are given at every level, under the core's first-order reductions: tautology of DNF formulas, its restriction to width three and the unsatisfiability of 3-CNF formulas for coNP; SAT-UNSAT for DP; and, for every k ≥ 1, quantified Boolean formulas with k alternating blocks for Σₖ and for Πₖ, according to the first quantifier.

    Each level is then related to a machine model: acceptance by an alternating Turing machine with k blocks of states, within the bounds of the instance, is complete for Σₖ or Πₖ according to its first block, and a problem is in the level exactly when it reduces to that acceptance problem. At one block these are the nondeterministic machine and its dual.

    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
    38 concepts
    100%
    The complement of a decision problemProblems given by a property of structuresAtoms in second-order relation variablesThe classes PTIME and coPTIMEThe Horn fragment of existentialsecond-order logicThe polynomial hierarchy by alternatingTuring machinesInvariance and characterization of alternatingmachine acceptanceAcceptance by alternating Turing machineswith a bounded number of alternationscoNP is closed under first-order reductionsDP is closed under first-order reductionsNP ∪ coNP ⊆ DP ⊆ Σ₂ ∩ Π₂The class DPThe polynomial hierarchy, coNP and PHΠ_k is co-Σ_kThe levels of the polynomial hierarchy arenestedPTIME at the bottom of the polynomialhierarchyQBF with k alternations is complete for thek-th levelQuantified Boolean formulas with a boundednumber of alternationsInvariance and characterization of quantifiedBoolean formulasSAT-UNSATSAT-UNSAT is DP-completeInvariance and characterization ofSAT-UNSATTAUT is coNP-completeTautology of DNF formulasInvariance and characterization of TAUT3-DNF-TAUT and 3-UNSAT arecoNP-completeTautology of 3-DNF formulas andunsatisfiability of 3-CNF formulasInvariance and characterization of3-DNF-TAUT and 3-UNSATClauses, literals and binary numbersProblems given by a property of structures3SATComplexity classes, cofinal hardness, and NPFirst-order interpretations and first-orderreductionsNondeterministic Turing machines as finitestructuresDecision problems on finite structuresRelativized first-order interpretationsSAT, propositional satisfiabilitySecond-order definability with boundedalternation
    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-564036,
  author = {Pierre Senellart and Claude (Anthropic)},
  title = {Descriptive complexity: coNP, DP and the polynomial hierarchy},
  year = {2026},
  howpublished = {Lax Archive, lax-564036},
  url = {https://laxarchive.org/lax-564036/},
}

    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. Ronald Fagin. Generalized first-order spectra and polynomial-time recognizable sets. In Complexity of Computation 7:43–73, 1974.
    4. Larry J. Stockmeyer. The Polynomial-Time Hierarchy. Theor. Comput. Sci. 3(1):1–22, 1976. doi:10.1016/0304-3975(76)90061-X
    5. Celia Wrathall. Complete Sets and the Polynomial-Time Hierarchy. Theor. Comput. Sci. 3(1):23–33, 1976. doi:10.1016/0304-3975(76)90062-1
    6. Christos H. Papadimitriou and Mihalis Yannakakis. The Complexity of Facets (and Some Facets of Complexity). J. Comput. Syst. Sci. 28(2):244–259, 1984. doi:10.1016/0022-0000(84)90068-0
    7. Ashok K. Chandra, Dexter Kozen and Larry J. Stockmeyer. Alternation. J. ACM 28(1):114–133, 1981. doi:10.1145/322234.322243
    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…