The sealed itinerary

A courier claims to have found a route through forty towns that visits each town once and follows only permitted roads. Finding the route may have required days. Checking the submitted list is mundane: count forty names, reject duplicates, and inspect thirty-nine road entries. The certificate has changed the task. The checker does not need to repeat the search that produced it.

This asymmetry is the intuitive entrance to Cook’s 1971 paper. Earlier computability results separated problems that machines can solve from problems no algorithm solves in general. Church and Turing had shown that some decision demands cross that absolute border. Cook asks for a finer distinction inside the computable world. When every finite instance is decidable, how should one compare the resources required by different decision procedures?

Running time supplies the meter. An input has a length n. A deterministic machine follows one prescribed transition at each step. A nondeterministic machine may branch among allowed transitions, and it accepts if at least one branch reaches an accepting state. Cook studies sets accepted by such machines within a polynomial Q(n). Nondeterminism is a mathematical acceptance rule. It is not a claim that a physical computer guesses correctly or explores an exponential tree without cost.

The certificate reading is equivalent in the modern account: an accepting branch can be written down and checked step by step in polynomial time. Cook’s paper speaks directly in terms of nondeterministic machines, not certificate verifiers. Translating between the two is illuminating only if the time bound is preserved. The certificate includes every choice needed to reconstruct the accepting branch, and the deterministic verifier checks each local transition.

The gap is not simply “fast versus slow”. A polynomial such as n¹⁰⁰ can be useless in practice, while an exponential routine can succeed on small or structured instances. Polynomial time matters because it is stable under ordinary changes of machine and under composition: a polynomial number of polynomial-cost steps remains polynomial. Cobham had advanced polynomial growth as a candidate boundary for feasible functions. Cook makes that boundary organise degrees of decision difficulty.

Time becomes a mathematical boundary

A decision problem is represented as a set of strings over a fixed finite alphabet. Membership means yes; non-membership means no. The encoding matters because running time is measured against string length. Cook permits a sufficiently large fixed alphabet and binary suffixes for infinitely many proposition symbols. A formula of length n can therefore mention only a controlled number of distinct indexed symbols.

Let P denote, in modern notation, the sets decided by deterministic machines in polynomial time. Cook describes the corresponding polynomial degree as the degree of the trivial set. Let NP denote sets accepted by nondeterministic machines in polynomial time. The letters later became standard, but the structural question is already present: does branching acceptance recognise more sets efficiently than deterministic computation decides?

A deterministic simulation can enumerate all nondeterministic branches. If there are two choices at each of T steps, that gives as many as 2^T paths. Since T itself may be a polynomial in n, direct enumeration need not remain polynomial. This observation explains the apparent gap. It does not prove the gap cannot be closed by a different algorithm that never enumerates the tree.

The bound applies to every branch, not only the successful one. This keeps the certificate length under control: record the transition choice made at each of at most Q(n) steps. A verifier simulates those choices and rejects an illegal transition. If a yes-instance has one accepting branch, it has a polynomial-length witness. If the machine rejects, no proposed choice string can create a legal accepting history. This is the bridge from branching machines to certificates, although Cook’s proof proceeds with machine configurations directly.

Encoding discipline protects the resource claim. A number written in unary has length proportional to its value; the same number in binary has logarithmic length. An algorithm polynomial in the value may be exponential in the binary input length. Cook fixes strings and measures their lengths so that a reduction cannot win by silently inflating the representation. Later complexity theory makes encoding choices explicit for exactly this reason.

Cook’s reduction is a machine with questions

Cook formalises reducibility through a query machine. It is a deterministic multitape Turing machine with a distinguished query tape and query, yes and no states. Relative to a set T, the machine writes a string u on the query tape, enters the query state, and receives in one step the correct answer to whether u belongs to T. The oracle is an ideal interface, not an algorithm for T.

