1
$\begingroup$

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

Improve this question
$\endgroup$
16
  • 1
    $\begingroup$ I think this is a duplicate of cstheory.stackexchange.com/questions/3810/… $\endgroup$
    – Huck Bennett
    Commented Jan 18, 2016 at 16:57
  • 4
    $\begingroup$ @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/… $\endgroup$
    – daniel gratzer
    Commented Jan 18, 2016 at 18:04
  • 2
    $\begingroup$ 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. $\endgroup$
    – Kaveh
    Commented Jan 18, 2016 at 22:51
  • 3
    $\begingroup$ 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. $\endgroup$
    – Kaveh
    Commented Jan 18, 2016 at 23:01
  • 4
    $\begingroup$ 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. $\endgroup$
    – Kaveh
    Commented Jan 18, 2016 at 23:50

1 Answer 1

Reset to default
1
$\begingroup$

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.

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.