Constructive proof of the Halting Problem

Question

Does there exist any constructive (indeed, computable) proof of the Halting Problem? All the ones I have encountered make use of proof by contradiction.

As an aside, some proofs I have encountered make use of Cantor's diagonal argument, but this seems to be purely extraneous (e.g. the proof in Sipser).

• Huck Bennett: I think this is a duplicate of cstheory.stackexchange.com/questions/3810/…
• daniel gratzer: @Noldorin It actually may not be a problem, by assumption we have some decider $halt$ with the property that it always returns true or false and $halt(\bar{p}) = 1 \iff p \Downarrow$ so there is really no nonconstructive reasoning; the use of what looks like LEM is just a hypothesis. The proof is constructive. As positive evidence: I formalized it in a Nuprl like theorem prover which is certainly constructive: github.com/jonsterling/JonPRL/blob/master/example/foundations/…
• Kaveh: The proof is constructive. It is a confusion resulting from thinking that diagonalization is not constructive. Please check our help center, this question seems more suitable for Computer Science or Mathematics.
• Kaveh: ps: you are confusing the rule for introducing negation (from $\Gamma, A \vdash \bot$ to $\Gamma \vdash \lnot A$) with proof by contradiction (RAA) (from $\Gamma, \lnot A \vdash \bot$ to $\Gamma \vdash A$). The former is valid constructively.
• Kaveh: The answer is what I wrote in the previous comment: assuming $A,ドル driving $\bot,ドル therefore concluding $\lnot A$ is constructive. We assume $H$ is decidable, we derive a contradiction from that, therefore $H$ is not decidable. This is not proof by contradiction, this is introduction of negation which is valid constructively. If this is not the part that confuses you then specify which part of the proof you think is not constructive.

Answer 1

I think if we want to answer this problem constructively, then we should be able propose problem constructively. Let language of arithmetic be $L=\{0,S,+,\cdot \}$ and $\phi(n,x,y)$ be kleene predicate in $L$. Now the first problem is:

Is there any $m\in \mathbb{N}$ such that $$H_1(m):=\forall x\in\mathbb{N}:\forall y \in \mathbb{N} \neg \phi(x,x,y)\leftrightarrow \exists z\in \mathbb{N} \phi(m,x,z)$$ ?

Proof. Suppose there exists such $m,ドル so by above definition we have: $$\forall y \in \mathbb{N} \neg \phi(m,m,y)\leftrightarrow \exists z\in \mathbb{N} \phi(m,m,z)$$ and this leads to a contradiction, therefore there does not such $m$. (note that $\neg \exists A(x)\rightarrow \forall x \neg A(x)$ has a constructive proof.)

Define $$H_2(m):=\forall x\in \mathbb{N}\exists ! y\in\{0,1\} \phi(m,x,y) \land \forall x\in\mathbb{N}:\exists u \in \mathbb{N}\phi(x,x,u)\leftrightarrow \phi(m,x,1)$$

Is there any $m$ such that $H_2(m)$ satisfied in natural numbers?

proof. If there exists such m, we can construct number $m'$ from $m$ such that $H_1(m')$ satisfied in natural numbers and this lead to a contradiction, therefore we have $\forall n\in \mathbb{N}\neg H_2(n)$.

We can see that $H_2(n)$ means that "partial recursive function with code $n$ is a solution for halting problem". Actually we can not deduce constructively that $$\neg H_2(n)\leftrightarrow \neg(\forall x\in \mathbb{N}\exists ! y\in\{0,1\} \phi(n,x,y)) \lor \neg(\forall x\in\mathbb{N}:\exists u \in \mathbb{N}\phi(x,x,u)\leftrightarrow \phi(n,x,1))$,ドル but $\neg H_2(n)$ means there exists a time in tmeline that we figure out $\neg\forall x\in \mathbb{N}\exists ! y\in\{0,1\} \phi(n,x,y)$ or $\neg\forall x\in\mathbb{N}:\exists u \in \mathbb{N}\phi(x,x,u)\leftrightarrow \phi(n,x,1)$ although maybe we don't know which of them is true this moment.