Corollaries of Cook–Levin

Structural consequences of the NP-completeness of SAT (SAT.NPComplete_language):

• SAT.coNPComplete_compl_language — the complement of the SAT language is coNP-complete, by dualizing through NPComplete.compl.
• SAT.language_mem_P_iff_P_eq_NP — SAT is decidable in deterministic polynomial time iff P = NP.

Note that languageᶜ is the complement as a set of bit-strings: it contains the encodings of unsatisfiable CNF formulas together with all strings that are not well-formed formula encodings. This is the standard convention — completeness of the complement holds regardless, because the ill-formed strings are polynomial-time recognizable.

theorem Complexity.SAT.coNPComplete_compl_language : coNPComplete languageᶜ

The complement of SAT is coNP-complete. Immediate dual of the Cook–Levin theorem NPComplete_language.

theorem Complexity.SAT.language_mem_P_iff_P_eq_NP : language ∈ P ↔ P = NP

SAT is in P iff P = NP. Deciding satisfiability in deterministic polynomial time is equivalent to the collapse of NP to P.

theorem Complexity.SAT.language_mem_coNP_iff_NP_eq_coNP : language ∈ coNP ↔ NP = coNP

SAT is in coNP iff NP = coNP. A coNP certificate for satisfiability would collapse NP and coNP.