<p>I'm probably not directly answering your question, but there is a common mathematical generalisation of a lot of paradoxa, including G&ouml;del's theorems and the Y-combinator.
I think this was first explored by Lawvere. See also [2, 3].</p>

<ol>
<li><p>F. W. Lawvere, <a href="http://www.tac.mta.ca/tac/reprints/articles/15/tr15.pdf">Diagonal arguments and cartesian closed categories</a>.</p></li>
<li><p>D. Pavlovic, <a href="ftp://ftp.kestrel.edu/pub/papers/pavlovic/para-AML92.pdf">On the structure of paradoxes</a>.</p></li>
<li><p>N. S. Yanofsky, <a href="http://arxiv.org/pdf/math/0305282.pdf">A Universal Approach to Self-Referential Paradoxes,
Incompleteness and Fixed Points</a>.</p></li>
</ol>

CC BY-SA 3.0
2014-11-06T11:11:00.453Z
Thank you, Martin, these are very interesting references! I'm having trouble however to extract from the logical situation a categorical context to which Lawvere's logical fixed point theorem applies verbatimly. In Yanofsky's article, for example, I doubt that the substitution operation $\text{Lind}^1\times\text{Lind}^1\to\text{Lind}^0$ is well-defined if one considers terms up to logical equivalence. Do you understand this?
Hanno
CC BY-SA 3.0
2014-11-06T11:27:46.530Z
@HannoBecker This may be quite difficult and sensitive to coding.
Martin Berger
CC BY-SA 3.0
2014-11-04T12:33:44.260Z
2014-11-04T21:10:33.923Z
2014-11-04T21:10:33.923Z
Martin Berger
<p>I don't have a complete answer to your question, but I do have this:</p>

<p>As per <a href="http://en.wikipedia.org/wiki/Kleene%27s_recursion_theorem#Kleene.27s_second_recursion_theorem">Wikipedia</a> says</p>

<blockquote>
  <p>For every partial recursive function $Q(x, y)$ there exists an index $p$ such that
  $$ \varphi_p\simeq \lambda y.Q(p, y)$$
  where $\varphi$ is a bijection between $\mathbb{N}$ and the partial recursive functions.</p>
</blockquote>

<p>Now it's pretty clear that this theorem is a consequence of the fix-point theorem in the $\lambda$-calculus. We can use this to prove a <em>variant</em> of the logical-fixed point theorem:</p>

<blockquote>
  <p>For every formula $\phi$ and r.e. theory ${\mathscr T}$ containing arithmetic, there exists an index $n$ such that
  $${\mathscr T}\vdash \phi(\overline{n}) \Leftrightarrow {\mathscr T}\vdash \exists y, \varphi_n(y)=0$$</p>
</blockquote>

<p>This isn't quite what you want, but an internalization trick can give you the stronger statement</p>

<blockquote>
  <p>${\mathscr T}\vdash \phi(\overline{n})\leftrightarrow \exists y, \varphi_n(y) = 0$</p>
</blockquote>

<p>Now again, this is not quite the logical fixed-point theorem, but it can serve the same purpose.</p>

<blockquote>
  <p><strong>Proof:</strong>
  Define $Q(x,y)$ to be the recursive function defined by
  $$Q(x,y) = 0 \mbox{ iff }{\mathscr T}\vdash \phi(\overline{x})\mbox{ in at most $y$ steps} $$
  It is easy to see that $Q$ is (total) recursive. Note that $\exists y, Q(x, y)$ expresses the fact "${\mathscr T}$ proves $\phi(\overline{x})$", and that this is true iff ${\mathscr T}\vdash\exists y,Q(\overline{x}, y)$ (we are assuming $\omega$-consistency). Now a simple application of the Kleene Recursion Theorem on $Q$ gives us the desired conclusion. $\square$</p>
</blockquote>

<p>With a little thought, you can probably strengthen this argument to give you the full theorem directly without the internalization.</p>

