10
$\begingroup$

I asked this question on CS.SE, too:

https://cstheory.stackexchange.com/questions/27322/fixed-points-in-computability-and-logic


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 viewed as a functional programming language, the construction of fixed points is of interest for 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 stunning 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?

$\endgroup$
  • $\begingroup$ If I remember correctly, one way you can think of the technical noise is that you are encoding $\lambda$-calculus into your theory. That is essentially a technical problem - there are lots of ways to do it, so the choices seem arbitrary. $\endgroup$ – Thomas Andrews Nov 2 '14 at 13:50
  • $\begingroup$ @ThomasAndrews: Ah, I guess that's precisely what I am looking for and what I would like to learn! So if you don't mind, I'd be very happy if you could detail on it or give references in an answer. $\endgroup$ – Hanno Nov 2 '14 at 13:54
  • 1
    $\begingroup$ I don’t have time to write a full answer now, but “Lawvere’s fixed point theorem” very nicely abstracts the fixed-point aspects of many fixed-point/diagonal arguments, and so helps sort these out from coding and other technical specifics. If someone else can expand on this for an answer, that would be great! $\endgroup$ – Peter LeFanu Lumsdaine Nov 4 '14 at 8:51
  • $\begingroup$ Adding to what @Peter LeFanu Lumsdaine says, you might also want to take a look at this blog post by Andrej Bauer. $\endgroup$ – Basil Nov 4 '14 at 12:19
  • $\begingroup$ Hi Hanno, send me an email. I've been working on a purely syntactic generalization of various fixed point theorems. It could be fun to chat. $\endgroup$ – Michael Wehar Nov 9 '14 at 0:00

Your Answer

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

Browse other questions tagged or ask your own question.