Read-back: PvsNP.cook_levin

Statement. The theorem asserts a single closed proposition with no free variables, hypotheses or typeclass assumptions:

$$\mathrm{NPComplete}(\mathrm{SAT}),$$

i.e. the set $\mathrm{SAT}$ of binary strings defined below belongs to the class $\mathrm{NP}$ defined below, and every language $L'$ in that class $\mathrm{NP}$ is polynomial-time reducible (in the sense defined below) to $\mathrm{SAT}$. Everything named here is a custom definition from the accompanying file; each is unfolded below down to standard notions.

---

Strings and languages

A string is a finite list $w$ of booleans (a word over the two-letter alphabet $\{\mathsf{false},\mathsf{true}\}$, i.e. $\{0,1\}$); $|w|$ denotes its length. A language is an arbitrary set of such strings (no computability or decidability is imposed on a language as such), and $w\in L$ is ordinary set membership.

The machine model (Mathlib's bundled two-stack-style machine "TM2")

A machine $M$ consists of:

• a type $K$ of stack names which is finite and has decidable equality, together with two distinguished names $k_0$ (input stack) and $k_1$ (output stack) — $k_0=k_1$ is allowed;
• for each stack name $k$ a type $\Gamma_k$ of stack symbols; only $\Gamma_{k_0}$ is required to be finite (the other $\Gamma_k$ are arbitrary types);
• a finite type $\Lambda$ of labels with a distinguished label $\mathsf{main}$;
• a finite type $\Sigma$ of internal states with a distinguished initial state $s_0$;
• a program $m$ assigning to each label $\ell\in\Lambda$ a statement $m(\ell)$.

A statement is a finite tree built from the constructors: push a symbol $f(v)\in\Gamma_k$ (depending on the current internal state $v$) onto stack $k$ and continue; peek at the top of stack $k$ (an optional symbol) and update the internal state by an arbitrary function $\Sigma\times(\Gamma_k\cup\{\bot\})\to\Sigma$, then continue; pop the top of stack $k$ and update the state likewise, then continue; load, i.e. replace the state by $g(v)$ for an arbitrary $g:\Sigma\to\Sigma$, then continue; branch on a boolean function of the state to one of two continuations; goto a label $h(v)$ depending on the state; or halt. All the functions occurring in statements are arbitrary (set-theoretic) functions; no effectiveness is required of them.

A configuration is a triple (current label or "halted", internal state $v\in\Sigma$, and for each $k\in K$ a finite list $S_k$ of symbols of $\Gamma_k$ — the stacks, top of stack first). The step function is: a halted configuration has no successor; a configuration with label $\ell$ has exactly one successor, obtained by executing the entire statement $m(\ell)$ (all its pushes, pops, peeks, loads and branches, however many) until it reaches a goto (which sets the new label) or a halt (which sets the label to "halted"). Thus one "step" is the execution of one whole statement block.

For an input list $s$ of symbols of $\Gamma_{k_0}$, the initial configuration $\mathrm{init}(s)$ has label $\mathsf{main}$, state $s_0$, stack $k_0$ equal to $s$, and every other stack empty. For an output list $t$ of symbols of $\Gamma_{k_1}$, the halting configuration $\mathrm{halt}(t)$ has label "halted", state $s_0$ (the initial state), stack $k_1$ equal to $t$, and every other stack empty.

"$M$ outputs $t$ on input $s$ within $N$ steps" means: there is a natural number $n\le N$ such that iterating the step function exactly $n$ times starting from $\mathrm{init}(s)$ (where "no successor" is absorbing) yields exactly the configuration $\mathrm{halt}(t)$. In particular the machine must stop with its internal state reset to $s_0$, with all stacks other than $k_1$ empty, and with stack $k_1$ holding exactly $t$.

Polynomial-time computability of a function relative to encodings

Given types $A,B$, alphabets $\alpha,\beta$, encodings $e_A:A\to\alpha^{*}$ and $e_B:B\to\beta^{*}$ (lists of letters), and a function $f:A\to B$, the structure "$f$ is TM2-computable in polynomial time w.r.t. $e_A,e_B$" consists of:

• a machine $M$ as above;
• a bijection $\iota:\Gamma_{k_0}\cong\alpha$ between the input-stack alphabet and $\alpha$, and a bijection $\omega:\Gamma_{k_1}\cong\beta$ between the output-stack alphabet and $\beta$;
• a polynomial $p\in\mathbb{N}[X]$ with natural-number coefficients;
• for every $a\in A$: $M$ outputs $\omega^{-1}(e_B(f(a)))$ (the letter-by-letter preimage of the encoded output) on input $\iota^{-1}(e_A(a))$ within $p(|e_A(a)|)$ steps, where $|e_A(a)|$ is the length of the encoded input.

Every use below is of the form "there exists at least one such structure" (mere existence, no particular machine is fixed).

The encodings used are:

• $\mathrm{id}$ on strings: a string $w\in\{0,1\}^{*}$ is its own code, alphabet $\{0,1\}$;
• $\mathrm{encodeBool}(b)=[b]$: a boolean is coded as the one-letter string $[b]$, alphabet $\{0,1\}$;
• $\mathrm{encodePair}(x,y)$ for a pair of strings: the letters of $x$ each tagged "left" followed by the letters of $y$ each tagged "right", a string over the four-letter alphabet $\{0,1\}\sqcup\{0,1\}$; its length is $|x|+|y|$.

Hence:

• $\chi$ is a polynomial-time decider ($\chi:\{0,1\}^{*}\to\{\mathsf{true},\mathsf{false}\}$): there exist a machine, alphabet bijections $\Gamma_{k_0}\cong\{0,1\}$, $\Gamma_{k_1}\cong\{0,1\}$, and a polynomial $p\in\mathbb{N}[X]$ such that for every string $w$ the machine, started on $w$, halts (in the strict sense above) with output stack holding exactly the single letter $\chi(w)$ within $p(|w|)$ steps.
• $R$ is a polynomial-time checker ($R:\{0,1\}^{*}\times\{0,1\}^{*}\to\{\mathsf{true},\mathsf{false}\}$): the same with input alphabet in bijection with $\{0,1\}\sqcup\{0,1\}$, input $\mathrm{encodePair}(x,y)$, output the single letter $R(x,y)$, within $p(|x|+|y|)$ steps.
• $f$ is polynomial-time computable ($f:\{0,1\}^{*}\to\{0,1\}^{*}$): the same with both alphabets in bijection with $\{0,1\}$, input $w$, output exactly the string $f(w)$, within $p(|w|)$ steps.

The classes and reducibility

• $L\in\mathrm{NP}$ iff there exist a function $R:\{0,1\}^{*}\times\{0,1\}^{*}\to\{\mathsf{true},\mathsf{false}\}$ and a natural number $k\in\mathbb{N}$ (with $k=0$ allowed) such that $R$ is a polynomial-time checker and, for every string $w$,

$$w\in L \iff \exists\,y\in\{0,1\}^{*},\ |y|\le |w|^{k}\ \text{ and }\ R(w,y)=\mathsf{true}.$$

Here $|w|^{k}$ is natural-number exponentiation with $|w|^{0}=1$ (including $0^{0}=1$); for $k\ge1$ and $w$ the empty string the only admissible certificate $y$ is the empty string.

• $L_1$ is polynomial-time reducible to $L_2$ (written $L_1\le_P L_2$) iff there exists $f:\{0,1\}^{*}\to\{0,1\}^{*}$ which is polynomial-time computable in the above sense and such that for every string $x$,

$$x\in L_1 \iff f(x)\in L_2 .$$

• $L$ is NP-complete iff $L\in\mathrm{NP}$ and for every language $L'$ with $L'\in\mathrm{NP}$, $L'\le_P L$.

(The file also defines a class $\mathrm{P}$, a class $\mathrm{E}$ and a language $\mathrm{ThreeSAT}$; none of these occurs in the theorem.)

Formulas and their string coding

• A literal is a pair $(s,i)$ with $s$ a boolean (sign) and $i\in\mathbb{N}$ (variable index). A clause is a finite list of literals. A CNF formula $F$ is a finite list of clauses. Duplicates and any ordering are allowed; the empty clause and the empty formula are allowed.
• For an assignment $\tau:\mathbb{N}\to\{\mathsf{true},\mathsf{false}\}$: the literal $(\mathsf{true},i)$ evaluates to $\tau(i)$ and $(\mathsf{false},i)$ to $\neg\tau(i)$; a clause evaluates to $\mathsf{true}$ iff some literal in it does (the empty clause evaluates to $\mathsf{false}$); $F$ evaluates to $\mathsf{true}$ iff every clause in it does (the empty formula evaluates to $\mathsf{true}$).
• $F$ is satisfiable iff there exists $\tau:\mathbb{N}\to\{\mathsf{true},\mathsf{false}\}$ (an arbitrary function, defined on all of $\mathbb{N}$) under which $F$ evaluates to $\mathsf{true}$.

The coding of formulas as binary strings, writing $0$ for $\mathsf{false}$ and $1$ for $\mathsf{true}$:

• $\mathrm{bits}(i)$ is the binary expansion of $i\in\mathbb{N}$ written least-significant bit first with no leading zeros, so $\mathrm{bits}(0)=[\,]$ (empty), $\mathrm{bits}(1)=[1]$, $\mathrm{bits}(2)=[0,1]$, $\mathrm{bits}(6)=[0,1,1]$, and for $i>0$ the last bit is $1$.
• A literal $(s,i)$ is coded by taking the list $s::\mathrm{bits}(i)$ (sign first, then the bits), replacing each of its entries $b$ by the two letters $0\,b$, and then appending the terminator $1\,0$:

$$\mathrm{encodeLiteral}(s,i) \;=\; 0\,s\;\;0\,b_0\;\;0\,b_1\cdots 0\,b_{r-1}\;\;1\,0, \qquad \mathrm{bits}(i)=[b_0,\dots,b_{r-1}].$$

For example $(\mathsf{true},0)\mapsto 0\,1\,1\,0$ and $(\mathsf{false},2)\mapsto 0\,0\,0\,0\,0\,1\,1\,0$.

• A clause is coded by concatenating the codes of its literals in order and appending the terminator $1\,1$; the empty clause is coded as $1\,1$.
• A formula is coded by concatenating the codes of its clauses in order, with no further delimiter; the empty formula is coded as the empty string.

Finally,

$$\mathrm{SAT} \;=\; \{\,w\in\{0,1\}^{*} \;:\; \exists\,F \text{ a CNF formula with } \mathrm{encodeCNF}(F)=w \text{ and } F \text{ satisfiable}\,\}.$$

Thus a string is in $\mathrm{SAT}$ iff it is the exact code of some satisfiable formula; strings that are not codes of any formula are not in $\mathrm{SAT}$; the empty string is in $\mathrm{SAT}$ (it codes the empty formula, which is satisfiable); the string $1\,1$ (code of the formula consisting of one empty clause) is not.

The assertion, assembled

The theorem asserts both of the following:

1. $\mathrm{SAT}\in\mathrm{NP}$: there exist $R:\{0,1\}^{*}\times\{0,1\}^{*}\to\{\mathsf{true},\mathsf{false}\}$ and $k\in\mathbb{N}$, such that some machine of the kind described (with input alphabet in bijection with $\{0,1\}\sqcup\{0,1\}$, output alphabet in bijection with $\{0,1\}$, some polynomial $p\in\mathbb{N}[X]$) computes $R$ on every tagged pair $\mathrm{encodePair}(x,y)$ within $p(|x|+|y|)$ steps, halting exactly in the configuration with output stack $[R(x,y)]$, all other stacks empty and internal state reset to the initial state, and such that for every string $w$: $w$ is the code of a satisfiable CNF formula iff there is a string $y$ with $|y|\le|w|^{k}$ and $R(w,y)=\mathsf{true}$.

2. Every $L'\in\mathrm{NP}$ reduces to $\mathrm{SAT}$: for every set $L'$ of binary strings for which there exist $R',k'$ as in the definition of $\mathrm{NP}$, there exists a function $f:\{0,1\}^{*}\to\{0,1\}^{*}$, computed by some machine of the kind described (both stack alphabets $\Gamma_{k_0},\Gamma_{k_1}$ in bijection with $\{0,1\}$) within $p(|x|)$ steps for some polynomial $p\in\mathbb{N}[X]$ on every input $x$ (halting exactly with output stack $f(x)$, other stacks empty, state reset), such that for every string $x$: $x\in L'$ iff $f(x)$ is the code of a satisfiable CNF formula.