1
$\begingroup$

The proof of Gödel's incompleteness theorem can be streamlined by means of the Carnap-Gödel diagonal lemma and the ensuing fixed point theorem $\vdash_S G\leftrightarrow\lnot\Pi\ulcorner G\urcorner$ together with adequacy conditions upon the provability predicate $\Pi$, so that formal system S is incomplete if S is consistent and $\vdash_S A \Leftrightarrow \ \vdash_S\Pi\ulcorner A\urcorner$.

Is there a similar streamlining of the proof of the undecidability of the Halting Problem that appeals to the Carnap-Gödel diagonal lemma and fundamental adequacy conditions?

Improve this question
$\endgroup$
3
  • 4
    $\begingroup$ Turing's proof (the usual proof) of the undecidability of the halting problem is already a diagonalization: you make a program $p$ that halts on program $q$ if and only if $q$ does not halt on $q$; so $p$ halts on $p$ if and only if it doesn't, a contradiction. Meanwhile, the computability analogue of the diagonal lemma is the Kleene recursion theorem. I think one could easily use Kleene's theorem to prove the undecidability of the halting problem, but I wouldn't regard this as "streamlining", since Turing's argument is already succinct, as well as extremely robust. $\endgroup$
    – Joel David Hamkins
    Commented Mar 6, 2017 at 23:02
  • $\begingroup$ @JoelDavidHamkins Thanks. I wanted to understand if one can make a precise connection between notions such as "program $i$ halts on input $x$" and "formal system $i$ proves $x$ or proves $neg(x)$". $\endgroup$
    – Frode Alfson Bjørdal
    Commented Mar 7, 2017 at 13:24
  • $\begingroup$ @FrodeBjørdal The connection rather goes the other way. Undecidability of the Halting Problem shows, by Post's argument, that true sentences of arithmetic are not computably enumerable -- a version of the First Incompleteness Theorem. $\endgroup$
    – Andrew Polonsky
    Commented Mar 10, 2017 at 8:42

0

Reset to default

You must log in to answer this question.

Browse other questions tagged .