<p>I would like to elaborate on Kaveh's answer because I see people wondering about the constructive status of $P = NP$.</p>

<p>Levin's algorithm performs a dove-tailing parallel execution of all Turing machines on the given SAT instance. If and when any machine terminates, it is verified whether its output is a solution to the SAT instance. If so, Levin's algorithm terminates, otherwise it keeps going.</p>

<p>The algorithm solves SAT because there is a Turing macine that solves SAT, and so eventually Levin's algorithm emulates enough of it to find a solution. Moreover, with careful programming the dove-tailing technique incures at most a polynomial slowdown of any particular simulated machine, so if there is a machine solving SAT in polynomial time, then Levin's algorithm does it in polynomial time as well.</p>

<p>Now let us consider the logical complexity of the statement *"Levin's algorithm runs in polynomial time". It is a specific algorithm whose Gödel code is some number $\ell$. The statement that it runs in polytime can be expressed in first-order arithmetic using Kleene's predicate $T$:
$$\exists C, k. \forall m . \exists n &lt; 2^{C \cdot m^k}. T(\ell, k, n).$$
This can be read as: "There are $C$ and $k$ such that for every (Gödel code of a) SAT instance $m$ there is (a Gödel code of) an execution trace $n$ of $\ell$ running on input $k$, and the length of execution trace does not exceed $C \cdot m^k$."</p>

<p>The predicate $T$ is primitive recursive, and so is the inner formula as its quantifier is bounded by a primitive recursive function. If I am not making a mistake here (please correct me if I am, or provide a reference as I cannot be the first person noticing this), this means that we can express $P = NP$ as a $\Sigma^0_2$-formula. Thus, by negating the formula we can express $P \neq NP$ as a $\Pi^0_2$-formula. By Friedman's conservativity result we therefore have</p>

<blockquote>
  <p>If Peano arithmetic proves $P \neq NP$ then Heyting arithmetic proves $P \neq NP$.</p>
</blockquote>

<p>In other words, this shows that in the context of first-order arithmetic $P \neq NP$ has a constructive proof if it has a classical one.</p>

<p>Am I making a mistake somewhere?</p>

