<p>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:</p>

<blockquote>
  <p>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)$$
  ?</p>
</blockquote>

<p>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.)</p>

<p>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)$$</p>

<blockquote>
  <p>Is there any $m$ such that $H_2(m)$ satisfied in natural numbers?</p>
</blockquote>

<p>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)$.</p>

<p>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.  </p>

CC BY-SA 3.0
2016-01-18T19:18:16.987Z
2016-01-18T19:18:16.987Z
Erfan Khaniki
<p>Does there exist any constructive (indeed, computable) proof of the Halting Problem? All the ones I have encountered make use of proof by contradiction.</p>

<p>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).</p>

CC BY-SA 3.0
2016-01-18T16:57:38.030Z
I think this is a duplicate of http://cstheory.stackexchange.com/questions/3810/is-there-an-alternative-proof-of-the-tm-halting-problem-other-than-the-standard
Huck Bennett
CC BY-SA 3.0
2016-01-18T16:59:51.063Z
I think you misunderstood Sipser. He uses diagonalization to show that there exists *some* undecidable language, and then proves (not using diagonalization) that the halting problem in particular is undecidable.
Huck Bennett
CC BY-SA 3.0
2016-01-18T17:03:38.417Z
Is the constructive issue really the proof by contradiction or the use of LEM to assert that a function either halts or doesn't? Constructively, to prove something is false you build an effective transformation from $A \to \bot$ so it may "look like contradiction" even though it's not.
daniel gratzer
CC BY-SA 3.0
2016-01-18T17:05:44.030Z
@HuckBennett But he doesn't, he uses diagonalisation as an afterthought to the proof...
Noldorin
CC BY-SA 3.0
2016-01-18T17:08:02.157Z
@jozefg: Possibly both. I kind of brushed over that issue of LEM, since it's possible that a restricted form of LEM applies to the predicate "TM does halt" (though I'm not at all sure on this).
Noldorin
CC BY-SA 3.0
2016-01-18T17:12:54.237Z
@Noldorin "TM does halt" is a pretty big thing to assume LEM for though because the undecidability of the halting problem still applies in whatever constructive metalanguage we choose though; we cannot have something like an intuistionistic type theory as the metatheory then because it cannot possibly realize a decider for that predicate.
daniel gratzer
CC BY-SA 3.0
2016-01-18T17:44:34.577Z
@jozefg: Yeah, that's quite true: the lack of LEM (for that predicate) seems to be the real problem here. The 'proof by contradiction' is on second thought a benign one.
Noldorin
CC BY-SA 3.0
2016-01-18T17:53:33.930Z
Down-voters care to explain??
Noldorin
CC BY-SA 3.0
2016-01-18T17:55:52.963Z
@jozefg: The question now is: where exactly in the common proof is LEM used? Hmm.
Noldorin
CC BY-SA 3.0
2016-01-18T18:04:06.240Z
@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: https://github.com/jonsterling/JonPRL/blob/master/example/foundations/halting-problem.jonprl
daniel gratzer
CC BY-SA 3.0
2016-01-18T21:22:48.567Z
@jozefg: Thanks, I'm starting to see you're right. There's one other point though. (Are you familiar with the proof in Sipser?) It seems like the use of the diagonal argument is very artificial and not in fact needed at all. Does it actually have a genuine place in the proof, or other reasoning connected to the halting problem?
Noldorin
CC BY-SA 3.0
2016-01-18T22:51:34.123Z
The proof is constructive. It is a confusion resulting from thinking that diagonalization is not constructive. Please check our [help/on-topic], this question seems more suitable for [cs.se] or [math.se].
Kaveh
CC BY-SA 3.0
2016-01-18T23:01:23.687Z
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
CC BY-SA 3.0
2016-01-18T23:09:46.127Z
@Kaveh: There's no confusion about diagonalisation being non-constructive. Please reread my question; the issue of diagonalisation is separate.
Noldorin
CC BY-SA 3.0
2016-01-18T23:50:07.927Z
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.
Kaveh
CC BY-SA 3.0
2016-01-19T20:24:50.837Z
@Kaveh: Sure, I'm with you there. It's my "side-question" that I'm still unsure about: where does diagonalisation come into it at all? I don't see any need for it in the proof.
Noldorin
<halting-problem>
Constructive proof of the Halting Problem
Noldorin
# Constructive proof of the Halting Problem

(Asked by: username_0 on 2016-01-18)

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

**Tags:** halting-problem

> **Comments:**
> **username_1**: I think this is a duplicate of http://cstheory.stackexchange.com/questions/3810/is-there-an-alternative-proof-of-the-tm-halting-problem-other-than-the-standard  
> **username_1**: I think you misunderstood Sipser. He uses diagonalization to show that there exists *some* undecidable language, and then proves (not using diagonalization) that the halting problem in particular is undecidable.  
> **username_2**: Is the constructive issue really the proof by contradiction or the use of LEM to assert that a function either halts or doesn't? Constructively, to prove something is false you build an effective transformation from $A \to \bot$ so it may "look like contradiction" even though it's not.  
> **username_0**: @HuckBennett But he doesn't, he uses diagonalisation as an afterthought to the proof...  
> **username_0**: @jozefg: Possibly both. I kind of brushed over that issue of LEM, since it's possible that a restricted form of LEM applies to the predicate "TM does halt" (though I'm not at all sure on this).  
> **username_2**: @username_0 "TM does halt" is a pretty big thing to assume LEM for though because the undecidability of the halting problem still applies in whatever constructive metalanguage we choose though; we cannot have something like an intuistionistic type theory as the metatheory then because it cannot possibly realize a decider for that predicate.  
> **username_0**: @jozefg: Yeah, that's quite true: the lack of LEM (for that predicate) seems to be the real problem here. The 'proof by contradiction' is on second thought a benign one.  
> **username_0**: Down-voters care to explain??  
> **username_0**: @jozefg: The question now is: where exactly in the common proof is LEM used? Hmm.  
> **username_2**: @username_0 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: https://github.com/jonsterling/JonPRL/blob/master/example/foundations/halting-problem.jonprl  
> **username_0**: @jozefg: Thanks, I'm starting to see you're right. There's one other point though. (Are you familiar with the proof in Sipser?) It seems like the use of the diagonal argument is very artificial and not in fact needed at all. Does it actually have a genuine place in the proof, or other reasoning connected to the halting problem?  
> **username_3**: The proof is constructive. It is a confusion resulting from thinking that diagonalization is not constructive. Please check our [help/on-topic], this question seems more suitable for [cs.se] or [math.se].  
> **username_3**: 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.  
> **username_0**: @username_3: There's no confusion about diagonalisation being non-constructive. Please reread my question; the issue of diagonalisation is separate.  
> **username_3**: 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.  
> **username_0**: @username_3: Sure, I'm with you there. It's my "side-question" that I'm still unsure about: where does diagonalisation come into it at all? I don't see any need for it in the proof.  

---

## 1 answers

### Answer by username_4 on 2016-01-18. Score: 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.


---

