Computer Science Stack Exchange is a question and answer site for students, researchers and practitioners of computer science. It only takes a minute to sign up.
Sign up to join this community
Suppose P vs. NP is independent of ZFC. Then there cannot be an efficient SAT solver, otherwise it would constitute a proof for P = NP. Therefore P $\ne$ NP.
What we see here is that independence implies unequality. So why is independence a big deal? It is just one way to show P $\ne$ NP. See Scott Aaronson's paper Is P Versus NP Formally Independent?.
As Yuval Filmus comments, your argument is flawed: just because a given algorithm is a SAT-solver doesn't mean that we can prove that it is a SAT-solver.
Technically, the same issue applies to the time bound - we can cook up a Turing machine which always runs in polynomial time iff ZFC is consistent - but this is easily avoidable: given a Turing machine $T$ and a polynomial $p$, we can form a machine $T[p]$ which behaves like $T$ except with the time bound $p$ artificially imposed: on input of length $n$, $T[p]$ simulates $T$ for $p(n)$-many steps and diverges if it hasn't halted within that time. We can decide whether a machine $S$ has the form $T[p]$ for some $T, p$, so if $T$ happens to be a SAT solver which operates in polynomial time $p$, then $T[p]$ is a polytime SAT solver which we can prove operates in polynomial time. The culprit is "is a SAT solver," for which there doesn't appear to be a similar trick.
The issue here is logical complexity. "Undecidability implies truth" holds for statements with verifiable counterexamples; these are the $\Pi^0_1$ statements.$^*$ The Goldbach conjecture is a good example: in order to be false, there would need to be a counterexample, and being a counterexample to Goldbach is an easily checkable property since it only relies on "bounded quantifiers." By contrast, the Twin Primes Conjecture is a priori merely $\Pi^0_2$, and so at the moment we don't have any reason to believe that its undecidability from (say) PA would imply its truth.
Even in the $\Pi^0_1$ context, however, undecidability is more than just a method for proving a statement. It establishes that the principle is true "for deep reasons" in some sense. If a statement $P$ about the natural numbers$^{**}$ is true but not PA-provable, this means that the reason $P$ is true is more complicated than just our simple intuitions about induction, since PA already incorporates the full arithmetical induction scheme. Now whether one consider this a worthwhile observation depends on one's particular interests, but it (and even weaker independence phenomena) is certainly noteworthy to me.
$^*$This is in fact an exact characterization, in the following sense. If $S$ is a reasonable theory of arithmetic, and the independence of $P$ from $S$ implies the truth of $P$, then $P$ is equivalent to the statement "$P$ is not provable from $S$" (part of "reasonable" here is soundness). But this latter statement is $\Pi^0_1$. Now this is actually silly - every sentence is either equivalent to $0=0$ if true or $0=1$ if false - but it can be "de-sillified" by phrasing it as: if $T,S$ are reasonable theories and $T$ proves that $S$ is consistent and that if $P$ is $S$-undecidable then $P$ is true, then $T$ proves that $P$ is equivalent to the $\Pi^0_1$ sentence "$P$ is not $S$-disprovable."
$^{**}$Or a statement interpretable as a statement about the natural numbers; e.g. "P=NP" is a statement about Turing machines, but by the usual techniques is "faithfully translateable" into the language of arithmetic.
