Consider the following situation. In a parallel world (let's hope not in this one), in 2020 a clever guy proved $P\neq NP$ in a theory $T_1=\{ZFC+some\, reasonable\, new\, axioms\}$. Then, in 2021 a clever gal proved $P=NP$ in $T_2=\{ZFC+other\, reasonable\, axioms\}$. We assume that the both theories are consistent and the both proofs are correct. Still, the situation is theoretically possible, because $P\neq NP$ is a $\Pi_2$ statement.

*Question: How to clear the mess?*

Actually, this question is not exactly about $P\neq NP$. Rather,
it is about $\Pi_2$ statements in general.
If such a statement is *false* then it contradicts some true $\Pi_1$ statement;
all we have to do is to find and prove the latter. (Which may be not so easy, but this is
a different problem). The question is, if the statement is *true*, how do we know this,
even if we have a correct proof in a consistent theory?
In my opinion, this question is not purely academic: after all, a lot of

mathematical problems belong to this class, and we cannot possibly
know what new axioms (or whole theories) will be proposed in the future.

knowit. All we can do is to somehow develop consensus which axiom system is more reasonable, but if this turns out not to lead anywhere, there is not really any problem with pursuing research in both. Though in this case, as you say, a true $\Sigma^0_2$ statement is implied by a true $\Pi^0_1$ statement, hence one could ask the gal to provide a proof of a $\Pi^0_1$ statement implying $P=NP$. If she succeeds, her statement is true (due to consistency); if she does not, it would cast serious doubts on her axiom system, so it would make sense to go with the guy. $\endgroup$ – Emil Jeřábek supports Monica Oct 30 '12 at 12:11