CC BY-SA 3.0
2014-11-06T11:04:52.260Z
Thank you for your answer! Let me go slowly to see if I understand you: In your first statement, can $\varphi:{\mathbb N}\cong\text{C}({\mathbb N},{\mathbb N})$ be completely arbitrary, or do you at least want the induced Currying map $$\text{C}({\mathbb N}^2,{\mathbb N})\to\text{Map}({\mathbb N},\text{C}({\mathbb N},{\mathbb N}))\cong\text{Map}({\mathbb N},{\mathbb N})$$ to have image in the partial recursive functions $\text{C}({\mathbb N},{\mathbb N})$, and that the induced evaluation ${\mathbb N}^2\to{\mathbb N}$, $(n,m)\mapsto\varphi(n)(m)$ be computable?
Hanno
CC BY-SA 3.0
2014-11-06T11:05:27.903Z
With these assumptions, I understand the statement is true; however, though - as in many of these types of statements - the *similarity* with the $Y$-combinator in $\lambda$-calculus is striking, I do not see how you would make it a *formal consequence* of the latter. Could you elaborate?
Hanno
CC BY-SA 3.0
2014-11-06T18:43:04.903Z
For the first point: you are correct, you want $\varphi$ to be "sane" in the sense you describe. For the second point: the $Y$ combinator essentially expresses $Y\ f\simeq f(Y\ f)$. The recursion theorem says essentially the same thing: take $p:= Y\ Q$. However, the theory of partial recursive functions allows for slightly more generality: the *code* of a function is distinct from the function itself. The equivalent in $\lambda$-calculus would be having a ``quote`` and ``eval`` operation as in Lisp. In this sense, the recursion theorem is more general than the existence of the $Y$ combinator.
cody
CC BY-SA 3.0
2014-11-04T21:15:47.103Z
2014-11-04T21:15:47.103Z
cody
<p><em>This question has also been posted on Math.SE,</em></p>
<p><em><a href="https://math.stackexchange.com/questions/1002540/fixed-points-in-computability-nd-logic">https://math.stackexchange.com/questions/1002540/fixed-points-in-computability-nd-logic</a></em></p>
<p><em>I hope it is ok to also post it here. If not, or if it is too basic for CS.SE, please tell me and I will delete it.</em></p>
<hr />
<p>I would like to understand better the relation between fixed point theorems in logic and <span class="math-container">$\lambda$</span>-calculus.</p>
<p><em><b>Background</b></em></p>
<p><em>1) The role of fixed points in incompleteness &amp; undefinability of truth</em></p>
<p>As far as I understand, apart from the fundamental idea of internalizing logic, the key to both the proofs of <em>Tarski's undefinability of truth</em> and <em>Goedel's incompleteness theorem</em> is the following <em>logical fixed point theorem</em>, living in a constructive, finitistic metatheory (I hope the formulation is ok, please correct me if something's incorrect or inprecise):</p>
<blockquote>
<p><b>Existence of fixed points in logic</b></p>
<p><em>Suppose</em> <span class="math-container">${\mathscr T}$</span> is a sufficiently expressive, recursively enumerable theory over the language <span class="math-container">${\mathcal L}$</span>, and let <span class="math-container">${\mathbf C}$</span> be a coding of <span class="math-container">${\mathcal L}$</span>-formulas in <span class="math-container">${\mathscr T}$</span>, that is, an algorithm turning arbitrary well-formed <span class="math-container">${\mathcal L}$</span>-formulas <span class="math-container">$\varphi$</span> into <span class="math-container">${\mathcal L}$</span>-formulas with one free variable <span class="math-container">${\mathbf C}(\varphi)(v)$</span>, such that for any <span class="math-container">${\mathcal L}$</span>-formula <span class="math-container">$\varphi$</span> we have <span class="math-container">${\mathscr T}\vdash \exists! v: {\mathbf C}(\varphi)(v)$</span>.</p>
<p><em>Then</em> there exists an algorithm <span class="math-container">${\mathbf Y}$</span> turning well-formed <span class="math-container">${\mathcal L}$</span>-formulas in one free variable into closed well-formed <span class="math-container">${\mathcal L}$</span>-formulas, such that for any <span class="math-container">${\mathcal L}$</span>-formula in one free variable <span class="math-container">$\phi$</span> we have <span class="math-container">$${\mathscr T}\vdash {\mathbf Y}(\phi)\Leftrightarrow \exists v: {\mathbf C}({\mathbf Y}(\phi))(v)\wedge \phi(v),$$</span> which, interpreting <span class="math-container">${\mathbf C}$</span> as a defined function symbol <span class="math-container">$\lceil -\rceil$</span>, might also be written more compactly as<span class="math-container">$${\mathscr T}\vdash {\mathbf Y}(\phi)\Leftrightarrow \phi(\lceil{\mathbf Y}(\phi)\rceil).$$</span></p>
<p>In other words, <span class="math-container">${\mathbf Y}$</span> is an algorithm for the construction of fixed points with respect to <span class="math-container">${\mathscr T}$</span>-equivalence of one-variable <span class="math-container">${\mathcal L}$</span>-formulas.</p>
</blockquote>
<p>This has at least two applications:</p>
<ul>
<li><p>Applying it to the predicate <span class="math-container">$\phi(v)$</span> expressing &quot;<span class="math-container">$v$</span> codes a sentence which, when instantiated with its own coding, is not provable.&quot; yields the formalization of &quot;This sentence is not provable&quot; which lies at the heart of Goedel's argument.</p>
</li>
<li><p>Applying it to <span class="math-container">$\neg\phi$</span> for an arbitrary sentence <span class="math-container">$\phi$</span> yields Tarski's undefinability of truth.</p>
</li>
</ul>
<p><em>2) Fixed points in untyped <span class="math-container">$\lambda$</span>-calculus</em></p>
<p>In untyped <span class="math-container">$\lambda$</span>-calculus the construction of fixed points is important in the realization of recursive functions.</p>
<blockquote>
<p><b>Existence of fixed points in <span class="math-container">$\lambda$</span>-calculus:</b></p>
<p>There is a <em>fixed point combinator</em>, i.e. a <span class="math-container">$\lambda$</span>-term <span class="math-container">$Y$</span> such that for any <span class="math-container">$\lambda$</span>-term <span class="math-container">$f$</span>, we have <span class="math-container">$$f(Y f)\sim_{\alpha\beta} Yf.$$</span></p>
</blockquote>
<p><em><b>Observation</b></em></p>
<p>What leaves me stunned is that the fixed point combinator <span class="math-container">$\lambda f.(\lambda x. f(x x))(\lambda x. f(x x))$</span> in <span class="math-container">$\lambda$</span>-calculus directly reflects, in a very clean and nontechnical way, the usual proof of the logical fixed point theorem:</p>
<p><em>Very roughly</em>, given a formula <span class="math-container">$\varphi$</span>, one considers the formalization <span class="math-container">$\varphi(v)$</span> of the statement &quot;<span class="math-container">$v$</span> codes a sentence which, when instantiated with itself, satisfies <span class="math-container">$\phi$</span>&quot;, and puts <span class="math-container">${\mathbf A}(\phi) := \varphi(\lceil\varphi\rceil)$</span>. The sentence <span class="math-container">$\varphi(v)$</span> is like <span class="math-container">$\lambda x. f(x x)$</span>, and <span class="math-container">$\varphi(\lceil\varphi\rceil)$</span> corresponds to <span class="math-container">$(\lambda x. f(x x))(\lambda x. f(x x))$</span>.</p>
<p><em><b>Question</b></em></p>
<p>Despite its quickly described idea, I found the proof of the logical fixed point theorem quite technical and difficult to carry out in all details; Kunen does so for example in Theorem 14.2 of his 'Set Theory' book. On the other hand, the <span class="math-container">$Y$</span>-combinator in <span class="math-container">$\lambda$</span>-calculus is very simple and its properties are easily verified.</p>
<blockquote>
<p><em>Does the logical fixed point theorem follow rigorously from fixed point combinators in <span class="math-container">$\lambda$</span>-calculus?</em></p>
<p>E.g., can one model the <span class="math-container">$\lambda$</span>-calculus by <span class="math-container">${\mathcal L}$</span>-formulas up to logical equivalence, so that the interpretation of any fixed point combinator gives an algorithm as described in the logical fixed point theorem?</p>
</blockquote>
<hr />
<p><b><em>Edit</em></b></p>
<p>In view of the many other instances of the same diagonalization argument described in Martin's and Cody's answers, one should rephrase the question:</p>
<blockquote>
<p><em>Is there a common generalization of the diagonalization arguments following the principle expressed in the <span class="math-container">$Y$</span>-combinator? <span class="math-container">$$\lambda f.(\lambda x. f(xx))(\lambda x.f(xx))$$</span></em></p>
</blockquote>
<p>If I understand it correctly one proposal is <em>Lawvere's Fixed Point Theorem</em>, see below. Unfortunately however I can't follow the relevant specializations in either of the articles that Martin cited in his answer, and I'd be happy if someone could explain them. First, for completeness:</p>
<blockquote>
<p><b><em>Lawvere's Fixed Point Theorem</em></b></p>
<p>Let <span class="math-container">${\mathscr C}$</span> be a category with finite products and <span class="math-container">$\varphi: A\times A\to Y$</span> such that for any morphism <span class="math-container">$f: A\to Y$</span> in <span class="math-container">${\mathscr C}$</span> there is some <span class="math-container">$\lceil f\rceil: 1\to A$</span> such that for all points <span class="math-container">$p: 1\to A$</span>  one has <span class="math-container">$$1\xrightarrow{p} A\xrightarrow{\ f\ } Y\ \  =\ \  1\xrightarrow{p} A\xrightarrow{\langle \lceil f\rceil,\text{id}_A\rangle} A\times A\xrightarrow{\varphi} Y.$$</span></p>
<p>Then for any endomorphism <span class="math-container">$g: Y\to Y$</span>, putting <span class="math-container">$$f\ :=\ A\xrightarrow{\Delta} A\times A\xrightarrow{\varphi} Y\xrightarrow{g} Y,$$</span> any choice of <span class="math-container">$\lceil f\rceil$</span> gives rise to a fixed point of <span class="math-container">$g$</span>, namely
<span class="math-container">$$1\xrightarrow{\langle\lceil f\rceil,\lceil f\rceil\rangle} A\times A\xrightarrow{\varphi} Y.$$</span></p>
</blockquote>
<p>This is a statement in the (intuitionistic) first order theory of categories with finite products and hence applies to any model of the latter.</p>
<p><em>For example</em>, taking the whole set theoretic universe as the domain of discourse gives Russel's paradox (take <span class="math-container">$A$</span> the hypothetical set of sets, <span class="math-container">$Y := \Omega := \{0,1\}$</span> and <span class="math-container">$\rho: A\times A\to\Omega$</span> the <span class="math-container">$\in$</span>-predicate) and Cantor's theorem (take <span class="math-container">$A$</span> any set and <span class="math-container">$\rho: A\times A\to \Omega$</span> corresponding to the hypothetical surjection <span class="math-container">$A\to\Omega^A$</span>). Further, the translation of the proof of Lawvere's Theorem gives the usual diagonal arguments.</p>
<blockquote>
<p><em><b>More concrete problem:</b></em></p>
<p><em>Can someone explain in detail an application of Lawvere's Theorem to partial recursive functions or the logical fixed point theorems? In particular, what categories do we need to consider there?</em></p>
</blockquote>
<p>In  D. Pavlovic, <a href="ftp://ftp.kestrel.edu/pub/papers/pavlovic/para-AML92.pdf" rel="nofollow noreferrer">On the structure of paradoxes</a>, the author considers the category freely generated by <span class="math-container">${\mathbb N}$</span> with <span class="math-container">${\text{End}}({\mathbb N})$</span> the partical recursive functions.</p>
<p>Unfortunately, I don't understand what this means.</p>
<p>For example, what should the composition law on <span class="math-container">$\text{End}({\mathbb N})$</span> be? Composition of partial recursive functions? After all, it is said that Lawvere's theorem applies with <span class="math-container">$A=Y={\mathbb N}$</span>, so that in particular any morphism <span class="math-container">${\mathbb N}\to{\mathbb N}$</span> should have a fixed point <span class="math-container">$1\to {\mathbb N}$</span>. If the endomorphisms are indeed just partial recursive functions and if composition means composition of functions, this seems odd - if points <span class="math-container">$1\to {\mathbb N}$</span> are just elements of <span class="math-container">${\mathbb N}$</span>, then the claim is wrong, and if a morphism <span class="math-container">$1\to {\mathbb N}$</span> is only a partial function, too, hence can  be undefined, the fixed point theorem is trivial.</p>
<p>What is the category one really wants to consider?</p>
<p>Maybe the goal is to get Roger's fixed point theorem, but then one should somehow build a coding of partial recursive functions by natural numbers into the definition of the category, and I can't figure out how to do this.</p>
<p>I'd be very happy if someone could explain the construction of a context to which Lawvere's Fixed Point Theorem applies, giving rise to a logical fixed point theorem or a fixed point theorem for partial recursive functions.</p>
<p>Thank you!</p>

