SAT in some DTIME always via a constructive proof?
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 &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$."

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?