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.
Update
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.