Does ETH imply P vs NP is decidable?

Question

I have been reading Scott Aaronson's summary paper on P vs NP. In this paper, there was a section about the likelihood of the problem being undecidable (page 28). He mentions a paper that I could no get my hands on by S. Ben-David and S. Halevi entitled "Independence of P versus NP." It is supposedly proven in this paper that if P!=NP is proven to be unprovable in some weaker theories ($\mathrm{PA} + \Pi_1$), then we would have almost P=NP (he says that NP problems must at least have an algorithm that runs in $n^{\log \log \log \log n}$).

My question is, does this imply that if ETH or SETH are true, then P vs NP is decidable for sure?

Answer 1

The first point to be aware of about our PvsNP paper is that the direction "If SAT can't be solved in 'almost polynomial' time then $\mathrm{P \neq NP}$ is provable" applies only to provability in a very strong system ($\mathrm{PA}+Π_1$). This is an undecidable proof system so it is not one wishes to design proofs in (there is no algorithm that can tell a valid proof from an invalid one). Indeed, if ETH is true then our result implies that there will be a proof of $\mathrm{P \neq NP}$ in that strong proof system. The reason the result requires the strong proof system is that one needs a system that can prove the equivalence of any two Turing machines that compute the same function (otherwise a simple diagonalization trick can generate an undecidable statement equivalent to $\mathrm{P \neq NP}$). The collection of all such statements is equivalent to the $\Pi_1$ theory of natural numbers.