The logically defined classes are the degrees of their complete problems

Each class of this library with a complete problem Q₀ is the degree of Q₀ (DescriptiveComplexity.ComplexityClass.below, the file DescriptiveComplexity.Degree): NP = below SAT, coNP = below TAUT, PTIME = below HORNSAT, NL = below TwoSAT and RE = below FINSAT. This is the sanity check that the degree construction is the right one – and a theorem rather than a tautology, since the two sides are defined completely differently: on the left a logic, on the right a closure under reductions.

The payoff is that “Q₀-hardness is 𝒞-hardness” stops being folklore: since the classes are equal, so are their hardness predicates, whichever way a given hardness proof was obtained.

Each proof supplies DescriptiveComplexity.ComplexityClass.eq_below_of_complete with the class's own hardness discharge, which delivers the non-relativized reduction ≤ᶠᵒ[≤] that the equality needs – cofinal hardness on its own yields only ≤ʳᶠᵒ[≤]. This is why the statement cannot be proved generically, for an arbitrary class and an arbitrary complete problem of it.

theorem DescriptiveComplexity.NP_eq_below_sat : NP = ComplexityClass.below SAT

NP is the degree of SAT: a problem is in NP exactly when it reduces to SAT (Cook–Levin, read as an equality of classes).

theorem DescriptiveComplexity.coNP_eq_below_taut : coNP = ComplexityClass.below TAUT

coNP is the degree of TAUT.

theorem DescriptiveComplexity.PTIME_eq_below_hornSat : PTIME = ComplexityClass.below HORNSAT

PTIME is the degree of HORN-SAT.

theorem DescriptiveComplexity.NL_eq_below_twoSat : NL = ComplexityClass.below TwoSAT

NL is the degree of 2SAT.

theorem DescriptiveComplexity.RE_eq_below_finsat : RE = ComplexityClass.below FINSAT

RE is the degree of FINSAT: Trakhtenbrot's theorem, read as an equality of classes.