Read-back: PvsNP.ladner

The statement

Let $\Sigma^*$ denote the set of all finite strings over the two-letter alphabet $\{\mathsf{true},\mathsf{false}\}$ (finite lists of Booleans; the empty string is included). A language is any subset $L \subseteq \Sigma^*$ (any set whatsoever, with no computability or decidability requirement). Below, $\mathbf{P}$, $\mathbf{NP}$ and "$L$ is $\mathbf{NP}$-complete" are the specific notions defined in the accompanying definition file, unfolded in full in the next sections; they are not Mathlib's or the textbook's notions.

The declaration asserts:

Hypothesis. $\mathbf{P} \neq \mathbf{NP}$, i.e. the two sets of languages $\mathbf{P}$ and $\mathbf{NP}$ (both subsets of the power set of $\Sigma^*$) are not equal as sets. Nothing else is assumed: no inclusion $\mathbf{P} \subseteq \mathbf{NP}$ is hypothesised, and there are no other explicit, implicit, or typeclass hypotheses.

Conclusion. There exists a language $L \subseteq \Sigma^*$ such that all three of the following hold:

1. $L \in \mathbf{NP}$;
2. $L \notin \mathbf{P}$;
3. $L$ is not $\mathbf{NP}$-complete, i.e. it is not the case that ($L \in \mathbf{NP}$ and every $L' \in \mathbf{NP}$ is polynomial-time many-one reducible to $L$). Since item 1 already gives $L \in \mathbf{NP}$, item 3 amounts to: there is some language $L' \in \mathbf{NP}$ that is not polynomial-time many-one reducible to $L$ (in the specific sense of "reducible" unfolded below).

The existential is a plain "there exists" (not "there exists a unique"). The statement is a bare implication from the hypothesis to the conclusion; it says nothing about the case $\mathbf{P} = \mathbf{NP}$.

The machine model underlying every complexity notion

All of $\mathbf{P}$, $\mathbf{NP}$ and reducibility are phrased via one Mathlib notion, "$f$ is computable in polynomial time by a finite stack machine with respect to input encoding $e_{\mathrm{in}}$ and output encoding $e_{\mathrm{out}}$", written here $\mathrm{PolyTM}(e_{\mathrm{in}}, e_{\mathrm{out}}, f)$. It unfolds as follows.

Finite stack machine (Mathlib FinTM2). A machine $M$ consists of:

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

A statement is a finite tree built from: $\mathsf{push}\,k\,f\,q$ (push the symbol $f(s) \in \Gamma_k$, computed from the current internal state $s$, onto stack $k$, then continue with $q$); $\mathsf{peek}\,k\,f\,q$ (replace the internal state by $f(s, \text{top of stack } k)$, where the top is "none" if the stack is empty, then continue with $q$); $\mathsf{pop}\,k\,f\,q$ (same as peek but also remove the top of stack $k$, if any); $\mathsf{load}\,f\,q$ (replace the internal state by $f(s)$, then continue with $q$); $\mathsf{branch}\,b\,q_1\,q_2$ (continue with $q_1$ or $q_2$ according to the Boolean $b(s)$); $\mathsf{goto}\,g$ (end this statement and jump to label $g(s)$); $\mathsf{halt}$ (end this statement and enter the halted status). The functions $f, g, b$ here are arbitrary set-theoretic functions of the finite state $s$ (no computability restriction is imposed on them).

A configuration is a triple $(\ell, s, \vec{\sigma})$: a current label $\ell \in \Lambda$ or the special value "halted"; an internal state $s \in S$; and, for every stack name $k$, a finite list $\sigma_k$ of symbols from $\Gamma_k$ (the stack contents; the head of the list is the top of the stack). The one-step function $\mathrm{step}_M$ is: on a halted configuration it is undefined (returns "none"); on $(\ell, s, \vec\sigma)$ it executes the entire statement $m(\ell)$ (all of its pushes, pops, peeks, loads and branches) until it reaches a $\mathsf{goto}\,g$ or $\mathsf{halt}$, yielding the configuration $(g(s'), s', \vec\sigma')$ resp. $(\text{halted}, s', \vec\sigma')$. Thus one "step" is the execution of one whole labelled statement, however many stack operations it contains.

Initial and final configurations. For a list $w$ of symbols of $\Gamma_{k_0}$, the initial configuration $\mathrm{init}_M(w)$ is $(\mathsf{main}, s_0, \vec\sigma)$ with $\sigma_{k_0} = w$ and every other stack empty. For a list $u$ of symbols of $\Gamma_{k_1}$, the final configuration $\mathrm{final}_M(u)$ is $(\text{halted}, s_0, \vec\sigma)$ with $\sigma_{k_1} = u$ and every other stack empty. Note that the final configuration requires the internal state to be back at the initial state $s_0$ and requires all stacks other than $k_1$ to be empty.

Outputs within a time bound. "$M$ on input $w$ outputs $u$ within $t$ steps" means: there is a natural number $n \le t$ such that iterating $\mathrm{step}_M$ exactly $n$ times from $\mathrm{init}_M(w)$ (propagating "undefined" once it appears) yields precisely the configuration $\mathrm{final}_M(u)$. Since the step function is undefined on halted configurations, this forces the run to first become halted exactly at step $n$, in exactly the configuration $\mathrm{final}_M(u)$. (Because $\mathrm{init}_M(w)$ is not halted, necessarily $n \ge 1$.)

Polynomial-time computability of a function. Given types $A, B$, an input encoding $e_{\mathrm{in}} : A \to \text{(lists over an alphabet } \Gamma_{\mathrm{in}})$, an output encoding $e_{\mathrm{out}} : B \to \text{(lists over } \Gamma_{\mathrm{out}})$, and a function $f : A \to B$, the proposition $\mathrm{PolyTM}(e_{\mathrm{in}}, e_{\mathrm{out}}, f)$ says: there exists (mere existence, as a proposition) a finite stack machine $M$ together with

• a bijection $\iota : \Gamma_{k_0} \cong \Gamma_{\mathrm{in}}$ between the input-stack alphabet and $\Gamma_{\mathrm{in}}$,
• a bijection $\omega : \Gamma_{k_1} \cong \Gamma_{\mathrm{out}}$ between the output-stack alphabet and $\Gamma_{\mathrm{out}}$,
• a polynomial $p$ with natural-number coefficients,

such that for every $a \in A$: $M$ on input $\iota^{-1}(e_{\mathrm{in}}(a))$ (the encoding of $a$, transported symbol-by-symbol onto the input alphabet) outputs $\omega^{-1}(e_{\mathrm{out}}(f(a)))$ within $p\big(|e_{\mathrm{in}}(a)|\big)$ steps, where $|\cdot|$ is list length. For the empty encoding ($|e_{\mathrm{in}}(a)| = 0$) the bound is the constant term $p(0)$.

The three encodings used below are:

• $\mathrm{id}$ on $\Sigma^*$: a string encodes itself, over the alphabet $\{\mathsf{true},\mathsf{false}\}$;
• $\mathrm{enc}_{\mathbb B}$ on Booleans: $b \mapsto [b]$, the one-symbol string, over $\{\mathsf{true},\mathsf{false}\}$;
• $\mathrm{enc}_{\times}$ on pairs of strings $(x, y)$: the list $\mathrm{inl}(x_1)\cdots\mathrm{inl}(x_{|x|})\,\mathrm{inr}(y_1)\cdots\mathrm{inr}(y_{|y|})$ over the four-symbol alphabet $\{\mathsf{true},\mathsf{false}\} \sqcup \{\mathsf{true},\mathsf{false}\}$ (the two copies tag which component each symbol came from); its length is $|x| + |y|$.

The class $\mathbf{P}$

$L \in \mathbf{P}$ iff there exists a function $\chi : \Sigma^* \to \{\mathsf{true},\mathsf{false}\}$ such that

• $\mathrm{PolyTM}(\mathrm{id}, \mathrm{enc}_{\mathbb B}, \chi)$ holds — i.e. some finite stack machine with two-symbol input and output alphabets, on every input string $w$ (placed on the input stack as is), halts in the final configuration whose output stack holds exactly the single symbol $\chi(w)$ (and with internal state $s_0$ and all other stacks empty) within $p(|w|)$ steps for a fixed polynomial $p$ with natural coefficients; and
• for every string $w$: $w \in L \iff \chi(w) = \mathsf{true}$.

The class $\mathbf{NP}$

$L \in \mathbf{NP}$ iff there exist a function $R : \Sigma^* \times \Sigma^* \to \{\mathsf{true},\mathsf{false}\}$ and a natural number $k$ (with $k = 0$ allowed) such that

• $\mathrm{PolyTM}(\mathrm{enc}_{\times}, \mathrm{enc}_{\mathbb B}, R)$ holds — i.e. some finite stack machine whose input-stack alphabet is in bijection with the four-symbol alphabet $\{\mathsf{true},\mathsf{false}\} \sqcup \{\mathsf{true},\mathsf{false}\}$ and whose output-stack alphabet is in bijection with $\{\mathsf{true},\mathsf{false}\}$, on every input $\mathrm{enc}_\times(w, y)$, halts in the final configuration with output stack exactly $[R(w,y)]$ within $p(|w| + |y|)$ steps for a fixed polynomial $p$ with natural coefficients; and
• for every string $w$:

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

Edge cases of the certificate bound $|y| \le |w|^k$: for $k = 0$ the bound is $|y| \le 1$ for every $w$ (including $|w| = 0$, since $0^0 = 1$); for $k \ge 1$ and $w$ the empty string the bound is $|y| \le 0$, so only the empty certificate is permitted. The time bound for $R$ is polynomial in $|w| + |y|$, not directly in $|w|$.

Polynomial-time reducibility and $\mathbf{NP}$-completeness

$L_1$ is polynomial-time (many-one) reducible to $L_2$, written $L_1 \le_p L_2$, iff there exists $f : \Sigma^* \to \Sigma^*$ such that

• $\mathrm{PolyTM}(\mathrm{id}, \mathrm{id}, f)$ holds — i.e. some finite stack machine with two-symbol input and output alphabets, on every input string $x$, halts in the final configuration whose output stack holds exactly the string $f(x)$ (internal state $s_0$, all other stacks empty) within $p(|x|)$ steps for a fixed polynomial $p$ with natural coefficients; and
• for every string $x$: $x \in L_1 \iff f(x) \in L_2$.

$L$ is $\mathbf{NP}$-complete iff $L \in \mathbf{NP}$ and for every language $L'$ with $L' \in \mathbf{NP}$, $L' \le_p L$.

Summary of what is asserted, in these terms

If the set of languages $\mathbf{P}$ (those decided by a polynomially step-bounded finite stack machine as above) differs from the set of languages $\mathbf{NP}$ (those with a polynomially step-bounded checker $R$ and certificates of length at most $|w|^k$ as above), then some language $L \subseteq \Sigma^*$ lies in $\mathbf{NP}$, does not lie in $\mathbf{P}$, and fails to be $\mathbf{NP}$-complete — so, given $L \in \mathbf{NP}$, some $L' \in \mathbf{NP}$ admits no function $f$ that is computable by a polynomially step-bounded finite stack machine (in the exact sense above) and satisfies $x \in L' \iff f(x) \in L$ for all $x$.