# Proof Complexity of a Proof or Disproof of P = NP

Has there been any research on the proof complexity of a resolution to the P=NP problem? If not, given the lack of progress on the problem, would it be unreasonable to conjecture that any proof that resolves the P=NP problem will require a super-polynomial number of steps?

• Maybe I'm not understanding your question but any resolution to P vs NP would be a constant sized proof, yes? – Kurt Mueller Nov 28 '16 at 15:44
• @Kurt Muller. The proof will require a super-polynomial number of steps based on the number of symbols that are required to encode the P=NP problem. – Tony Johnson Nov 28 '16 at 20:01
• @TonyJohnson Superpolynomial in a constant is still a constant. – David Richerby Nov 29 '16 at 21:23

It is known that any proof of super-polynomial circuit lower bounds (which are slightly stronger statements than $P\neq NP$) require super-polynomial, even exponential size proofs in weak proof systems like resolution. Generalizing this to stronger proof systems is a well known open problem.

See section 5 of this survey by A. Razborov where these things are shown.

Proof complexity only makes sense when there is a sequence of statements depending on a parameter $n$. For example, the proposition $\mathsf{PHP}_n$ states (informally) that there is no bijection $[n+1] \to [n]$. This sequence of propositions is hard for certain propositional proof systems.

The statement $\mathsf{P} \neq \mathsf{NP}$ is a single statement, so you can't apply proof complexity to it directly. However, the following sequence of statements does make sense, for particular functions $s(n)$: "there is no circuit of size $s(n)$ correctly solving SAT for instances of length $n$". This has been considered in the literature, for example by Razborov (who considered the setting of uniform proof complexity, i.e., bounded arithmetic).

We have 3 cases:

• There exists a proof that $P = NP$. Than there's an algorithm solving the problem "Emit a proof that $P=NP$" that runs in $O(1)$ time. It hard-codes the proof in the Turing Machine itself, and emits it. It runs in the same time no matter its input.

• Similarly, if there exists a proof that $P\neq NP$, than we can write an algorithm emitting this proof in $O(1)$ time.

• If there exists no proof of either case, than the minimum complexity of finding a proof for either is $O(\infty)$: no Turing Machine can ever halt and emit a proof of either, since no such proofs exist.

Just because we haven't found any proof doesn't mean that it doesn't exist, and the complexity classes are defined in terms of what exists.

More precisely, we can't know precisely how hard it is to find a proof of $P=NP$ or the converse until we know the result, which kind of defeats the point.

What we do know is that, in general, the problem of "Take a statement in Predicate logic and determine if there's a proof for it" is undecidable. So there are no generic proof-generating procedures that we can plug P vs NP into, that are guaranteed to produce a result.

If P = NP then all you need to do is to create a polynomial time algorithm for solving some NP-complete problem, and prove that it is indeed polynomial (which might be hard, for example the Simplex algorithm usually runs very fast but proving that it runs fast seems incredibly difficult).

Ok, this might be very difficult. Assume we find an algorithm that supposedly solves the Traveling Salesman problem in O ($n^{100}$). Tough. We can't even measure the execution time for a problem with two cities.

• OK, but I don't see how this answers the question. Proof complexity is a specific field of computer science; the question isn't just asking "How difficult would it be to resolve $\mathbf{P}\overset{?}=\mathbf{NP}\,$?" – David Richerby Nov 29 '16 at 21:22
• There's also the (unlikely but entirely possible) outcome that P=NP but there is no provably uniformly polynomial-time algorithm for e.g. SAT. – Steven Stadnicki Nov 29 '16 at 22:41