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.
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).
Registered in the Lax archive as
Lax604544.ClassesAsDegrees.NP_eq_below_sat.
Dependency graph
coNP is the degree of TAUT.
Registered in the Lax archive as
Lax604544.ClassesAsDegrees.coNP_eq_below_taut.
Dependency graph
PTIME is the degree of HORN-SAT.
Registered in the Lax archive as
Lax604544.ClassesAsDegrees.PTIME_eq_below_hornSat.
Dependency graph
NL is the degree of 2SAT.
Registered in the Lax archive as
Lax604544.ClassesAsDegrees.NL_eq_below_twoSat.
Dependency graph
RE is the degree of FINSAT: Trakhtenbrot's theorem, read as an equality
of classes.
Registered in the Lax archive as
Lax604544.ClassesAsDegrees.RE_eq_below_finsat.