CC BY-SA 3.0
2014-11-06T14:07:43.803Z
Well, the technical part of Gödel’s fixed-point theorem is to prove that recursive functions can be numerically represented in the theory, and there is no way around it, as you have to use at some point something that distinguishes, say $Q$, from various decidable theories. If you wish, you can think of it as implementation of $\lambda$-calculus in arithmetic.
Emil Jeřábek
CC BY-SA 3.0
2014-11-06T14:20:28.003Z
@EmilJeřábek: Thank you for your comment! I understand that there will be no way around a coding of recursive functions, but I'd like to separate clearly what concerns the coding and what is formal afterwards.
Hanno
CC BY-SA 3.0
2014-11-06T14:43:19.260Z
@EmilJeřábek: What I would like to understand is whether one can make rigorous the impression that the part concerning the coding gives rise some kind of model of $\lambda$-calculus through which the $Y$-combinator can be interpreted and gives rise to the various fixed point theorems.
Hanno
CC BY-SA 3.0
2014-11-12T19:10:48.467Z
The Lawvere fixed-point theorem can be relatively trivially applied to partial recursive functions considering there is a (recursive) enumeration $\varphi$ of partial recursive functions, i.e. a computable surjection $\mathbb{N}\rightarrow(\mathbb{N}\rightarrow\mathbb{N})$ in the category of partial recursive functions. The fixed-point theorem says: "every recursive *functional* (of type $(\mathbb{N}\rightarrow\mathbb{N})\rightarrow(\mathbb{N}\rightarrow\mathbb{N})$) has a fixed-point" which is exactly the $Y$ combinator.
cody
CC BY-SA 3.0
2014-11-12T20:32:53.427Z
Cody, could you elaborate precisely what category you are using, because that's the point where I can't follow the other sources.
Hanno
CC BY-SA 3.0
2014-11-14T21:39:12.753Z
@andrejbauer would probably be more suited to answer this, but you could take the category where the objects are simple types built on $\mathbb{N}$ and as arrows between $A$ and $B$ the closed terms in some turing-complete language, say [PCF](http://en.wikipedia.org/wiki/Programming_Computable_Functions), of type $A\rightarrow B$.
cody
<lo.logic><computability><lambda-calculus>
Fixed points in computability and logic
Hanno
# Fixed points in computability and logic

(Asked by: username_0 on 2014-11-04)

*This question has also been posted on Math.SE,*

*<https://math.stackexchange.com/questions/1002540/fixed-points-in-computability-nd-logic>*

*I hope it is ok to also post it here. If not, or if it is too basic for CS.SE, please tell me and I will delete it.*

---

I would like to understand better the relation between fixed point theorems in logic and $\lambda$-calculus.

***Background***

*1) The role of fixed points in incompleteness & undefinability of truth*

