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, 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!