<p>The first point to be aware of about our PvsNP paper is that the direction
&quot;If SAT can't be solved in 'almost polynomial' time then <span class="math-container">$\mathrm{P \neq NP}$</span> is provable&quot; applies only to provability in a very strong system (<span class="math-container">$\mathrm{PA}+Π_1$</span>). 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 <span class="math-container">$\mathrm{P \neq NP}$</span> 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 <span class="math-container">$\mathrm{P \neq NP}$</span>). The collection of all such statements is equivalent to the <span class="math-container">$\Pi_1$</span> theory of natural numbers.</p>

CC BY-SA 4.0
2024-09-03T14:04:06.957Z
Thanks for the helpfull answer and even more helpfull paper !
maikio
CC BY-SA 4.0
2024-09-02T13:26:08.800Z
2024-09-02T16:29:41.773Z
2024-09-02T16:29:41.773Z
Shai Ben-David
<p>I have been reading Scott Aaronson's summary paper on <a href="https://www.scottaaronson.com/papers/pnp.pdf" rel="nofollow noreferrer">P vs NP</a>. 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 &quot;Independence of P versus NP.&quot; It is supposedly proven in this paper that if P!=NP is proven to be unprovable in some weaker theories (<span class="math-container">$\mathrm{PA} + \Pi_1$</span>), then we would have almost P=NP (he says that NP problems must at least have an algorithm that runs in <span class="math-container">$n^{\log \log \log \log n}$</span>).</p>
<p>My question is, does this imply that if ETH or SETH are true, then P vs NP is decidable for sure?</p>

CC BY-SA 4.0
2024-08-30T15:41:31.463Z
This doesn't sound like a [*research-level* question](https://cstheory.stackexchange.com/help/on-topic) and would be more suitable for [CS.SE](https://cs.stackexchange.com/). Anyway, ETH says “SAT requires exponential time”, so ETH ⇒ P ≠ NP by definition.
Jean Abou Samra
CC BY-SA 4.0
2024-08-30T16:00:10.470Z
@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.
Peter Shor 
CC BY-SA 4.0
2024-08-30T16:02:40.323Z
Oops, sorry for the stupid comment, I should get some rest.
Jean Abou Samra
CC BY-SA 4.0
2024-08-30T18:48:20.113Z
I don't understand this question. Let's say undeidable means "not provable from ZFC". If ZFC |- ETH, then (probably) ZFC |- P not NP. But if ZFC does not prove ETH, then what does "ETH is true" even mean?
Reijo Jaakkola
CC BY-SA 4.0
2024-08-30T22:48:27.053Z
@ReijoJaakkola By ‘ETH is true’ one probably refers to the statement being true in the standard model of the theory/in the metatheory. Truth is different from provability.
Noel Arteche
CC BY-SA 4.0
2024-08-31T06:14:53.553Z
"ETH is true" just means ETH.
Emil Jeřábek
CC BY-SA 4.0
2024-08-31T09:06:05.103Z
@NoelArteche But if the theory/metatheory is ZFC (or something stronger), then what is its standard model?
Reijo Jaakkola
CC BY-SA 4.0
2024-08-31T14:32:03.093Z
http://www.cs.technion.ac.il/~shai/ph.ps.gz
Kaveh
CC BY-SA 4.0
2024-08-31T15:15:09.333Z
FYI here is the Ben-David and Halevi paper: https://web.archive.org/web/20221224145635/http://www.cs.technion.ac.il/users/wwwb/cgi-bin/tr-get.cgi/1991/CS/CS0699.revised.pdf
Joshua Grochow
CC BY-SA 4.0
2024-08-31T16:48:13.907Z
The edited question makes much more sense.
Reijo Jaakkola
CC BY-SA 4.0
2024-09-01T13:51:43.763Z
@JoshuaGrochow : Thanks for the link. I will see if I can find my answer in the paper. Although just by looking at the beginning, its not clear if the running time they mentioned applies to worst case.
maikio
<lo.logic><complexity><p-vs-np><proof-theory>
Does ETH imply P vs NP is decidable?
maikio
# Does ETH imply P vs NP is decidable?

(Asked by: username_0 on 2024-08-30)

I have been reading Scott Aaronson's summary paper on [P vs NP](https://www.scottaaronson.com/papers/pnp.pdf). 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?

**Tags:** lo.logic, complexity, p-vs-np, proof-theory

> **Comments:**
> **username_1**: This doesn't sound like a [*research-level* question](https://cstheory.stackexchange.com/help/on-topic) and would be more suitable for [CS.SE](https://cs.stackexchange.com/). Anyway, ETH says “SAT requires exponential time”, so ETH ⇒ P ≠ NP by definition.  
> **username_2**: @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.  
> **username_1**: Oops, sorry for the stupid comment, I should get some rest.  
> **username_3**: I don't understand this question. Let's say undeidable means "not provable from ZFC". If ZFC |- ETH, then (probably) ZFC |- P not NP. But if ZFC does not prove ETH, then what does "ETH is true" even mean?  
> **username_4**: @ReijoJaakkola By ‘ETH is true’ one probably refers to the statement being true in the standard model of the theory/in the metatheory. Truth is different from provability.  
> **username_5**: "ETH is true" just means ETH.  
> **username_3**: @NoelArteche But if the theory/metatheory is ZFC (or something stronger), then what is its standard model?  
> **username_6**: http://www.cs.technion.ac.il/~shai/ph.ps.gz  
> **username_7**: FYI here is the Ben-David and Halevi paper: https://web.archive.org/web/20221224145635/http://www.cs.technion.ac.il/users/wwwb/cgi-bin/tr-get.cgi/1991/CS/CS0699.revised.pdf  
> **username_3**: The edited question makes much more sense.  
> **username_0**: @JoshuaGrochow : Thanks for the link. I will see if I can find my answer in the paper. Although just by looking at the beginning, its not clear if the running time they mentioned applies to worst case.  

---

## 1 answers

### Answer by username_8 on 2024-09-02. Score: 10 | Accepted answer

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.

> **Comments:**
> **username_0**: Thanks for the helpfull answer and even more helpfull paper !  

---