A set S is P-reducible to T when some query machine decides membership in S in time polynomial in the input length while using T as its oracle. If a fast procedure for T were inserted at the oracle boundary, the composed process would solve S efficiently. Reduction transfers an algorithmic breakthrough backwards: an easy T would make S easy.

This relation is transitive. Suppose S reduces to T and T reduces to U. Replace each T query in the first machine by the polynomial U-query computation of the second. Polynomial bounds compose. Mutual reducibility is therefore an equivalence relation, and Cook calls each equivalence class a polynomial degree of difficulty.

Modern introductions often define NP-hardness using a polynomial-time many-one reduction: compute one string f(w) such that w∈S exactly when f(w)∈T. Cook’s native definition permits multiple adaptive oracle queries. His proof of Theorem 1 actually constructs one formula A(w), so that central step has the stronger many-one shape. Historical accuracy still requires keeping the definition and the construction distinct.

Direction is another frequent source of error. To show T carries S’s difficulty, reduce S to T. The hypothetical T solver sits at the end of the arrow. Reducing tautology to a new problem X means a polynomial procedure for X would decide tautology. Reducing X to tautology only shows X can borrow a tautology oracle. Completeness requires every member of the source class to point towards the complete target.

A time bound must include the work of forming queries, moving across tapes and processing replies. The oracle’s internal labour is free by definition, but the query string cannot be longer than the reducing machine has time to write. Consequently, every query has polynomial length and there can be only polynomially many query steps. The abstraction isolates T’s decision power without allowing an exponentially long instance to be smuggled through a unit-cost call.

Transitivity also needs this accounting. When a T oracle call is replaced by a reduction from T to U, the inner polynomial is evaluated on a polynomial-sized query. Composing fixed polynomials yields another polynomial. An informal chain of “can be translated” claims is insufficient if an intermediate representation grows exponentially. Cook’s query-machine definition makes the closure argument a property of machines and clocks.

Compile an accepting history into clauses

Let M accept S nondeterministically within T=Q(n) steps. Fix an input w of length n. Cook assumes a one-tape machine whose tape is infinite to the right. No accepting computation of T steps can scan beyond square T. A candidate history therefore fits inside a finite T-by-T space-time region: time along one axis, tape position along the other.

The formula needs atoms describing that region. Pⁱ_s,t says tape square s contains symbol σ_i at time t. Qⁱ_t says the machine is in state q_i at time t. S_s,t says the head scans square s at time t. A truth assignment to these atoms proposes a whole computation history at once.

Constraint B says exactly one square is scanned at each time. It combines an at-least-one disjunction with pairwise exclusions. C says each square at each time contains exactly one symbol. D says exactly one state holds at every time. These are exclusivity constraints. Without them, a satisfying assignment could pretend the head occupies several squares or the machine inhabits incompatible states.

E fixes the initial configuration: initial state, head at the first square, input symbols written in their positions, and blanks beyond the input. F, G and H enforce the transition function. They relate the scanned symbol and current state to the next state, next head position and rewritten symbol, while unscanned cells retain their contents. I asserts that an accepting state occurs. Cook modifies the machine so it can continue harmlessly after acceptance, allowing histories to share the same horizon T.

Why is A(w) polynomial in |w|? T=Q(n) is polynomial. There are polynomially many time-position cells and a fixed machine contributes only constant-sized state and alphabet sets. Pairwise uniqueness can add powers of T, yet any fixed power of a polynomial is polynomial. The construction algorithm writes all clauses within a polynomial bound. Finally, A(w) is satisfiable exactly when M has an accepting branch on w.

Cook states Theorem 1 using DNF tautology. Negate the CNF formula A(w) and apply De Morgan’s laws. The result is a DNF formula that is a tautology exactly when A(w) is unsatisfiable, so complements must be tracked carefully. In modern language, the construction is usually presented as SAT being NP-complete. The 1971 text reaches the same central universality through its tautology and complement conventions.

