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:

- Show that if P=NP, then P=NP is provable is some fixed system $S$, such as ZFC or ZFC+large cardinals;
- Improve the previous result for weaker and weaker $S$ $-$ for example, go from ZFC down to PA2, PA, $I\Sigma_1$, etc.;
- 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.