# Does ETH imply P vs NP is decidable?

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?

• This doesn't sound like a research-level question and would be more suitable for CS.SE. Anyway, ETH says “SAT requires exponential time”, so ETH ⇒ P ≠ NP by definition. Commented Aug 30 at 15:41
• @JeanAbouSamra: But it might be the case that SAT requires exponential time, but you can't prove it, so it's undecidable. The result is not trivial. Commented Aug 30 at 16:00
• "ETH is true" just means ETH. Commented Aug 31 at 6:14
• cs.technion.ac.il/~shai/ph.ps.gz Commented Aug 31 at 14:32
• FYI here is the Ben-David and Halevi paper: web.archive.org/web/20221224145635/http://www.cs.technion.ac.il/… Commented Aug 31 at 15:15

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.