# How to prove a $\Pi_2$ statement properly?

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.

• We can’t know it. 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. – Emil Jeřábek supports Monica Oct 30 '12 at 12:11
• However, I also have doubts whether this scenario is realistic. How would we know that both axiom systems are consistent? – Emil Jeřábek supports Monica Oct 30 '12 at 12:14
• (Necropost) One interesting thing is that it cannot be the case that both proofs are completely constructive. The gal would have to construct a particular algorithm for an NP-complete problem, and give a specific polynomial bound on its running time. The guy's proof would then have to take this algorithm and bound, and provide an input that would make it run longer than the bound. (This requirement on the guy's proof is stronger than a constructive disproof of P = NP). The two theories then disagree about how long a program runs on a particular input, which would make one of them inconsistent. – qbt937 Aug 6 '17 at 0:27