<p>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.</p>

<ul>
<li>Lawvere, F. William. <a href="http://tac.mta.ca/tac/reprints/articles/15/tr15abs.html">Diagonal Arguments and Cartesian Closed Categories</a>. Lecture Notes in Mathematics, 92 (1969), 134-145.</li>
</ul>

<p>For a nice introduction to these ideas, see this <a href="http://math.andrej.com/2007/04/08/on-a-proof-of-cantors-theorem/">blog post of Andrej Bauer</a>.</p>

CC BY-SA 3.0
2012-03-11T19:01:51.773Z
that's pretty neat. I didn't realize that there was an actual formal argument unifying them.
Suresh Venkat
CC BY-SA 3.0
2012-03-12T08:11:18.317Z
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.
Vijay D
CC BY-SA 3.0
2012-03-12T08:30:43.923Z
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.
Neel Krishnaswami
CC BY-SA 3.0
2012-03-12T19:55:08.330Z
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 :-)
Andrej Bauer
CC BY-SA 3.0
2017-10-24T20:13:31.797Z
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 https://ncatlab.org/nlab/show/Lawvere%27s+fixed+point+theorem
fhyve
CC BY-SA 4.0
2020-12-17T21:21:13.277Z
Here is the formalism to get the halting theorem out of it https://cs.ru.nl/~dfrumin/pdf/diagonal_argument.pdf
Weier
CC BY-SA 3.0
2012-03-11T14:49:36.017Z
2012-03-11T14:49:36.017Z
Neel Krishnaswami
<p>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.</p>

<p>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.</p>

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

<p>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 ?</p>

CC BY-SA 3.0
2012-03-11T12:30:49.737Z
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](http://qwiki.stanford.edu/index.php/Complexity_Zoo:R#re) and [R](http://qwiki.stanford.edu/index.php/Complexity_Zoo:R#r), both of which are countable families of subsets of ℕ.
Tsuyoshi Ito
CC BY-SA 3.0
2012-03-11T13:09:24.237Z
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.
David Harris
<computability><halting-problem>
Halting problem, uncomputable sets: common mathematical proof?
Weier
# Halting problem, uncomputable sets: common mathematical proof?

(Asked by: username_0 on 2012-03-11)

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 ?

**Tags:** computability, halting-problem
> **Comments:**
> **username_1**: 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](http://qwiki.stanford.edu/index.php/Complexity_Zoo:R#re) and [R](http://qwiki.stanford.edu/index.php/Complexity_Zoo:R#r), both of which are countable families of subsets of ℕ.  
> **username_2**: 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.  

---

## 1 answers

### Answer by username_3 on 2012-03-11. Score: 43 | Accepted answer

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.

* Lawvere, F. William. [Diagonal Arguments and Cartesian Closed Categories](http://tac.mta.ca/tac/reprints/articles/15/tr15abs.html). Lecture Notes in Mathematics, 92 (1969), 134-145.

For a nice introduction to these ideas, see this [blog post of Andrej Bauer](http://math.andrej.com/2007/04/08/on-a-proof-of-cantors-theorem/).

> **Comments:**
> **username_4**: that's pretty neat. I didn't realize that there was an actual formal argument unifying them.  
> **username_5**: 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.  
> **username_3**: 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.  
> **username_6**: 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 :-)  
> **username_7**: 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 https://ncatlab.org/nlab/show/Lawvere%27s+fixed+point+theorem  
> **username_0**: Here is the formalism to get the halting theorem out of it https://cs.ru.nl/~dfrumin/pdf/diagonal_argument.pdf  

---