The proof has two directions, both necessary. For completeness, take a real accepting computation of M on w and assign every P, Q and S atom according to its frames. The uniqueness, initial, transition and acceptance clauses are then true, so A(w) is satisfiable. For soundness, start with any satisfying assignment. Uniqueness clauses extract one state, one head position and one symbol per cell at each time. Initial and update clauses force those frames to trace a legal run of M, while I forces acceptance. The assignment cannot describe a fictional history that merely resembles one.

Local constraints are the compression device. A formula does not contain a separate clause comparing every complete history with M. It checks bounded neighbourhoods between consecutive frames. Because Turing-machine dynamics are local, global legality follows by induction over time: the initial row is correct, and if row t is correct, the update and frame clauses make row t+1 correct. Polynomially many small obligations replace enumeration of exponentially many branches.

From formulas to bounded clauses and subgraphs

Theorem 2 places four sets in one polynomial degree: tautologies, DNF tautologies, D3, and subgraph pairs. D3 consists of DNF tautologies whose disjuncts contain at most three literals. Once mutual reductions are established, a polynomial algorithm for any one would give polynomial algorithms for all.

The first nontrivial gadget shortens a long conjunction without expanding truth conditions uncontrollably. Suppose a DNF disjunct begins R₁∧R₂∧R₃∧…∧R_s. Introduce a fresh atom p and replace the disjunct by two pieces, p∧R₃∧…∧R_s and ¬p∧R₁∧R₂. Repetition reduces each disjunct to at most three literals while preserving tautologyhood. The fresh atom routes assignments between the retained fragments.

The subgraph construction turns logical consistency into adjacency. Write a D3 formula as C₁∨…∨C_k, with three literals per disjunct. To falsify the formula, select one false literal from each C_i. Selected literals must be mutually consistent: no variable may be demanded both true and false. Build a graph whose vertices are literal positions and whose edges join positions from different disjuncts when their literals are not opposites.

A k-clique selecting one vertex from each disjunct describes a consistent falsifying choice. Cook then attaches sufficiently distinct graph gadgets so a subgraph embedding respects the disjunct groups. Logical selection becomes a graph-embedding question. The proof is specific about what the edges mean: they encode compatibility of falsifying literals, not vague similarity between clauses.

Two exclusions are as informative as the equivalence list. Cook says he cannot add primality or graph isomorphism to the complete degree. Decades later, primality entered P, while graph isomorphism received a quasipolynomial algorithm without becoming known NP-complete. The 1971 caution models correct completeness practice: absence of a reduction is not evidence that a problem belongs to the same degree, and apparent difficulty is not a proof of completeness.

The tautology presentation also reverses modern labels. Satisfiability asks whether there exists a truth assignment making a CNF true, a characteristic NP question. Tautology asks whether every assignment makes a formula true and is naturally associated with the complement class coNP. Cook’s theorem handles this through DNF duality and complements before the later vocabulary settled. Reading “tautology is NP-complete” straight from the page without tracking his sets and reduction direction can therefore generate a historical and logical error.

The common degree is more precise than a list of hard-looking examples. Mutual reducibility says each problem can simulate the others with polynomial overhead under Cook’s query definition. It does not say their best algorithms use the same exponent, memory, constants or data structures. Polynomial degree deliberately discards those differences to expose a coarser structural equivalence.

How should theorem provers be compared?

The title reaches beyond propositional completeness. Predicate-calculus unsatisfiability is semi-decidable: a sound complete proof procedure halts on unsatisfiable formulas, yet no decision procedure halts with a correct yes-or-no answer for every formula. Input length alone cannot yield a recursive worst-case time bound over all terminating cases. Cook therefore seeks a second parameter describing how deep the needed proof evidence lies.

Using Herbrand’s theorem, order the ground substitution instances A₁, A₂, … of a formula’s functional form. For an unsatisfiable A, let φ(A) be the least k such that A₁∧…∧A_k is propositionally inconsistent. A procedure can enumerate instances in that order and test successive finite conjunctions. The parameter records where a contradiction becomes available in this fixed enumeration.

