SAT is NP-complete, with NP read as existential second-order definability and hardness as cofinal hardness under relativized ordered first-order reductions. The two halves are stated in their sharper forms as well: SAT is $\Sigma_1$-definable, by the sentence that guesses a truth assignment and checks, in first-order logic, that every clause contains a true literal; and every $\Sigma_1$-definable problem has a plain ordered first-order reduction to SAT. The reduction is generic and machine-free: in the manner of Dahlhaus, it rewrites the first-order kernel of the defining sentence into clauses over the elements of the input structure, with the guessed relations as propositional variables.

Since ordered first-order reductions are computable in $\mathrm{AC}^0$ (a standard fact, not formalized here), the hardness half is stronger than hardness under polynomial-time reductions.