1

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

Noldorin
  • 857
  • 1
  • 9
  • 12
  • 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 – Huck Bennett Jan 18 '16 at 16:57
  • 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 Jan 18 '16 at 16:59
  • 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 Jan 18 '16 at 17:03
  • @HuckBennett But he doesn't, he uses diagonalisation as an afterthought to the proof... – Noldorin Jan 18 '16 at 17:05
  • @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 Jan 18 '16 at 17:08
  • @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 Jan 18 '16 at 17:12
  • @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 Jan 18 '16 at 17:44
  • Down-voters care to explain?? – Noldorin Jan 18 '16 at 17:53
  • @jozefg: The question now is: where exactly in the common proof is LEM used? Hmm. – Noldorin Jan 18 '16 at 17:55
  • 4
    @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 Jan 18 '16 at 18:04
  • @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 Jan 18 '16 at 21:22
  • 2
    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 Jan 18 '16 at 22:51
  • 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. – Kaveh Jan 18 '16 at 23:01
  • @Kaveh: There's no confusion about diagonalisation being non-constructive. Please reread my question; the issue of diagonalisation is separate. – Noldorin Jan 18 '16 at 23:09
  • 4
    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 Jan 18 '16 at 23:50
  • @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 Jan 19 '16 at 20:24

1 Answers1

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.

Erfan Khaniki
  • 342
  • 2
  • 11