# A paradox involving complexity class separations and arithmetical soundness

Here is a paradox I came up with that I've only partly unraveled. The question is about how to mathematically model this situation in a way that satisfactorily explains both points of view. In the form of a story:

It's the year $2050$ and no significant developments have been made in theoretical computer science for three decades, no complexity class separations or other sought-after results. Although computers are a thousand times faster than thirty years ago, progress in the theoretical field has halted.

A message arrives from outer space which will soon rekindle a sudden worldwide interest.

Some experimentation reveals that the message can be interpreted as a description of a multi-tape Turing machine, and soon it is discovered that it seems to correctly solve $\text{3SAT}$, encoded in a straightforward way, and that it seems to do so very quickly, by postmodern standards, meaning that its runtime is empirically well-described by a polynomial-time function of small degree and a tractable multiplicative constant.

Baffled but overjoyed, the scientists proceed with the obvious course of business: claim the Millenium Prize by proving that the program works as it appears to. However, it is completely inscrutable. (In fact, a translation of it wins the Obfuscated C Code Contest the same year.) But one bright scientist comes up with a plan: we'll assume it works, and use it to find a proof of $\text{P} = \text{NP}$ by encoding the search for such a proof as a series of $\text{3SAT}$ problems, increasing in size along with the proof-length bound, but not too quickly. Lo and behold, this works...

But first, in order to frame the paradox, I'll introduce an additional assumption, that in the year $2050$, our preferred theory of arithmetic is both consistent and $\Sigma_1$-sound. That is, if mathematicians in that year can prove that a particular program halts on all inputs, then it actually does.

... it works, but actually, a megabyte-long formal proof of $\text{P} \neq \text{NP}$ is produced instead, and the scientists, while happy to claim the Millenium Prize, are left baffled as to how they produced it with a program that it implies is slow or broken. And so are we as spectators of this hypothetical scenario, because $\text{P} \neq \text{NP}$ is actually true. That follows from the soundness condition we assumed. But enough of this world for now.

Across the galaxy is another planet, not so different from Earth in the year $2050$, that receives the same message. One important difference is that their arithmetical theory is not the same as ours, although it is also consistent and $\Sigma_1$-sound. Their scientists proceed to analyze the situation similarly, using a different reduction from their own arithmetical language to prepare the input for the proof-search. However, their program outputs a megabyte-long proof of $\text{P} = \text{NP}$ instead, which is possible because their theory happens to be $\Sigma_2$-unsound and $\text{P} = \text{NP}$ is a $\Sigma_2$-sentence. In fact, it may even tell them that the program from outer space is both correct and has polynomial runtime, implying $\text{P} = \text{NP}$, and this statement is also a $\Sigma_2$-sentence. It won't give them a specific polynomial degree for the runtime of the program while proving it correct, since their theory is $\Sigma_1$-sound and we already know $\text{P} \neq \text{NP}$ really. However, these people are satisfied with their belief that $\text{P} = \text{NP}$ and that the program from outer space solves $\text{3SAT}$ in polynomial time, because their $\Sigma_2$-unsound theory proves it.

Now the paradox is, who is right? Superficially, we are, since we proved $\text{P} \neq \text{NP}$ and that's what's really true. But how did the program work to help us find the proof if that is the case? If the program works, they are right. And the twist is to ask, regardless of who is right, how do we know which planet we are really living on? If someday we encounter an actual proof of $\text{P} = \text{NP}$ that's lacking a $\Sigma_1$ refinement (we don't have both a specific $\text{3SAT}$-solving program and effective polynomial time bound) can it be rational to deny the truth of the result and instead support a new theory claiming $\text{P} \neq \text{NP}$ and that the old theory is $\Sigma_2$-unsound?

How do we mathematically describe this situation?

I know one resolution is to say that the program from outer space is at least as long as the proofs that we and they use it to find. And if it's not vastly larger there is also the disturbing suggestion that the authors of the message have knowledge of the arithmetic theories in use on both worlds as well as the particular reductions that the scientists will choose, since the construction of such a mock $\text{3SAT}$ solver would seem to require it. In any case, armed with this explanation that the program essentially just encodes the proofs and behaves as advertised for enough other instances to fool us, we should side with Planet Earth and $\text{P} \neq \text{NP}$. But how to prove any relationship between the program size and the length of the proof that it supposedly finds?

Alternatively, the program correctly solves $\text{3SAT}$ in time that is not quite polynomial, for example quasipolynomial, and simply appears polynomial in the regime that we are able to operate. Or perhaps it actually is polynomial except for an infinite but small set of instances that for some reason never show up in practice, or at least not during our proof search. Everybody wins, because $\text{P} \neq \text{NP}$ but they might as well be equal — the theory of the other world is just barely unsound.

Another line of inquiry I've considered is the question of what may be defined to constitute evidence for or against a sentence with respect to its level in the arithmetical hierarchy. I suspect this issue has been well-studied, but unfortunately not by me. Any references are appreciated.

I formulated this problem today by considering variations on some of the possible counterexamples to the Extended Church-Turing Thesis described in my recent answer on the cstheory.SE site. I'm also curious to know if it's not original, maybe I'm remembering it from somewhere that I can't remember. For some background here is an informative post from Dick Lipton's blog discussing the arithmetical hierarchy and $\text{P} = \text{NP}$.

• If you cannot understand the program, how can you exclude that it actually runs in exponential time, but the exponential terms are dwarfed by the polynomial terms in the range of sizes you tried? Maybe the exponential term takes over only for problems that need planet-sized computers in 2050. Indeed, if you don't understand the code, how can you sure that it really correctly solves 3SAT for anything but the cases you tested? – celtschk Dec 6 '17 at 6:57
• Sounds like a non-standard exoplanet to me! :P – Asaf Karagila Dec 6 '17 at 11:07
• Your question contains far too many hypotheticals. – Rob Arthan Dec 6 '17 at 23:45
• Let's focus on P vs. NP specifically and the idea of evidence against soundness... With a different $\Sigma_2$ problem like twin primes we can set up the same "twist" where we don't know what world we're on. However, the "evidence" in that version is of a lower quality, since there is no reason to think that the truth or falsehood of twin primes would affect our ability to settle the question. – Dan Brumleve Dec 7 '17 at 18:13