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

Question

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.

Answer 1

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

Answer 2

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.