# Why doesn't Godel's Second Incompleteness Theorem rule out a formalizable proof of P!=NP?

I'm sure there must be something wrong with the following reasoning because otherwise a lot of P vs. NP research would be curtailed but I cannot determine my error:

For any fixed integer $k>0$ define $$B_k := \{ \langle \varphi \rangle | \; \varphi \; \text{is a wff of ZF and has a proof of length} \; \leq k{|\varphi|}^k \; \}$$

Now for all $k$, the language $B_k$ is in NP since a valid proof for $\varphi$ of length $\leq k{|\varphi|}^k$ can be a NP-witness verified by an automated proof-checker in polynomial time. Furthermore, for sufficiently large enough $k$, $B_k$ is NP-complete since SAT reduces to it: that is, for an instance $\phi$ of SAT make a corresponding wff of ZF $\varphi$ using existential quantifiers. Then a satisfying truth assignment of $\phi$ can be made into a formal proof of $\varphi$ of length polynomial in $|\varphi|$ since a truth assignment of $\phi$ is linear in $|\phi|$.

Now, if ZF is inconsistent, this means that there is a formal statement $\sigma$ such that both $\sigma$ and $\neg \sigma$ have proofs in ZF. As is well known, any other statement $\tau$ can then be derived from the contradictory conjunction $\langle \sigma \wedge \neg \sigma \rangle$ (that is by following the path: $$\langle \sigma \wedge \neg \sigma \rangle \implies \text{both} \; \sigma \; \text{and} \; \neg \sigma \; \text{are true} \implies \langle \neg \tau \rightarrow \sigma \rangle \; \text{is true (since regardless of} \; \tau \; \text{the implication is valid since} \; \sigma \; \text{is true)} \implies \langle \neg \sigma \rightarrow \tau \rangle \; \text{(by contraposition and double negation)} \implies \tau \; \text{ is true (by modus ponens with} \; \neg \sigma \, )$$

). Thus if ZF is inconsistent, then every statement $\varphi$ has a proof polynomial (it seems to me even just linear) in $|\varphi|$.

Let $B:=B_k$ for a sufficiently large $k$ a referred to above to allow for $B$ to be NP-complete. Then if ZF is inconsistent, there are only finitely many $\varphi$ such that $\langle \varphi \rangle \notin B$ because the high-degree polynomial proof length allowance of $B$ is enough to cover the guaranteed short proofs of wffs of sufficient length. This implies that $B$ is decidable in polynomial time which by its NP-completeness implies that P=NP. If we rephrase this chain of reasoning in terms of contrapositives, if P!=NP then ZF is not inconsistent (that is it is consistent).

Therefore If we have a formal proof of P!=NP then we have a formal proof of the consistency of ZF. But by Godel's Second Incompleteness theorem, this implies that ZF is inconsistent which in turn get P=NP as outlined above (as well as the theoremhood of any negated theorem).

This is not exactly a proof that P vs. NP is independent of ZF. It could be that ZF is consistent and that P=NP or that P!=NP can be proven through techniques not formalizable within ZF. However, it does present another formidable barrier to resolving P vs. NP.

There seems to be a flaw as alluded to by Arno in his answer. While the reduction $SAT \leq B$ seems innocuous enough (and is indeed a textbook exercise as pointed out by Ariel in his comment) it implicitly assumes the consistency of ZF. Otherwise, if ZF is inconsistent, since every statement of ZF would then have a proof, unsatisfiable SAT-instances would not necessarily be mapped to wffs $\varphi$ which do not have a relatively short proof.

Thus, if we assume that ZF is consistent and $ZF \vdash P \neq NP$ then although we can conclude metamathematically that $B \notin P$ (because being NP-complete, $B$ could not be in $P$ since we are assuming $P \neq NP$) we would not have a formal deduction of $ZF \vdash B \notin P$ (since this depends on $B$ being an established NP-complete set, so if we want to use the reduction above, we must assume that ZF is consistent, which cannot be formally asserted by Godel's Second Incompleteness Theorem). Thus this argument cannot suggest any necessary implications of $ZF \vdash P \neq NP$.

• Good job! this seems to be the issue. Commented Jun 17, 2018 at 21:13

The problem is in your assertion that for sufficiently big $k$, the language $B_k$ is NP-complete. In your proposed reduction, you only argue that any satisfiable SAT-instance is to a ZF-formula with "short" proof. However, you also need to argue that whenever the resulting ZF-formula has a short proof, then the original SAT-instance is satisfiable. This of course just boils down to saying that if ZF proves that the SAT-instance is satisfiable, then it really is - but here we are using soundness of ZF.

• You're correct in that I am implicitly assuming the soundness of ZF and the correctness of a proof checker, but how does this affect the proof that $B_k$ is NP-complete? These are just necessary assumptions for the language $B_k$ to be of any interest. Under my reduction, only a satisfyable SAT-instance wiil have a proof of any length because an unsatisfyable one corresponds to a ZF statement which is false.
– Ari
Commented Jun 17, 2018 at 15:41
• @Ari Unsatisfiable SAT-instances correspond to ZF statements that are false in your meta-theory. So for the reduction to work, you need that false ZF statements do not have a ZF-proof.
– Arno
Commented Jun 17, 2018 at 16:44
• The equivalence is clear, if the formula has a proof then the SAT instance is satisfiable (ZF is sound, I don't see why this should be an obstacle here). See this question for a proof of its NP completeness. Commented Jun 17, 2018 at 17:41
• @Ariel The answer in that question is imprecise on what the assumptions are. It necessarily needs to assume that ZF is sound. Just the reminder: "Sound" means that if a statement has a proof, then it is actually true. If ZF is inconsistent, then it proves everything, and hence cannot be sound. In particular, we see that "ZF is sound" is not a theorem of ZF. If our meta-theory proves "ZF is sound", then it also proves "ZF is consistent", and there is no issue. If it does not prove it, then we don't have the NP-completeness proof, and there is no issue either.
– Arno
Commented Jun 20, 2018 at 11:04
• The correctness of the reduction indeed relies on the consistency of ZF, however it has nothing to do with soundness. Recall that soundness is defined relative to some semantics, and ZF is sound in the sense that proveable statements are true in all models, if ZF is inconsistent that it is vacuously sound as it has no models. Commented Jun 20, 2018 at 14:03