# Is there a categorical proof of Gödel's incompleteness theorem?

A significant result in set theory was shown by Cohen when he showed that the continuum hypothesis was independent of ZFC using a new technique called forcing. In Topos theory, this result has a new geometric interpretation: the sheaf for the dense topology on the poset of finite approximations on the 'impossible monic' form a new model of sets where this monic is actually there.

Now, presumably Gödel's incompleteness theorem remains valid for typed intuitionistic higher-order logic; such a logic is the internal logic of a topos.

Is there a categorical proof of Gödel's theorem in Topos theory? Does Gödel's theorem say anything geometric or throw new light on the theorem when interpreted in a topos?

• I'm guessing you mean to ask for an answer along the lines similar to the result about the completeness theorem, e.g. mathoverflow.net/questions/68335/… Jun 5, 2013 at 5:06
• Dear Mozibur, This question could be improved with some rewriting. You should provide some background, to clarify your question. You should also sharpen your question: "what does A mean for B" is very broad, and does not make a good MathOverflow question. As I'm sure you saw on mathoverflow.net/howtoask, an extremely important thing for all questions is to "do your homework", but right now your question looks like idle speculation with no homework done. I am far from an expert, but I expect there is some meat here. You won't find it as the question stands, I'm afraid. All the best, Jun 5, 2013 at 6:56
• Or at least, spell Gödel's name correctly... Jun 5, 2013 at 7:27
• These are fair points. @Bauer: I did mean qualifier not quantifier, as an adjective qualifies. Jun 5, 2013 at 11:03
• arxiv.org/abs/math/0305282 Mar 26, 2015 at 22:51

This is not exactly what you asked for but I think it's reasonably close to what you want...

The idea of recasting Gödel's results in the context of category theory has led André Joyal to develop arithmetic universes, a minimalistic category tailored for that purpose. Unfortunately, Joyal never published this as explained by Paul Taylor in this recent answer.

• Your assumption is correct, this is close to what I was looking for! Jun 5, 2013 at 12:27
• Joyal's proof (or at least a proof very much in the same spirit) has been written up last year: arxiv.org/pdf/2004.10482.pdf Apr 13, 2021 at 14:57

There is a reformulation in categorical terms of Godel's incompleteness theorem in the book "Conceptual mathematics" by Schanuel and Lawvere. There are also notes of Gromov Ergostructures, Ergodic and the Universal Learning Problem: Chapters 1, 2 where on page 16-17 he discusses "an adaptation of [Schanuel-Lawvere] argument". For both approaches the key is Cantor's diagonal argument; I do not think either mentions topos theory.

• I think thats only a categorical formulation of the diagonal lemma there. Jun 15, 2013 at 0:56

It means that higher-order intuitionistic logic with natural numbers and Heyting arithmetic cannot prove its own consistency.

I think it is hard to see from your question what sort of an answer you are expecting. Are you looking for topos-theoretic formulations of Gödel's theorems? Or the impact that the theorems have on topos theory? I can amend the answer once I understand what you are looking for.

Lawvere's fixpoint theorem generalizes the diagonal argument, and the incompleteness theorem can be taken as a special case.

The proof can be found in Frumin and Massas's Diagonal Arguments and Lawvere's Theorem. Here is a copy.

Definition: A morphism $$f: X\times X\to Y$$ is weakly point-surjective iff for every $$g: X\to Y$$, there is a $$t: 1\to X$$ such that, for all $$x: 1\to X$$: $$gx=f\langle x,t\rangle$$

Lawvere's Fixpoint Theorem:

Let $$\mathbf{C}$$ be a category with a terminal object and binary products. If $$f: X\times X\to Y$$ is weakly point-surjective, then every morphism $$\alpha: Y\to Y$$ has a fixpoint $$y: 1\to Y$$.

Consider a first-order theory $$\mathrm{T}$$. We form $$\mathbf{C}_\mathrm{T}$$ a classifying category of $$\mathrm{T}$$ in the following way:

The $$\mathbf{C}_\mathrm{T}$$-objects are generated by a sort object $$A$$ (more object if the theory is multi-sorted), and an object $$2$$.

The $$\mathbf{C}_\mathrm{T}$$-morphisms are equivalence classes of (tuples of) formulas $$A^n\to 2$$ or terms $$A^n\to A$$ of $$\mathrm{T}$$.

In particular, morphisms $$1\to 2$$ are sentences, and morphisms $$1\to A$$ are constant terms.

A theory is complete iff $$\operatorname{Hom}(1,2)=\{\top,\bot\}$$.

• Undefinability of $$\operatorname{sat}$$. Suppose that the satisfiabilty predicate is definable in $$\mathrm{T}$$: $$\vdash \operatorname{sat}(a,\ulcorner\varphi\urcorner)\leftrightarrow\varphi(a)$$ for all $$\varphi,a$$.

In categorical terms, we have a Godel encoding $$\ulcorner \urcorner: \operatorname{Hom}(A^n,2)\to \operatorname{Hom}(1,A)$$, and a formula $$\operatorname{sat}: A^2\to 2$$, such that for $$\varphi: A\to 2$$ and $$a: 1\to A$$, $$\operatorname{sat}\langle a,\ulcorner\varphi\urcorner\rangle=\varphi a$$.

But this is exactly the condition for weak point-surjectivity!

• Undefinability of $$\operatorname{truth}$$. Suppose that $$\mathrm{T}$$ has a 'truth' predicate: $$\operatorname{true}\circ\ulcorner\varphi\urcorner=\varphi$$ for all $$\varphi\in \operatorname{Hom}(1,2)$$.

Suppose that $$\mathrm{T}$$ supports 'substitution': $$\operatorname{subst}\langle a,\ulcorner\varphi\urcorner\rangle=\ulcorner\varphi(a)\urcorner$$.

Then we can define $$\operatorname{sat} := \operatorname{true}\circ \operatorname{subst}$$.

• Incomplenteness. Suppose that 'provability' is representable in $$\mathrm{T}$$: $$\mathrm{T}\vdash\varphi\iff\mathrm{T}\vdash\operatorname{prov}(\ulcorner\varphi\urcorner)$$.

If $$\mathrm{T}$$ is complete, then $$\varphi=\top$$ or $$\varphi=\bot$$.

And $$\varphi=\top\implies \operatorname{prov}(\ulcorner\varphi\urcorner)=\top$$, $$\varphi=\bot\implies \operatorname{prov}(\ulcorner\varphi\urcorner)=\bot$$.

Therefore, for all $$\varphi\in \operatorname{Hom}(1,2): \operatorname{prov}\circ\ulcorner\varphi\urcorner=\varphi$$, i.e. $$\operatorname{true}$$ is $$\operatorname{prov}$$.