Constructive Mathematics and Termination

In the 1988 book The Universal Turing Machine A Half-Century Survey there is the paper "The Confluence of Ideas in 1936" by Robin Gandy. In section 4.2, Gandy writes:

"If one accepts, on whatever grounds, that a process terminates after a finite number of steps, then one should also accept, on the same grounds, that the number of steps can, in principle, be computed - one only needs a clock!"

Footnote  states:

"A constructive mathematician may have good grounds for believing that the process doesn't fail to terminate, without believing that it does terminate. Markov used his principle to jump over this gap."

My question is, can there exist a constructive logic and a Turing machine such that

1) the logic proves that the Turing machine doesn't fail to always terminate and

2) the logic does not prove that the Turing machine does always terminate?

• The question is subtle for the following reason: Peano arithmetic is conservative over Heyting arithmetic (i.e. intuitionistic Peano arithmetic) with respect to statements of the form "$\forall \exists (\ldots)$" (where no quantifiers may occur in the bracketed subexpression). This result goes by the name Friedman's trick or Friedman 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. – Ingo Blechschmidt Sep 11 '15 at 13:35
• For a general statement $\varphi$, not of the special form required by Friedman's trick, the story goes as follows. Believing that $\varphi$ doesn't fail to hold -- i.e. believing $\neg\neg\varphi$ -- is constructively weaker than believing that $\varphi$ holds. For instance, a proof of $\exists x(\ldots)$ requires an explicit witness of $x$, while a proof of $\neg\neg\exists x(\ldots)$ doesn't. A real-world example is the following: If in the morning you can't find the keys to your apartment, but you do know that they must be somewhere (as you used them to unlock the door last night), ... – Ingo Blechschmidt Sep 11 '15 at 13:44
• ... then you can constructively only justify $\neg\neg \exists x (\text{the key is at position x})$. (This real-world example doesn't fully work out since it confuses absolute mathematical truth with personal knowledge.) – Ingo Blechschmidt Sep 11 '15 at 13:46
• Why was this question put on hold? (Are the mods unaware that constructively, $\lnot \lnot P$ does not imply $P$, or is there some other reason?) – usul Sep 15 '15 at 16:57
• @usul, I don't know why the question was put on hold, but the mods have nothing to do with it. The five people who voted to close are not mods. – Gerry Myerson Sep 16 '15 at 0:17

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.
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)$?