# Lawvere's fixed point theorem and the Recursion Theorem

Building off of Qiaochu's comment on my answer to a previous mathoverflow question, I would like to know: can the Recursion Theorem, $$\forall e\exists k[\Phi_e\text{ is total }\implies \Phi_{\Phi_e(k)}\cong\Phi_k],$$ be gotten as a corollary of Lawvere's Fixed Point Theorem: $$\text{If \mathcal{C} is Cartesian closed and }f: A\rightarrow B^A\text{ is an epimorphism, then every g: B\rightarrow B has a fixed point.}$$

I tried to work this out myself, but I couldn't seem to come up with the right category to live in; I feel like the proof should be fairly simple, and quite illuminating. Alternatively, if it can't be done (at least in a reasonable way), I'd like to know what the obstacle is.

(I apologize if this question is too low-level for MO; my own background in category theorem is somewhat limited, so I don't know how whether this is actually a research-level question. As partial justification, I would like to point out that from a computability theory perspective, this doesn't seem entirely trivial.)

-
See Theorem 5 here: arxiv.org/pdf/math/0305282v1.pdf. – tci May 19 '13 at 23:07
Tanmay, isn't that an answer? – François G. Dorais May 19 '13 at 23:50
That's an answer for logicians, yes. Are we all logicians here? I can be. – Andrej Bauer May 20 '13 at 7:23
@Tanmay That looks like a standard proof of the recursion theorem—without any explicit reference to Lawvere’s theorem (it looks kinda analogously, but we knew that before). – The User May 20 '13 at 16:44

There is indeed a very close connection between Lawvere's fixed-point theorem and Recursion theorem, but one has to look at it the right way. Namely, it all becomes clear once we do it in the effective topos.

Let us start by recalling Lawvere's theorem. (I use $X \to Y$ and $Y^X$ as synonyms for the set of all functions from $X$ to $Y$.)

Theorem (Lawvere): If $e : A \to B^A$ is onto then every $f : B \to B$ has a fixed point.

Proof. There is $x \in A$ such that $e(x)(y) = f(e(y)(y))$ for all $y \in A$, because $e$ is onto and $x \mapsto f(e(y)(y))$ is a map from $A$ to $B$. Then $e(x)(x) = f(e(x)(x))$ so $e(x)(x)$ is a fixed point of $f$. QED.

Now here is Recursion theorem written so that it is most similar to Lawvere's theorem. I explain below why this is the Recursion theorem.

Recursion theorem: Suppose countable choice holds and $e : \mathbb{N} \to B^{\mathbb{N}}$ is onto. Then every total relation $R \subseteq B \times B$ has a fixed point.

We say that $x \in B$ is the fixed point of $R$ if $R(x,x)$. Note that total relations can also be viewed as multivalued maps, so this is a fixed point theorem which generalizes the instance of Lawvere's fixed point theorem in which $A = \mathbb{N}$.

Proof. Because $R$ is total, for every $n \in \mathbb{N}$ there is $y \in B$ such that $R(e(n)(n), y)$. Therefore, by countable choice, there is a map $c : \mathbb{N} \to B$ such that $R(e(n)(n), c(n))$ for all $n \in \mathbb{N}$. As $e$ is onto there exists $k \in \mathbb{N}$ such that $e(k) = c$. But then $e(k)(k)$ is a fixed point of $R$ because $e(k)(k) = c(k)$. QED.

Of course, you are asking yourself what the theorem has to do with Recursion theorem from computability theory. Note that the proof is intuitionistic and uses countable choice, therefore it is valid in the effective topos. To get the connection with the classical recursion theorem, we need to understand what the object of partial computable maps looks like in the effective topos. In fact, it is just the function space $\mathbb{N} \to \mathbb{N}_\bot$ where I do not really want to get into the internal definition of $\mathbb{N} _{\bot}$, let me describe it as a numbered set instead: the underlying set of $\mathbb{N} _\bot$ is $\mathbb{N} \cup \lbrace \bot \rbrace$. A number $r$ realizes $\bot \in \mathbb{N} _\bot$ if the $r$-th Turing machine diverges on input $0$, and it realizes $n \in \mathbb{N} _\bot$ if the $r$-th Turing machine halts and outputs $n$ on input $0$.

Another way to explain the object of partial computable maps $\mathbb{N} \to \mathbb{N} _\bot$ in the effective topos is that this is the object of those partial maps whose domain is a countable subset of $\mathbb{N}$ (which of course is just the internal version of the classic theorem that partial computable maps have c.e. sets as their domains).

Anyhow, $\mathbb{N} \to \mathbb{N}_\bot$ is countable in the effective topos. This can be proved from the axioms of synthetic computability, but a shortcut is just to observe that there is an effective enumeration of partial computable maps, which realizes an enumeration $\varphi : \mathbb{N} \to (\mathbb{N} \to \mathbb{N} _\bot)$ in the effective topos.. But then, since by $\lambda$-calculus $$(\mathbb{N} \to (\mathbb{N} \to \mathbb{N} _\bot)) \cong (\mathbb{N} \times \mathbb{N} \to \mathbb{N} _\bot) \cong \mathbb{N} \to \mathbb{N} _\bot$$ we see that we may apply Recursion theorem to $\mathbb{N} \to \mathbb{N} _\bot$. So, given any $f : \mathbb{N} \to \mathbb{N}$, consider the total relation $R$ defined on $\mathbb{N} \to \mathbb{N} _\bot$ by $$R(u,v) \iff \exists k \in \mathbb{N} . u = \varphi_k \land v = \varphi_{f(k)}.$$ There is a fixed point $u$ and so by definition of $R$ there is $k$ such that $u = \varphi_k$ and $u = \varphi_{f(k)}$. And we have the usual recursion theorem as a consequence.

Let's do another one, just to convince you this is the recursion theorem. There is an enumeration $W$ of all countable subsets of $\mathbb{N}$ (yes, there are countably many countable subsets of $\mathbb{N}$ in the effective topos, and that is a way cool axiom if you like to smoke weird stuff). A typical exercise in recursion theorem asks for $n$ such that $W_n = \lbrace{ n \rbrace}$. Because the countable subsets of $\mathbb{N}$ satisfy the condition of recursion theorem, we get such a set simply by considering the total relation $R$ defined by $$R(S,T) \iff \exists m \in \mathbb{N} . S = W_m \land T = \lbrace m\rbrace.$$ Indeed, a fixed point is a countable set $S$ such that for some $m$ we have $S = W_m$ and $S = \lbrace m \rbrace$.

I could go on, but I am in fact preparing a paper about this which should appear on arXiv in a couple of days. See also my materials on synthetic computability (older material has suboptimal proofs of recursion theorem).

-
But it is only “similar”—it is not an application? – The User May 20 '13 at 16:49
A special case of Lavwere's fixed point theorem is a special case of Recursion theorem. – Andrej Bauer May 20 '13 at 17:50