As far as I understand, apart from the fundamental idea of internalizing logic, the key to both the proofs of *Tarski's undefinability of truth* and *Goedel's incompleteness theorem* is the following *logical fixed point theorem*, living in a constructive, finitistic metatheory (I hope the formulation is ok, please correct me if something's incorrect or inprecise):

> **Existence of fixed points in logic**
>
> *Suppose* ${\mathscr T}$ is a sufficiently expressive, recursively enumerable theory over the language ${\mathcal L}$, and let ${\mathbf C}$ be a coding of ${\mathcal L}$-formulas in ${\mathscr T}$, that is, an algorithm turning arbitrary well-formed ${\mathcal L}$-formulas $\varphi$ into ${\mathcal L}$-formulas with one free variable ${\mathbf C}(\varphi)(v)$, such that for any ${\mathcal L}$-formula $\varphi$ we have ${\mathscr T}\vdash \exists! v: {\mathbf C}(\varphi)(v)$.
>
> *Then* there exists an algorithm ${\mathbf Y}$ turning well-formed ${\mathcal L}$-formulas in one free variable into closed well-formed ${\mathcal L}$-formulas, such that for any ${\mathcal L}$-formula in one free variable $\phi$ we have $${\mathscr T}\vdash {\mathbf Y}(\phi)\Leftrightarrow \exists v: {\mathbf C}({\mathbf Y}(\phi))(v)\wedge \phi(v),$$ which, interpreting ${\mathbf C}$ as a defined function symbol $\lceil -\rceil$, might also be written more compactly as$${\mathscr T}\vdash {\mathbf Y}(\phi)\Leftrightarrow \phi(\lceil{\mathbf Y}(\phi)\rceil).$$
>
> In other words, ${\mathbf Y}$ is an algorithm for the construction of fixed points with respect to ${\mathscr T}$-equivalence of one-variable ${\mathcal L}$-formulas.

This has at least two applications:

* Applying it to the predicate $\phi(v)$ expressing "$v$ codes a sentence which, when instantiated with its own coding, is not provable." yields the formalization of "This sentence is not provable" which lies at the heart of Goedel's argument.
* Applying it to $\neg\phi$ for an arbitrary sentence $\phi$ yields Tarski's undefinability of truth.

*2) Fixed points in untyped $\lambda$-calculus*

