# SAT in some DTIME always via a constructive proof?

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

• Because it's very probably not true? – David Richerby Nov 26 '13 at 13:35
• To clarify: Assume there is a proof for $SAT \in DTIME(n^3)$. Can this proof be nonconstructive? – user20264 Nov 26 '13 at 15:27
• See Levin's universal optimal search algorithm. – Kaveh Nov 26 '13 at 15:59
• @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 Nov 26 '13 at 16:42
• Why is this question downvoted? – usul Nov 26 '13 at 18:56

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?

• 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 Nov 26 '13 at 23:44
• 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 Nov 27 '13 at 8:13
• @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 Nov 27 '13 at 19:57
• Google found this post on FOM 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 Nov 28 '13 at 4:36

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.