Introduction and Background
The \(\mathsf{P}\) versus \(\mathsf{NP}\) question asks: is it possible to determine whether a Boolean formula is satisfiable, in time polynomial in the length of the formula? Determining whether a Boolean formulas is satisfiable is called the SAT problem, and programs which solve the problem are called SAT solvers. SAT solvers are used in many modern programming tools (usually, for automatically solving some system of constraints), so the SAT problem is of great practical importance today. And it is often suggested that a solution to “\(\mathsf{P}\) versus \(\mathsf{NP}\)” would resolve whether there exists any efficient algorithm at all for SAT.
There are a number of reasons why this suggestion could be wrong, or at least, a number of ways to argue against it. But here’s a particular thought: what if \(\mathsf{P} = \mathsf{NP}\) (that is, SAT can be solved in polynomial time), but the polynomial-time algorithm is beyond our ability to find – and in particular, beyond our ability to prove correct? What if there exists some magic algorithm that happens to work, but there doesn’t exist any proof that it works? Or perhaps there doesn’t exist any proof that it runs in polynomial time? Such a scenario would be an unsatisfying resolution to \(\mathsf{P}\) versus \(\mathsf{NP}\), in a way: because practically speaking, we generally only trust algorithms that we can prove correct.
The question I’m trying to motivate is: does \(\mathsf{ProvableP} = \mathsf{ProvableNP}\)? That is, what happens if we restrict our attention to algorithms which can be proven correct? Is this question answerable, or is it just as hard as \(\mathsf{P}\) versus \(\mathsf{NP}\)?
Summary
It turns out that \(\mathsf{P} = \mathsf{NP}\) if and only if \(\mathsf{ProvableP} = \mathsf{ProvableNP}\). I’ll define what I mean by \(\mathsf{ProvableP}\) and \(\mathsf{ProvableNP}\). This post is adapted from a question and answer I made on Computer Science StackExchange.
The ProvableP versus ProvableNP question
Fix a logic \(\mathcal{L}\) that is strong enough to encode statements about Turing machines. By this I mean the same requirements as Godel’s second incompleteness theorem; but for the purposes of this question, just assume the following:
-
\(\mathcal{L}\) is consistent (it doesn’t prove False); and
-
\(\mathcal{L}\) implies the Peano arithmetic axioms of \(\mathbb{N}\) (PA).
Then define
\[\begin{align*} \mathsf{ProvableP} &:= \{A \mid \mathcal{L} \text{ proves } [A \in P]\} \\ \mathsf{ProvableNP} &:= \{A \mid \mathcal{L} \text{ proves } [A \in NP] \} \end{align*}\]There’s an issue with this definition: how do we encode languages \(A\) (of which there are uncountably many) as finite objects in order for the logic \(\mathcal{L}\) to have something to say about them? In particular, how do we encode formulas for \([A \in \mathsf{P}]\) and \([A \in \mathsf{NP}]\)? Let us assume that languages are subsets of the natural numbers \(\mathbb{N}\), and that any \(A\) in \(\mathsf{ProvableP}\) or \(\mathsf{ProvableNP}\) must be given by an arbitrary formula of the symbols of \(\mathcal{L}\), i.e. it is any definable subset of \(\mathbb{N}\).
From the definition we have that \(\mathsf{ProvableP} \subseteq \mathsf{ProvableNP} \subseteq \mathsf{NP}\). But does \(\mathsf{ProvableP} = \mathsf{ProvableNP}\)? How does this relate to the original \(\mathsf{P}\) vs \(\mathsf{NP}\) question?
The Answer
Obligatory warning: to my knowledge, this proof has not been rigorously checked by someone else :) But we now argue that
\[\boxed{\mathsf{ProvableP} = \mathsf{ProvableNP} \;\;\text{ if and only if }\;\;\mathsf{P} = \mathsf{NP}.}\]For the forward direction, assume \(\mathsf{ProvableP} = \mathsf{ProvableNP}\), and consider any language \(A\) in \(\mathsf{NP}\). Note that \(A\) is accepted by a nondeterministic Turing machine \(N\), such that there exists a polynomial \(p(n)\) which bounds the longest execution branch of \(N\) on input a string of length \(n\). Then let \(N'\) be a nondeterministic Turing machine with the following description: first, count the input length \(n\); second, calculate \(p(n)\); and finally, runs \(N\) for at most \(p(n)\) steps nondeterministically. If \(N\) doesn’t halt (this never actually occurs, but \(N'\) doesn’t know that for sure), \(N'\) rejects.
Now observe that \(\mathcal{L}\) (more specifically, PA) proves that \(N'\) runs in time \(p(n)\). Moreover, \(\mathcal{L}\) can describe “the language of strings accepted by \(N'\)” by a formula (roughly, “there exists an sequence of configurations such that the sequence is a run of \(N'\) and ends in an accept state”). Then we have that \(\mathcal{L}\) proves \([L(N') \in \mathsf{NP}]\). Therefore, \(L(N') \in \mathsf{ProvableNP}\). But we know (even if \(\mathcal{L}\) doesn’t) that \(L(N') = L(N) = A\) by construction. So \(A \in \mathsf{ProvableNP}\). But \(\mathsf{ProvableNP} = \mathsf{ProvableP} \subseteq \mathsf{P}\), so \(A \in \mathsf{P}\).
The backward direction is a similar trick. Assume \(\mathsf{P} = \mathsf{NP}\) and that \(A \in \mathsf{ProvableNP}\). Then \(\mathsf{ProvableNP} \subseteq \mathsf{NP} = \mathsf{P}\), so \(A \in \mathsf{P}\). From here, we know there is some Turing machine \(M\) and polynomial \(p(n)\) such that \(M\) runs in time \(p(n)\) and \(L(M) = A\). Let \(M'\) be a deterministic Turing machine which, on input of length \(n\), first calculates \(p(n)\), and then runs \(M\) for at most \(p(n)\) steps. If \(M\) doesn’t halt, \(M'\) returns a default value, say \(0\).
Then similarly to before, \(\mathcal{L}\) proves that \(M'\) halts in time \(p(n)\) and therefore that \([L(M') \in \mathsf{P}]\). it follows that \(L(M') \in \mathsf{ProvableP}\), but we know (even if \(\mathcal{L}\) doesn’t) that \(L(M') = L(M) = A\). Thus, \(\mathsf{ProvableNP} = \mathsf{ProvableP}\). \(\quad \square\)