In untyped $\lambda$-calculus the construction of fixed points is important in the realization of recursive functions.

> **Existence of fixed points in $\lambda$-calculus:**
>
> There is a *fixed point combinator*, i.e. a $\lambda$-term $Y$ such that for any $\lambda$-term $f$, we have $$f(Y f)\sim\_{\alpha\beta} Yf.$$

***Observation***

What leaves me stunned is that the fixed point combinator $\lambda f.(\lambda x. f(x x))(\lambda x. f(x x))$ in $\lambda$-calculus directly reflects, in a very clean and nontechnical way, the usual proof of the logical fixed point theorem:

*Very roughly*, given a formula $\varphi$, one considers the formalization $\varphi(v)$ of the statement "$v$ codes a sentence which, when instantiated with itself, satisfies $\phi$", and puts ${\mathbf A}(\phi) := \varphi(\lceil\varphi\rceil)$. The sentence $\varphi(v)$ is like $\lambda x. f(x x)$, and $\varphi(\lceil\varphi\rceil)$ corresponds to $(\lambda x. f(x x))(\lambda x. f(x x))$.

***Question***

Despite its quickly described idea, I found the proof of the logical fixed point theorem quite technical and difficult to carry out in all details; Kunen does so for example in Theorem 14.2 of his 'Set Theory' book. On the other hand, the $Y$-combinator in $\lambda$-calculus is very simple and its properties are easily verified.