Why is a second parameter unavoidable? Assume a recursive function R(n) bounded the halt time of a complete unsatisfiability procedure for every unsatisfiable formula of length n. Run the procedure for R(n) steps. If it has not halted, declare the formula satisfiable. This would decide predicate-calculus satisfiability, contradicting its undecidability. Formula length alone cannot supply the desired recursive worst-case clock. Restricting attention to formulas with φ(A)≤k creates a finite evidence horizon on which a recursive comparison becomes possible.

The ordering of the Herbrand universe now carries methodological weight. Terms of lower rank are placed earlier, followed by more deeply nested terms. Two procedures may exploit this space differently, but φ(A) is defined independently of the procedure being evaluated. That independence permits comparison. It also creates the crudeness Cook notes: a poor global ordering can make an easy sparse contradiction appear deep.

Cook defines a time function T_Q(k) for a theorem-proving machine Q, bounding its halt time when φ(A)≤k and the formula length is at most about log k. He proves a lower-bound architecture using a reduction from machine non-halting and diagonalisation, and supplies a broad upper bound for a general Herbrand procedure. The scanned typography is difficult, but the conceptual move is clear: compare procedures relative to proof-depth evidence, not formula length alone.

The paper immediately criticises its own measure. φ(A) depends on the ordering of instances, and a contradiction may need only a sparse subset rather than every earlier instance. Cook suggests a multivariable measure, including the minimum number of instances needed. That reservation matters. The predicate-calculus section introduces a research instrument, not a timeless benchmark with established empirical adequacy.

The section also links theorem-prover improvement to deterministic simulation of nondeterminism. Cook’s Theorem 4 shows that a sufficiently good honest T_Q bound would transfer to recognition bounds for languages accepted nondeterministically in exponential time. Conversely, a much stronger lower bound would separate tautology from the easy polynomial degree. The proposed measure sits on the same fault line as the completeness theorem.

A finite SAT witness laboratory

The laboratory accepts a small CNF written with variables x1 to x8, vertical bars for OR, ampersands for AND and tildes for negation. It performs two different tasks. Witness checking evaluates one proposed assignment clause by clause. Exhaustive search enumerates assignments until it finds a satisfying one or exhausts the finite space.

What a positive result permits. A passing witness proves the entered finite formula satisfiable. A successful exhaustive search finds such a witness. An exhausted search proves unsatisfiability for this parsed formula because the finite assignment space was fully enumerated. The artefact makes the verification/search distinction observable.

What a negative result means. A rejected witness says only that this assignment fails; another may work. Exhaustion is stronger for the tiny instance. The laboratory cannot demonstrate an asymptotic lower bound, encode an arbitrary Turing machine automatically, establish NP-completeness, evaluate modern SAT solvers or decide P versus NP. Its enumerator deliberately uses the naïve search that Cook’s theorem does not claim is necessary.

Inspect the counter as variables are added. Verification reads one assignment and a number of literals proportional to the formula. Exhaustive enumeration admits up to 2ⁿ assignments. Cook’s construction concerns a deeper fact: every polynomially bounded nondeterministic computation can manufacture a formula whose satisfying assignments correspond to accepting histories. This tool shows the target semantics, not the full compiler.

Completeness is evidence of concentration, not a lower bound

Cook proves that DNF tautology carries every polynomial-time nondeterministic recognition problem under his P-reducibility. He does not prove tautology lies outside deterministic polynomial time. If tautology were easy, the reductions would make the whole nondeterministic class easy. If one source problem were proved outside P, the complete target would be outside P. Neither premise is supplied by the completeness theorem itself.

The paper says this plainly: no good lower bound for tautology recognition is provided. Completeness gives strong evidence because many apparently difficult problems converge on one target. It changes research strategy. Instead of inventing unrelated hardness stories, a researcher can place problems in a common degree and understand the consequences of one algorithm or lower bound.

