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?.

  • 4
    $\begingroup$ There could be an efficient SAT solver which cannot be proved to work (or to run in polynomial time) in ZFC. $\endgroup$ – Yuval Filmus Jun 20 '18 at 13:21
  • $\begingroup$ @YuvalFilmus OK, my newly learnt technique doesn't work here, because checking whether an algorithm works takes infinite amount of time, instead of finite. $\endgroup$ – Zirui Wang Jun 20 '18 at 14:36
  • $\begingroup$ @YuvalFilmus Why can't it be that there is a proof of correctness for every polynomial-time SAT solver? It may be undecidable for machines, but humans may come up with such proofs. $\endgroup$ – Zirui Wang Jul 20 '18 at 18:39
  • $\begingroup$ I don't believe there are polynomial SAT solvers. $\endgroup$ – Yuval Filmus Jul 20 '18 at 18:41

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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.