> *Does the logical fixed point theorem follow rigorously from fixed point combinators in $\lambda$-calculus?*
>
> E.g., can one model the $\lambda$-calculus by ${\mathcal L}$-formulas up to logical equivalence, so that the interpretation of any fixed point combinator gives an algorithm as described in the logical fixed point theorem?

---

***Edit***

In view of the many other instances of the same diagonalization argument described in Martin's and Cody's answers, one should rephrase the question:

> *Is there a common generalization of the diagonalization arguments following the principle expressed in the $Y$-combinator? $$\lambda f.(\lambda x. f(xx))(\lambda x.f(xx))$$*

If I understand it correctly one proposal is *Lawvere's Fixed Point Theorem*, see below. Unfortunately however I can't follow the relevant specializations in either of the articles that Martin cited in his answer, and I'd be happy if someone could explain them. First, for completeness:

> ***Lawvere's Fixed Point Theorem***
>
> Let ${\mathscr C}$ be a category with finite products and $\varphi: A\times A\to Y$ such that for any morphism $f: A\to Y$ in ${\mathscr C}$ there is some $\lceil f\rceil: 1\to A$ such that for all points $p: 1\to A$ one has $$1\xrightarrow{p} A\xrightarrow{\ f\ } Y\ \ =\ \ 1\xrightarrow{p} A\xrightarrow{\langle \lceil f\rceil,\text{id}\_A\rangle} A\times A\xrightarrow{\varphi} Y.$$
>
> Then for any endomorphism $g: Y\to Y$, putting $$f\ :=\ A\xrightarrow{\Delta} A\times A\xrightarrow{\varphi} Y\xrightarrow{g} Y,$$ any choice of $\lceil f\rceil$ gives rise to a fixed point of $g$, namely
> $$1\xrightarrow{\langle\lceil f\rceil,\lceil f\rceil\rangle} A\times A\xrightarrow{\varphi} Y.$$

This is a statement in the (intuitionistic) first order theory of categories with finite products and hence applies to any model of the latter.

