15
$\begingroup$

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!

$\endgroup$
  • 1
    $\begingroup$ 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. $\endgroup$ – Emil Jeřábek supports Monica Nov 6 '14 at 14:07
  • $\begingroup$ @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. $\endgroup$ – Hanno Becker Nov 6 '14 at 14:20
  • $\begingroup$ @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. $\endgroup$ – Hanno Becker Nov 6 '14 at 14:43
  • $\begingroup$ 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. $\endgroup$ – cody Nov 12 '14 at 19:10
  • $\begingroup$ Cody, could you elaborate precisely what category you are using, because that's the point where I can't follow the other sources. $\endgroup$ – Hanno Becker Nov 12 '14 at 20:32
7
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ 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? $\endgroup$ – Hanno Becker Nov 6 '14 at 11:11
  • $\begingroup$ @HannoBecker This may be quite difficult and sensitive to coding. $\endgroup$ – Martin Berger Nov 6 '14 at 11:27
5
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ 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? $\endgroup$ – Hanno Becker Nov 6 '14 at 11:04
  • $\begingroup$ 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? $\endgroup$ – Hanno Becker Nov 6 '14 at 11:05
  • $\begingroup$ 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. $\endgroup$ – cody Nov 6 '14 at 18:43

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.