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 ?

  • $\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 Mar 11 '12 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 Mar 11 '12 at 13:09

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.

  • 7
    $\begingroup$ that's pretty neat. I didn't realize that there was an actual formal argument unifying them. $\endgroup$ – Suresh Venkat Mar 11 '12 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 Mar 12 '12 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 Mar 12 '12 at 8:30
  • 6
    $\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 Mar 12 '12 at 19:55
  • 1
    $\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 Oct 24 '17 at 20:13

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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