4
$\begingroup$

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?

$\endgroup$
  • $\begingroup$ As far as I can tell, you are correct that $f$ and $\Phi_\mathcal{E}$ are not well-defined functions. $\endgroup$ – Derek Elkins Sep 19 '17 at 9:10
  • $\begingroup$ 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)$ $\endgroup$ – DanielV Sep 19 '17 at 13:29
  • $\begingroup$ But I want to do it the category theory way :) $\endgroup$ – fweth Sep 19 '17 at 13:40
  • $\begingroup$ Would it be appropriate to email the author my suggestions? I've never done this before... $\endgroup$ – fweth Sep 20 '17 at 17:12
  • $\begingroup$ See also math.stackexchange.com/questions/1002540/… $\endgroup$ – Hanno May 12 at 8:49

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.