Fixed points in computability and logic

Question

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!

Answer 1

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.

2. D. Pavlovic, On the structure of paradoxes.

3. N. S. Yanofsky, A Universal Approach to Self-Referential Paradoxes, Incompleteness and Fixed Points.

Answer 2

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

As per Wikipedia 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.