How much of P versus NP's difficulty stems from having to rule out the existence of Turing machines that "accidentally" solve, say, 3-SAT efficiently?

Question

It seems like there is a sense in which a Turing machine that demonstrates P=NP could be said to "accidentally" exist. I'm wondering the extent to which the possibility of such machines is the main reason P not equal to NP is so hard to prove. A priori can such machines exist, or are there heuristic or known reasons they can't?

By a Turing machine that accidentally solves P=NP, I mean a Turing machine that solves an NP-complete problem, say 3-SAT, in polynomial time. But its description might bear no logical or discernible relation to 3-SAT. To make this precise, maybe the right definition of an accidental solution is that it's not provable that the machine is a solution, even though one could observe empirically that it is (because it would be).

This would be analogous to observing empirically that a solution to 3-SAT happens to be encoded in the digits of pi starting at some digit (under some natural enumeration of all 3-SAT inputs and with pi written in base 2), or in the digits of some other irrational number whose digits can be computed in polynomial time.

If the existence of accidental solutions is consistent with ZFC, say, then P not equal to NP couldn't be proven. If this is in fact one of the things that makes P versus NP difficult, does it make sense to consider a variant of the P versus NP problem that restricts P not just to Turing machines that accept certain languages in polynomial time, but also to ones for which this is provable? Does this make the problem any easier?

Lines of thinking like this might be common knowledge to complexity theorists, but I haven't seen it expressed in writing.

This question is a little reminiscent of this MO question about the Goldbach conjecture.

Answer 1

Yes, it makes sense to consider such variants of the problem. Apart from the complexity-theoretic motivation, they arise quite naturally in the study of weak fragments of arithmetic (bounded arithmetic): for example, it is known that Buss’ theory $S_2$ (or equivalently, $I\Delta_0+\Omega_1$) is finitely axiomatizable if and only if $S_2$ proves that the polynomial hierarchy collapses (in an explicit way, i.e., there is a $\Sigma^P_n$-algorithm $M$ such that $S_2$ proves that $M$ solves a $\Sigma^P_{n+1}$-complete problem).

Unfortunately, the answer to the second part of your question is no, it does not seem to make the problem any easier, even if we ask for provability in an extremely weak theory (such as PV, and similar fragments of bounded arithmetic).

If you want to learn more about these issues, you can consult Bounded Arithmetic, Propositional Logic, and Complexity Theory by Krajíček, or Logical foundations of proof complexity by Cook and Nguyen.