*For example*, taking the whole set theoretic universe as the domain of discourse gives Russel's paradox (take $A$ the hypothetical set of sets, $Y := \Omega := \{0,1\}$ and $\rho: A\times A\to\Omega$ the $\in$-predicate) and Cantor's theorem (take $A$ any set and $\rho: A\times A\to \Omega$ corresponding to the hypothetical surjection $A\to\Omega^A$). Further, the translation of the proof of Lawvere's Theorem gives the usual diagonal arguments.

> ***More concrete problem:***
>
> *Can someone explain in detail an application of Lawvere's Theorem to partial recursive functions or the logical fixed point theorems? In particular, what categories do we need to consider there?*

In D. Pavlovic, [On the structure of paradoxes](ftp://ftp.kestrel.edu/pub/papers/pavlovic/para-AML92.pdf), the author considers the category freely generated by ${\mathbb N}$ with ${\text{End}}({\mathbb N})$ the partical recursive functions.

Unfortunately, I don't understand what this means.

For example, what should the composition law on $\text{End}({\mathbb N})$ be? Composition of partial recursive functions? After all, it is said that Lawvere's theorem applies with $A=Y={\mathbb N}$, so that in particular any morphism ${\mathbb N}\to{\mathbb N}$ should have a fixed point $1\to {\mathbb N}$. If the endomorphisms are indeed just partial recursive functions and if composition means composition of functions, this seems odd - if points $1\to {\mathbb N}$ are just elements of ${\mathbb N}$, then the claim is wrong, and if a morphism $1\to {\mathbb N}$ is only a partial function, too, hence can be undefined, the fixed point theorem is trivial.

What is the category one really wants to consider?

Maybe the goal is to get Roger's fixed point theorem, but then one should somehow build a coding of partial recursive functions by natural numbers into the definition of the category, and I can't figure out how to do this.

I'd be very happy if someone could explain the construction of a context to which Lawvere's Fixed Point Theorem applies, giving rise to a logical fixed point theorem or a fixed point theorem for partial recursive functions.

Thank you!

**Tags:** lo.logic, computability, lambda-calculus
> **Comments:**
> **username_1**: Well, the technical part of Gödel’s fixed-point theorem is to prove that recursive functions can be numerically represented in the theory, and there is no way around it, as you have to use at some point something that distinguishes, say $Q$, from various decidable theories. If you wish, you can think of it as implementation of $\lambda$-calculus in arithmetic.  
> **username_0**: @EmilJeřábek: Thank you for your comment! I understand that there will be no way around a coding of recursive functions, but I'd like to separate clearly what concerns the coding and what is formal afterwards.  
> **username_0**: @EmilJeřábek: What I would like to understand is whether one can make rigorous the impression that the part concerning the coding gives rise some kind of model of $\lambda$-calculus through which the $Y$-combinator can be interpreted and gives rise to the various fixed point theorems.  
> **username_2**: The Lawvere fixed-point theorem can be relatively trivially applied to partial recursive functions considering there is a (recursive) enumeration $\varphi$ of partial recursive functions, i.e. a computable surjection $\mathbb{N}\rightarrow(\mathbb{N}\rightarrow\mathbb{N})$ in the category of partial recursive functions. The fixed-point theorem says: "every recursive *functional* (of type $(\mathbb{N}\rightarrow\mathbb{N})\rightarrow(\mathbb{N}\rightarrow\mathbb{N})$) has a fixed-point" which is exactly the $Y$ combinator.  
> **username_0**: Cody, could you elaborate precisely what category you are using, because that's the point where I can't follow the other sources.  
> **username_2**: @andrejbauer would probably be more suited to answer this, but you could take the category where the objects are simple types built on $\mathbb{N}$ and as arrows between $A$ and $B$ the closed terms in some turing-complete language, say [PCF](http://en.wikipedia.org/wiki/Programming_Computable_Functions), of type $A\rightarrow B$.  

---

## 2 answers

### Answer by username_3 on 2014-11-04. Score: 7

I'm probably not directly answering your question, but there is a common mathematical generalisation of a lot of paradoxa, including Gödel's theorems and the Y-combinator.
I think this was first explored by Lawvere. See also [2, 3].

1. F. W. Lawvere, [Diagonal arguments and cartesian closed categories](http://www.tac.mta.ca/tac/reprints/articles/15/tr15.pdf).
2. D. Pavlovic, [On the structure of paradoxes](ftp://ftp.kestrel.edu/pub/papers/pavlovic/para-AML92.pdf).
3. N. S. Yanofsky, [A Universal Approach to Self-Referential Paradoxes,
   Incompleteness and Fixed Points](http://arxiv.org/pdf/math/0305282.pdf).

> **Comments:**
> **username_0**: Thank you, Martin, these are very interesting references! I'm having trouble however to extract from the logical situation a categorical context to which Lawvere's logical fixed point theorem applies verbatimly. In Yanofsky's article, for example, I doubt that the substitution operation $\text{Lind}^1\times\text{Lind}^1\to\text{Lind}^0$ is well-defined if one considers terms up to logical equivalence. Do you understand this?  
> **username_3**: @HannoBecker This may be quite difficult and sensitive to coding.  

---

### Answer by username_2 on 2014-11-04. Score: 5

I don't have a complete answer to your question, but I do have this:

As per [Wikipedia](http://en.wikipedia.org/wiki/Kleene%27s_recursion_theorem#Kleene.27s_second_recursion_theorem) says

> For every partial recursive function $Q(x, y)$ there exists an index $p$ such that
> $$ \varphi\_p\simeq \lambda y.Q(p, y)$$
> where $\varphi$ is a bijection between $\mathbb{N}$ and the partial recursive functions.

Now it's pretty clear that this theorem is a consequence of the fix-point theorem in the $\lambda$-calculus. We can use this to prove a *variant* of the logical-fixed point theorem:

> For every formula $\phi$ and r.e. theory ${\mathscr T}$ containing arithmetic, there exists an index $n$ such that
> $${\mathscr T}\vdash \phi(\overline{n}) \Leftrightarrow {\mathscr T}\vdash \exists y, \varphi\_n(y)=0$$

This isn't quite what you want, but an internalization trick can give you the stronger statement

> ${\mathscr T}\vdash \phi(\overline{n})\leftrightarrow \exists y, \varphi\_n(y) = 0$

Now again, this is not quite the logical fixed-point theorem, but it can serve the same purpose.

> **Proof:**
> Define $Q(x,y)$ to be the recursive function defined by
> $$Q(x,y) = 0 \mbox{ iff }{\mathscr T}\vdash \phi(\overline{x})\mbox{ in at most $y$ steps} $$
> It is easy to see that $Q$ is (total) recursive. Note that $\exists y, Q(x, y)$ expresses the fact "${\mathscr T}$ proves $\phi(\overline{x})$", and that this is true iff ${\mathscr T}\vdash\exists y,Q(\overline{x}, y)$ (we are assuming $\omega$-consistency). Now a simple application of the Kleene Recursion Theorem on $Q$ gives us the desired conclusion. $\square$

With a little thought, you can probably strengthen this argument to give you the full theorem directly without the internalization.

> **Comments:**
> **username_0**: Thank you for your answer! Let me go slowly to see if I understand you: In your first statement, can $\varphi:{\mathbb N}\cong\text{C}({\mathbb N},{\mathbb N})$ be completely arbitrary, or do you at least want the induced Currying map $$\text{C}({\mathbb N}^2,{\mathbb N})\to\text{Map}({\mathbb N},\text{C}({\mathbb N},{\mathbb N}))\cong\text{Map}({\mathbb N},{\mathbb N})$$ to have image in the partial recursive functions $\text{C}({\mathbb N},{\mathbb N})$, and that the induced evaluation ${\mathbb N}^2\to{\mathbb N}$, $(n,m)\mapsto\varphi(n)(m)$ be computable?  
> **username_0**: With these assumptions, I understand the statement is true; however, though - as in many of these types of statements - the *similarity* with the $Y$-combinator in $\lambda$-calculus is striking, I do not see how you would make it a *formal consequence* of the latter. Could you elaborate?  
> **username_2**: For the first point: you are correct, you want $\varphi$ to be "sane" in the sense you describe. For the second point: the $Y$ combinator essentially expresses $Y\ f\simeq f(Y\ f)$. The recursion theorem says essentially the same thing: take $p:= Y\ Q$. However, the theory of partial recursive functions allows for slightly more generality: the *code* of a function is distinct from the function itself. The equivalent in $\lambda$-calculus would be having a ``quote`` and ``eval`` operation as in Lisp. In this sense, the recursion theorem is more general than the existence of the $Y$ combinator.  

---