Completeness also changes what counts as a negative result. A failed attempt to design a fast subgraph algorithm remains inconclusive. A proof that subgraph pairs are complete explains why success would have consequences far beyond graphs. Researchers may still search for an algorithm, but they should expect it to resolve the whole class or exploit a restriction absent from the general encoding. Parameter bounds, planarity, bounded degree or special clause structure can create tractable islands without contradicting worst-case completeness.

Formula size deserves the same restraint. Cook proves a polynomial upper bound on the compiler’s output, not that his encoding is the smallest possible. Later presentations improve gadgets and clause counts. Those refinements matter for concrete solvers but leave completeness intact. The theorem needs a fixed polynomial, answer-preserving transformation. It does not require a practical reduction for every downstream workload.

Karp’s 1972 successor converted that possibility into a landscape. He gave reductions among 21 combinatorial problems involving covering, packing, routing, assignment and sequencing. Karp also helped standardise the many-one reduction methodology. His result strengthens the practical breadth of Cook’s framework; it does not strengthen Cook’s theorem into a proof that P differs from NP.

Baker, Gill and Solovay later exposed a proof-method boundary. They built an oracle A relative to which P equals NP and an oracle B relative to which P differs from NP. Any argument that survives unchanged under every oracle cannot settle the unrelativised question. This does not criticise the correctness of Cook’s reduction. It shows why familiar diagonal and simulation techniques may be insufficient for the separation Cook identified.

As of 1 September 2026, the Clay Mathematics Institute still lists P versus NP as unsolved. The open question is often phrased as whether solutions that are easy to check are also easy to find, but care is required. P and NP are classes of decision languages. Search versions, optimisation versions and average-case behaviour require reductions or additional definitions.

The professional lesson is diagnostic rather than promotional. Before calling a task hard, specify the decision language, encoding, input length, resource bound and reduction direction. Before using a completeness result to explain observed runtime, ask whether the workload is worst-case, parameterised, approximate, randomised or distributional. Completeness maps transferable consequences. It does not replace algorithm analysis or measurement.

Recover the proof from five objects

Three confusions can now be repaired from the spine. Nondeterminism is an existential branch condition, not free parallel hardware. The formula does not simulate every branch sequentially; one assignment proposes one complete history. A reduction is not a similarity claim; it is an explicit bounded procedure preserving membership in the stated direction.

Where Cook redirects the canon

Paper 0008 remains in Stage S0, module S0M1. Church and Turing established what no effective method can decide. Shannon measured information carried by selections. Solomonoff, Kolmogorov and Chaitin priced descriptions. Cook adds resource-bounded universality: among decidable finite problems, one target can represent the difficulty of every efficiently checkable acceptance process.

The closest prerequisite is Paper 0002, which supplies machine configurations and bounded computation. Paper 0003 supplies bit length and asymptotic counting. Paper 0007 supplies the habit of separating computability from a resource measure. Cobham’s polynomial feasibility boundary is the immediate external prerequisite. Cook’s new capability is reduction as a proof instrument: translate instances, preserve answers and transfer algorithmic consequences.

The strongest immediate successor is Karp’s 1972 reduction network. The strongest early proof-method boundary is Baker, Gill and Solovay’s relativisation result. Neither alters Theorem 1. Together they show the two directions opened by Cook: spread completeness across natural problems, and understand why proving a separation resists familiar techniques.

The next three canon papers create a deliberately varied continuation. Paper 0009, Chaitin (1975), returns from runtime to self-delimiting programme size and information identities, sharpening what counts as a description. Paper 0010, Valiant (1984), adds polynomial resources and probabilistic success to learning from examples. Paper 0011, Feynman (1982), asks whether physical simulation changes the computational model and its feasible processes.

The durable lesson

Cook’s achievement is a compiler for difficulty. A bounded accepting history can be expressed by variables and local constraints; the resulting formula preserves existence of that history. Once this compiler exists, an algorithm for the target would propagate through an entire class, and a lower bound for any source would propagate to the target. The theorem earns that concentration of consequences. The final separation remains outside the receipt.