# Godel's Diagonalization Lemma As Application Of Lawvere's Fixed Point Theorem

I've read through this paper with applications of Lawvere's fixed point theorem. On the diagonalization lemma, they say the following:  For one thing, how can $$f$$ and $$\Phi_{\cal E}$$ be well defined maps? As far as I understand, the Lindenbaum algebras contain all FO formulas in the language of some theory $$S$$, modulo $$S$$-equivalence (logical equivalence proveable from $$S$$). And this also makes sense, since the fixed point we ought to find is only fixed modulo $$S$$-equivalence, but I don't see $$f$$ and $$\Phi_{\cal E}$$ factorizing through $$S$$-equivalence.

Also, am I right to interpret the arrows here not as algebra homomorphisms but set functions?

Here's what I've tried so far to save the proof:

• First I define $$\ulcorner\phi\urcorner_S$$ to be the smallest number $$n$$ such that $$S\vdash\phi\longleftrightarrow\llcorner n\lrcorner$$

• Then I show that the diagonalization lemma $$\forall{\cal E}\in\text{Lind}^1_S.\exists{\cal C}\in\text{Lind}^0_S.S\vdash{\cal C}\longleftrightarrow{\cal E}(\ulcorner{\cal C}\urcorner)$$ is weaker than its variant using $$\ulcorner\cdot\urcorner_S$$ instead of $$\ulcorner\cdot\urcorner$$.

• I define $$f'$$ and $$\Phi'_{\cal E}$$ as the $$\ulcorner\cdot\urcorner_S$$-variants of $$f$$ and $$\Phi_{\cal E}$$ respectively.

• Then I show that $$f'$$ and $$\Phi'_{\cal E}$$ factorize through $$S$$-equivalence and that $$\Phi'_{\cal E}\circ f'\circ\Delta$$ can be encoded over $$f'$$, i.e. there exists $$[\phi]\in\text{Lind}^1_S$$ such that $$\Phi'_{\cal E}\circ f'\circ\Delta=f'\circ({\sf id}\times{\sf c}_{[\phi]})$$ (where $${\sf c}_x$$ denotes the constant map to $$x$$).

At this point I can safely apply Lawvere's fixed point theorem to get the $$\ulcorner\cdot\urcorner_S$$- variant of Godel's diagonalization lemma.

[EDIT] Let's say we want to prove the diagonalization lemma over some theory $$T$$ in a (possibly weaker) theory $$S$$. Intuitively it seems to me that very weak $$S$$ (Weaker than PA) might not prove the $$\ulcorner\cdot\urcorner_T$$-version of the lemma. Since I feel that for the original lemma I only need to formulate the halting problem (will program $$n$$ on input $$m$$ halt) but for the $$\ulcorner\cdot\urcorner_T$$-version I might need to formulate something like what is the smallest $$m$$ such that program $$n$$ halts on $$m$$. Could there be some truth to this?

• As far as I can tell, you are correct that $f$ and $\Phi_\mathcal{E}$ are not well-defined functions. – Derek Elkins Sep 19 '17 at 9:10
• The non category theory was of doing this is to define $S(,)$ as $$S(\ulcorner P() \lrcorner,~ x) = \ulcorner P(x) \lrcorner$$ (only defined for a predicate $A$ with a single free variable), and $B()$ as $$B(x) = A(S(x, x))$$ Then $D = B(\ulcorner B(x) \lrcorner) = A(S(\ulcorner B(x) \lrcorner, \ulcorner B(x) \lrcorner) = A(\ulcorner B(\ulcorner B(x) \lrcorner) \lrcorner) = A(\ulcorner D \lrcorner)$  Your $f(x, y)$ is $S(y, x)$ – DanielV Sep 19 '17 at 13:29
• But I want to do it the category theory way :) – fweth Sep 19 '17 at 13:40
• Would it be appropriate to email the author my suggestions? I've never done this before... – fweth Sep 20 '17 at 17:12
• – Hanno May 12 at 8:49