30
$\begingroup$

It is known that with a countable set of algorithms (characterised by a Gödel number), we cannot compute (build a binary algorithm which checks belonging) all subsets of N.

A proof could be summarized as: if we could, then the set of all subsets of N would be countable (we could associate to each subset the Gödel number of the algorithm which computes it). As this is false, it proves the result.

This is a proof I like as it shows that the problem is equivalent to the subsets of N not being countable.

Now I'd like to prove that the halting problem is not solvable using only this same result (uncountability of N subsets), because I guess those are very close problem. Is it possible to prove it this way ?

Improve this question
$\endgroup$
2
  • $\begingroup$ Clearly both results can be proved by using the same technique (diagonalization). However, I do not think that it is possible to prove the undecidability of the halting problem just by using the uncountability of the family of subsets of ℕ, because the former is about the comparison between RE and R, both of which are countable families of subsets of ℕ. $\endgroup$
    – Tsuyoshi Ito
    Commented Mar 11, 2012 at 12:30
  • $\begingroup$ There are only countably many programs with access to the halting oracle, again characterized by a Godel number. However, the halting problem IS among this countable set. $\endgroup$
    – David Harris
    Commented Mar 11, 2012 at 13:09

1 Answer 1

Reset to default
43
$\begingroup$

The halting theorem, Cantor's theorem (the non-isomorphism of a set and its powerset), and Goedel's incompleteness theorem are all instances of the Lawvere fixed point theorem, which says that for any cartesian closed category, if there is an epimorphic map $e : A \to (A \Rightarrow B)$ then every $f : B \to B$ has a fixed point.

For a nice introduction to these ideas, see this blog post of Andrej Bauer.

Improve this answer
$\endgroup$
6
  • 7
    $\begingroup$ that's pretty neat. I didn't realize that there was an actual formal argument unifying them. $\endgroup$
    – Suresh Venkat
    Commented Mar 11, 2012 at 19:01
  • 8
    $\begingroup$ I have learnt by now to suspect that, if it looks the same and smells the same, there is a categorical argument about the sense in which it is the same. $\endgroup$
    – Vijay D
    Commented Mar 12, 2012 at 8:11
  • 2
    $\begingroup$ IMO, the two really nice things about Lawvere's theorem is that (a) it is a positive statement, rather than a negative one, and (b) the proof is half-a-dozen lines of simple lambda calculus calculations. $\endgroup$
    – Neel Krishnaswami
    Commented Mar 12, 2012 at 8:30
  • 7
    $\begingroup$ As I read the question, I thought to myself that someone should mention Lawvere's fixed point theorem. Imagine my delight when I read the answer :-) $\endgroup$
    – Andrej Bauer
    Commented Mar 12, 2012 at 19:55
  • 2
    $\begingroup$ e being epimorphic is not the right condition. You need point-surjectivity, which neither implies nor is implied by the condition of being epimorphic. See Remark 2.3 ncatlab.org/nlab/show/Lawvere%27s+fixed+point+theorem $\endgroup$
    – fhyve
    Commented Oct 24, 2017 at 20:13

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.