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

Question

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.

Answer 1

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).