Are there any natural theories T for which P=NP implies T proves P=NP?

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.

Motivation.

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.

• 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. Dec 2 '16 at 14:56
• I mean the former. If you have the answer, please share it. Even (and especially!) if it seems trivial. ;) Dec 2 '16 at 21:05
• 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. Dec 2 '16 at 22:53
• Counterexample.T=PA. A=Con(PA). Dec 2 '16 at 23:47
• 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"? Dec 3 '16 at 10:54

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.