Unprovable behavior of a turing machine

Question

The wikipedia-article for the P-NP problem [1] says there are three possible answers to the P-NP-problem:

• $P=NP$
• $P\neq NP$
• $P=NP$ is independent of ZFC

The third possible solution seems to be very interesting. Assuming it is true, there could still exist a turing machine which solve e.g. $SAT$ in polynomial time, but it cannot be proved. Assume now someone has found this turing machine.

It should never be possible to prove that this turing machine solves $SAT$ in polynomial time (because we "know" $P=NP$ is independent of ZFC), but the machine does it.

This situation sound very strange to me: Someone has a turing machine, but it is not possible to prove that it solves a specific problem ($SAT$). More specifc: If someone has proven that $P=NP$ is independent of ZFC then there exists a proof which says that it is not possible to prove for any turing machine that is solves $P=NP$ in polynomial time. Even if someone has found this turing machine.

Did i understand this right? Or did i understand something wrong? Because it sounds very strange to me that someone has an algorithm and it can be proved that it is impossible to prove what exactly this algorithm does.

Best regards

Kevin

[1] https://en.wikipedia.org/wiki/P_versus_NP_problem#Results_about_difficulty_of_proof

Answer 1

Yes, your understanding is basically correct - this is (so far as we know) a possible outcome. The issue is that there may be models of ZFC in which there are "nonstandard" natural numbers. These nonstandard numbers correspond to nonstandard instances of SAT, which the algorithm $\alpha$ might fail to solve, even though it solves all actual instances of SAT.

It turns out that nonstandard running time isn't a problem - if $\alpha$ runs in polynomial time $p$, consider the algorithm $\alpha'$ which performs $\alpha$ for $p$-many steps, and then - if it hasn't halted yet - halts and outputs 1 (say). Then $\alpha'$ solves all actual instances of SAT, and even nonstandardly $\alpha'$ runs in polynomial time. So the issue really is about nonstandard instances of SAT.

This is analogous to Godel's incompleteness theorem: even though there is no actual natural number coding a proof of $0=1$ from the ZFC axioms (we hope :P), there will be a model of ZFC containing some nonstandard natural number $n$ which (the model thinks) codes a proof of $0=1$ from $ZFC$ - that is, a "nonstandard proof."

Answer 2

It may be helpful to distinguish different possible ways $P = NP$ could be true but not provably true. In order for $P = NP$, there must be a Turing machine $T$ that solves SAT in polynomial time. But:

1. It might be impossible to prove that it always halts.
2. It might be possible to prove it always halts, but impossible to prove that it always produces a correct result.
3. It might be possible to prove it always halts, but impossible to prove that it halts in polynomial time.

This shouldn't be so strange. Many unsolved mathematical problems can be formulated in terms of questions about a Turing machine. For example, the Collatz conjecture is true if and only if a certain Turing machine always halts.