Fixed points in computability and logic

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?

I would like to concur with Thomas Andrews' comment five years ago that it is essentially an encoding issue. In case you, or other readers who stumble across this post like I did, are still interested in this interesting and (in my opinion) very natural question, I am going to say a bit more than Thomas Andrews. =)

In my view, almost all modern logic texts (including Peter Smith's excellent book from which I actually first learned Godel's incompleteness theorems) fail to give the conceptually cleanest proofs. This is because traditionally Godel proved his results for a particular formal system, which is like PA, and so actually his main (and most difficult) contribution is the encoding trick (known as Godel's β)! But in fact, the incompleteness theorems hold in full generality for any practical foundational system for mathematics that we (or any sophont) have ever or can ever devise. Unfortunately, this fact is not in most expositions on the subject. For a mostly self-contained explanation of this general version and its proof, you can see this post, in which the underlying incompleteness phenomenon is cleanly and clearly abstracted away from the encoding issues.

Of course, we also wish to know precisely what those encoding issues are for each specific formal system for which we want to prove the incompleteness theorems (such as PA), and in that case we will have to use some ad-hoc argument (like Godel's β for PA).

That said, there is another aspect of your question that I want to answer, that is not addressed by merely having a computability-based proof of the general incompleteness theorems. You asked whether there is an easy rigorous way to get from a fixed-point combinator from λ-calculus to the fixed-point lemma for practical foundational systems for mathematics. The answer is yes for such systems based on FOL, and as with the incompleteness theorems this can too be cleanly abstracted away from encoding issues, but again is not found in almost all logic texts.

Firstly, we rigorously establish that adding definitorial expansion is conservative over the original FOL (first-order logic) system. Next, let $c$ be any encoding function (from finite strings to naturals in the case of PA), and construct (via Godel's β in the case of PA) a definable function $A$ such that $A(c(Q),x)$ is the code of the sentence obtained by replacing each occurrence of the parameter in the $1$-parameter sentence $Q$ by $x$ (the numeral for $x$ in the case of PA). By definitorial expansion, we can use $A$ as a function-symbol. Now take any $1$-parameter sentence $Q$. We can construct $D := ( x ↦ Q(A(x,x)) )$, which is a definable predicate that reflects the 'λ-expression' $λx.Q(x(x))$. By definitorial expansion again, we can use $D$ as a predicate-symbol. Finally, we can construct the sentence $G :≡ D(c(D))$. By definitions we have $G ≡ Q(A(c(D),c(D))) ≡ Q(c(D(c(D))))$, and hence $G$ is a fixed-point of the meta-logical map $( I ↦ Q(c(I)) )$ on sentences.

This can be easily applied to prove the incompleteness theorems. Let $Q$ be the $1$-parameter sentence such that $\mathbb{N} ⊨ Q(c(X))$ iff $X$ is not provable by the FOL-based foundational system $S$ in question. By the above, there is a sentence $G$ over $S$ such that $G ≡ Q(c(G))$ over $S$, so we are done.

More generally, you can see that this applies to any meta-logical operator on sentences of the form $( I ↦ F(c(I)) )$ where $F$ is a definable function over $S$. This can also be applied to yield the modal fixed-point lemma for provability logic, since every modal sentence with $1$ propositional parameter $I$ that only occurs under the $⬜$ is captured by a meta-logical operator of this form, since any $⬜$ enclosing an $I$ uses only the code for $I$ (even for nested $⬜$s).

The difficulty in carrying out the technical details in the typical proof of the fixed-point theorem (not only in Kunen) is partly inherent to base FOL (without definitorial expansion). As you can see above, the quantifier trickery needed in base FOL to handle application of a coded sentence to a coded term vanishes once we have definitorial expansion. When you expand what you get to eliminate definitorial expansion, you will recover the version that you find in most logic texts.

In summary, there are two aspects of encoding that can (and in my opinion should) be eliminated from the statement and proof of the incompleteness theorems so that we get at only the conceptual core of incompleteness phenomenon. The first aspect is the encoding in FOL that is needed to avoid definitorial expansion, and this aspect is not even meaningful for foundational systems that are not based on FOL. The second aspect is the encoding in arithmetical sentences and predicates needed to show that PA-like systems are incomplete, and this aspect is only needed for PA-like systems. Even in that case, it is still better to utilize the notion of "reasoning about programs" (see my first link) and reduce that to being able to manipulate finite sequences, which can then be done via Godel's β-lemma.