The qualifier "natural" is meant to exclude examples like "PA + P=NP" or "PA + True $\Pi_1$".
For concreteness, let's say that "natural" = sound, computably enumerable, with a feasible proof-checker.

Context of the question.

A naive way to approach the P vs NP problem, from the logical point of view, could go like this:

  1. Show that if P=NP, then P=NP is provable is some fixed system $S$, such as ZFC or ZFC+large cardinals;
  2. Improve the previous result for weaker and weaker $S$ $-$ for example, go from ZFC down to PA2, PA, $I\Sigma_1$, etc.;
  3. Once $S$ is as elementary as possible, use an ad-hoc argument to show $\not \vdash_S$ P=NP.

Of course, as all known approaches to the problem, this one quickly falls upon itself.

Proposition. (folklore?) For every function $f$ which is computed by a Turing machine $M$, and for every natural formal system $S$, which proves that $M$ computes $f$, there exists a Turing machine $M'$ which computes $f$, such that $S$ does not prove that $M'$ computes $f$. The runtime of $M'$ is $O(n+Time(M))$.

Given input $x$, the machine $M'$ searches for a contradiction in $S$ for $|x|$ many steps. If no contradiction is found, it runs $M$ on $x$, returning the result; otherwise, it launches all nuclear missiles at once.

Of course, $M'$ computes $f$. But $S$ can never know this, because then it would know that there is no contradiction from $S$, contradicting Gödel's theorem.

The point of the above observation is that no formal system can make inferences about correctness of algorithms from runtime constraints alone. If we assume that S knows that some machine M decides SAT in polynomial time, there will always be another M for which S will not know this.


This seems troubling, since it can in principle be conceived that, while P=NP, the logical complexity of proving any polynomial-time satisfiability algorithm $M$ to be correct can be larger than the consistency strength of any formal theory $T$ that may be considered in say, the next 100 years:

$(\forall x\ M(x){\in}\{0,1\}\ \&\ (M(x)=1 \iff x \in SAT)) \Rightarrow \mathsf{Con}(T)$

Can such a situation be ruled out, for some natural extension $T$ of ZFC? This would mean exactly that $T$ answers the question posed in the title.

  • $\begingroup$ Trivially, "P=NP implies T proves P=NP" holds if we parse it as P=NP implies (T proves P=NP). So I guess that you mean (P=NP implies T) proves P=NP. $\endgroup$ Dec 2 '16 at 14:56
  • $\begingroup$ I mean the former. If you have the answer, please share it. Even (and especially!) if it seems trivial. ;) $\endgroup$ Dec 2 '16 at 21:05
  • $\begingroup$ By elementary logic, if we premise a proposition $A$ (e.g. P=NP), then any theory whatsoever, including (say) ZFC + $\lnot A$, can prove $A$: Just write down any true statements of the theory you like (or none, if you prefer); then introduce $A$; and $A$ follows immediately. $\endgroup$ Dec 2 '16 at 22:53
  • 3
    $\begingroup$ Counterexample.T=PA. A=Con(PA). $\endgroup$ Dec 2 '16 at 23:47
  • $\begingroup$ Of course, PA does not prove Con(PA) if we can include no assumption beyond PA in any proof. But this stricture entails that the "$A$ implies" (i.e. Con(PA) implies) part of the statement is without any force and is effectively redundant. So, returning to the original question, what exactly do you mean by "P=NP implies"? $\endgroup$ Dec 3 '16 at 10:54

Does this work? Use the Bellantoni-Cook theorem to enumerate all the polynomial time Turing machines. If P=NP you will eventually run into a machine that you can recognize as running Levin's universal search algorithm on some NP-complete problem. That proves Levin's algorithm on that problem runs in P-time and therefore P=NP. The paper also cites a result of Leviant that

a function is polytime if and only if it can be proved convergent in the logical system $L_2(QF^+)$ using the function’s recursion equations and a 'surjective' principle. Here $L_2(QF^+)$ is second order logic with comprehension (i.e., definability of sets) for positive quantifier-free fomulas.

which might be of use to you.

(Hmm, I don't know if the BC theorem actually lets you enumerate the P-time Turing machines, or just syntactic descriptions of the languages, that might not get you all the recognizers. I better read the paper more carefully).

  • 1
    $\begingroup$ No, this doesn't work, for exactly the reason you state. It's not possible to enumerate polynomial-time Turing machines in the way you are suggesting - telling if a fixed Turing machine halts in polynomial time - as this would enable you to solve the halting problem by considering Turing machines that ignore their input and hence either halt in constant time or run forever. $\endgroup$
    – Will Sawin
    Jan 2 '17 at 8:15

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.