An academic descendant of Cook just lectured on NP completeness. He said that the idea came from a well-known theorem in first-order logic that talks about completeness of satisfiability for computably enumerable languages. He didn't seem to know exactly which.

Do we know what the theorem is? I bet is not mentioned in the original paper.


Here is Stephen Cook himself explaining.

  • Completeness for recursively enumerable sets.
  • Unsatisfiable predicate calculus formulas are complete for recursively enumerable problems.
  • Why can't we do this for propositional formulas?
  • Analog of recursively enumerable becomes NP.
  • The reductions he used were Turing reductions not Karp's.
  • 1
    $\begingroup$ The closes result I know is that the satisfiability problem of first-order logic over finite structures is $\Sigma_1^0$-complete, i.e., complete for the class of computably enumerable languages. $\endgroup$ Oct 4, 2021 at 20:23
  • 8
    $\begingroup$ Not judging the validity of the original claim, but a "well-known theorem" which even the speaker "didn't seem to know exactly" seems to be stretching the definition of "well-known" a little. $\endgroup$
    – Clement C.
    Oct 4, 2021 at 20:55
  • $\begingroup$ @ReijoJaakkola that helps. It sounds likely that was the result I will confirm. What is a standard reference for that kind of result? $\endgroup$ Oct 4, 2021 at 22:19
  • $\begingroup$ I googled history of NP completeness and found this publication by David Johnson. $\endgroup$ Oct 5, 2021 at 6:21
  • $\begingroup$ youtube.com/watch?v=M_S_pbaMy0o 1:09 $\endgroup$ Oct 12, 2021 at 7:31

1 Answer 1


There are two results this could plausibly be which nicely contrast each other - they differ on whether we look at finite or infinite structures:

  • (Turing, following Godel) The validity problem for first-order logic on arbitrary structures in a sufficiently rich language is $\Sigma^0_1$-complete; for example, the set of (codes of) sentences true in every directed graph is $\Sigma^0_1$-complete.

  • (Trakhtenbrot) The satisfiability problem for first-order logic on finite structures in a sufficiently rich language is $\Sigma^0_1$-complete; for example, the set of (codes of) sentences true in some finite directed graph is $\Sigma^0_1$-complete.

  • $\begingroup$ Since this is often overlooked, let me observe that by far the most surprising part of either of these results is the upper bound on the validity problem for arbitrary structures, which at first glance is merely $\Pi_1$ in the Levy hierarchy; see the discussion here. $\endgroup$ Oct 10, 2021 at 23:44

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.