CC BY-SA 3.0
2013-11-26T23:44:37.400Z
I have seen this argument about PA and HA but don't recall where. I personally feel a bit uncomfortable to interpret this result as "if P=NP is provable then it is constructively provable" since it interprets provable as provable in PA.
Kaveh
CC BY-SA 3.0
2013-11-27T08:13:52.710Z
I agree that we should not confuse provable with provable in $PA$, which is why I always wrote "in the context of arithmetic". On the other hand, it would be rather stunning if $P=NP$ were independent of $PA$.
Andrej Bauer
CC BY-SA 3.0
2013-11-27T19:57:38.187Z
@AndrejBauer: Looks right to me. I wasn't aware of Friedman's conservativity result, and this is quite an interesting consequence (which I had also not heard of)! Might be worth a short note on ECCC (or maybe even a ToC Note, or IPL?)...
Joshua Grochow
CC BY-SA 3.0
2013-11-28T04:36:35.417Z
Google found [this post on FOM](http://www.cs.nyu.edu/pipermail/fom/2010-August/015000.html) by Harvey but I am sure there are earlier references. ps: I looked around a bit but I couldn't find a good reference to cite. It can be a good idea to write and post it somewhere more accessible than a FOM thread.
Kaveh
CC BY-SA 3.0
2013-11-26T23:01:55.087Z
2013-11-26T23:01:55.087Z
Andrej Bauer
<p>It is not entirely clear what you mean by a nonconstructive proof of P=NP.
I am guessing that you are asking if it is possible to prove that there is a polynomial time algorithm for SAT without providing one. That cannot be the case because we can prove that Levin's universal search algorithm for SAT has optimal running time, if P=NP is true (even if it is not provable <em>at all</em>) his algorithm will be polynomial time and will solve SAT.</p>

<p>On the other hand, the proving that Levin's algorithm (or any algorithm for SAT) runs in polynomial time may require nonconstructive concepts and axioms.</p>

CC BY-SA 3.0
2013-11-26T19:49:23.027Z
2013-11-26T19:55:59.017Z
2013-11-26T19:55:59.017Z
Kaveh
<p>Why can the statement $SAT \in DTIME(n^3)$ not be proven through a non-constructive proof? Intuitively a proof would be a turing machine, which solves this problem in $DTIME(n^3)$, but there are non-constructive proofs like the following:
<a href="https://cs.stackexchange.com/questions/367/how-can-it-be-decidable-whether-pi-has-some-sequence-of-digits">https://cs.stackexchange.com/questions/367/how-can-it-be-decidable-whether-pi-has-some-sequence-of-digits</a></p>

CC BY-SA 3.0
2013-11-26T13:35:52.303Z
Because it's very probably not true?
David Richerby
CC BY-SA 3.0
2013-11-26T15:27:34.807Z
To clarify: Assume there is a proof for $SAT \in DTIME(n^3)$. Can this proof be nonconstructive?
user20264
CC BY-SA 3.0
2013-11-26T15:59:46.483Z
See Levin's universal optimal search  algorithm.
Kaveh
CC BY-SA 3.0
2013-11-26T16:42:07.357Z
@user20264 Why specifically SAT and cubic time? You could equally ask something like, "Can there be a non-constructive proof of the four-colour theorem" or anything else.
David Richerby
CC BY-SA 3.0
2013-11-26T18:56:34.490Z
Why is this question downvoted?
usul
CC BY-SA 3.0
2013-11-27T13:28:39.637Z
It is always an option to come to my office and discuss any problem. (I admit that I was not available yesterday afternoon.)
Markus Bläser
<cc.complexity-theory><lo.logic><sat><proof-theory><constructive-mathematics>
SAT in some DTIME always via a constructive proof?
user20264
# SAT in some DTIME always via a constructive proof?

(Asked by: username_0 on 2013-11-26)

Why can the statement $SAT \in DTIME(n^3)$ not be proven through a non-constructive proof? Intuitively a proof would be a turing machine, which solves this problem in $DTIME(n^3)$, but there are non-constructive proofs like the following:
<https://cs.stackexchange.com/questions/367/how-can-it-be-decidable-whether-pi-has-some-sequence-of-digits>

**Tags:** cc.complexity-theory, lo.logic, sat, proof-theory, constructive-mathematics
> **Comments:**
> **username_1**: Because it's very probably not true?  
> **username_0**: To clarify: Assume there is a proof for $SAT \in DTIME(n^3)$. Can this proof be nonconstructive?  
> **username_2**: See Levin's universal optimal search  algorithm.  
> **username_1**: @user20264 Why specifically SAT and cubic time? You could equally ask something like, "Can there be a non-constructive proof of the four-colour theorem" or anything else.  
> **username_3**: Why is this question downvoted?  
> **username_4**: It is always an option to come to my office and discuss any problem. (I admit that I was not available yesterday afternoon.)  

---

## 2 answers

### Answer by username_5 on 2013-11-26. Score: 8

I would like to elaborate on Kaveh's answer because I see people wondering about the constructive status of $P = NP$.

Levin's algorithm performs a dove-tailing parallel execution of all Turing machines on the given SAT instance. If and when any machine terminates, it is verified whether its output is a solution to the SAT instance. If so, Levin's algorithm terminates, otherwise it keeps going.

The algorithm solves SAT because there is a Turing macine that solves SAT, and so eventually Levin's algorithm emulates enough of it to find a solution. Moreover, with careful programming the dove-tailing technique incures at most a polynomial slowdown of any particular simulated machine, so if there is a machine solving SAT in polynomial time, then Levin's algorithm does it in polynomial time as well.

Now let us consider the logical complexity of the statement \*"Levin's algorithm runs in polynomial time". It is a specific algorithm whose Gödel code is some number $\ell$. The statement that it runs in polytime can be expressed in first-order arithmetic using Kleene's predicate $T$:
$$\exists C, k. \forall m . \exists n < 2^{C \cdot m^k}. T(\ell, k, n).$$
This can be read as: "There are $C$ and $k$ such that for every (Gödel code of a) SAT instance $m$ there is (a Gödel code of) an execution trace $n$ of $\ell$ running on input $k$, and the length of execution trace does not exceed $C \cdot m^k$."

The predicate $T$ is primitive recursive, and so is the inner formula as its quantifier is bounded by a primitive recursive function. If I am not making a mistake here (please correct me if I am, or provide a reference as I cannot be the first person noticing this), this means that we can express $P = NP$ as a $\Sigma^0\_2$-formula. Thus, by negating the formula we can express $P \neq NP$ as a $\Pi^0\_2$-formula. By Friedman's conservativity result we therefore have

> If Peano arithmetic proves $P \neq NP$ then Heyting arithmetic proves $P \neq NP$.

In other words, this shows that in the context of first-order arithmetic $P \neq NP$ has a constructive proof if it has a classical one.

Am I making a mistake somewhere?

> **Comments:**
> **username_2**: I have seen this argument about PA and HA but don't recall where. I personally feel a bit uncomfortable to interpret this result as "if P=NP is provable then it is constructively provable" since it interprets provable as provable in PA.  
> **username_5**: I agree that we should not confuse provable with provable in $PA$, which is why I always wrote "in the context of arithmetic". On the other hand, it would be rather stunning if $P=NP$ were independent of $PA$.  
> **username_6**: @AndrejBauer: Looks right to me. I wasn't aware of Friedman's conservativity result, and this is quite an interesting consequence (which I had also not heard of)! Might be worth a short note on ECCC (or maybe even a ToC Note, or IPL?)...  
> **username_2**: Google found [this post on FOM](http://www.cs.nyu.edu/pipermail/fom/2010-August/015000.html) by Harvey but I am sure there are earlier references. ps: I looked around a bit but I couldn't find a good reference to cite. It can be a good idea to write and post it somewhere more accessible than a FOM thread.  

---

### Answer by username_2 on 2013-11-26. Score: 6

It is not entirely clear what you mean by a nonconstructive proof of P=NP.
I am guessing that you are asking if it is possible to prove that there is a polynomial time algorithm for SAT without providing one. That cannot be the case because we can prove that Levin's universal search algorithm for SAT has optimal running time, if P=NP is true (even if it is not provable *at all*) his algorithm will be polynomial time and will solve SAT.

On the other hand, the proving that Levin's algorithm (or any algorithm for SAT) runs in polynomial time may require nonconstructive concepts and axioms.


---

