Ingo Blechschmidt already explained in the comments why we should expect a negative answer to the question (for most readings of "constructive logic"). Namely, if classical arithmetic proves $\forall n \in \mathbb{N} . \exists k \in \mathbb{N} . \phi(n, k)$, where $\phi(n,k)$ is quantifier-free, then so does intuitionistic arithmetic. So then, if intuitionstic arithmetic proves $\lnot\lnot \forall n \in \mathbb{N} . \exists k \in \mathbb{N} . \phi(n, k)$, then so does classical arithmetic, but classically we may remove the $\lnot\lnot$, and then go back to intuitionistic logic to get $\forall n \in \mathbb{N} . \exists k \in \mathbb{N} . \phi(n, k)$. The statement "Turing machine $M$ halts on every input" is of this form, namely
$$\forall n \in \mathbb{N} . \exists k \in \mathbb{N} . T(m, n, k),$$
where $m$ is a code of $M$ and $T$ is Kleene's predicate $T$.

What I would really like to explain is that in a sense this is the wrong question to ask. Let $H(m)$ be the statement that the Turing machine encoded by $m$ always halts, i.e., $$H(m) \iff \forall n \in \mathbb{N} . \exists k \in \mathbb{N} . T(m, n, k).$$ In terms of $H$, the question is: "Is there a number $m$ such that intuitionistic logic proves $\lnot\lnot H(m)$ but does not prove $H(m)$?" This seems to indicate to me that the author of the question is trying to imagine how $$\forall m \in \mathbb{N} . (\lnot\lnot H(m) \Rightarrow H(m))$$ might fail, and he expects to be able to find an instance of $m$ in which the implication fails. But in intuitionistic logic this is *not* the right way to think of quantification and implication!

The classical reading of $\forall x \in A . \psi(x)$ is "$\psi(a)$ holds for every element $a \in A$", whereas the intuitionistic reading of the same statement is "there is a *procedure* which takes as input any $a \in A$ and outputs evidence of $\phi(a)$. Here the word "procedure" is not fixed: it cold mean a computable map, or a continuous map, or computable with respect to an oracle, etc. But the point is this: in intuitionistic logic $\forall x \in A . \psi(x)$ may fail because there is no *procedure*, and not because there is a specific $b \in A$ for which $\lnot \psi(b)$ holds.

Applying the last paragraph to Markov's principle, we see that the "correct" question to ask was:

*Is there a procedure which takes as input (the code of) a Turing machine $M$ that never runs forever, and a number $n \in \mathbb{N}$, and halts and outputs the running time of $M(n)$?*

Friedman's trickorFriedman translation. The statement that a particular Turing machine halts on every input is of such a form. Therefore any classical termination proof gives rise to a constructive termination proof. $\endgroup$ – Ingo Blechschmidt Sep 11 '15 at 13:35