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/… – David Roberts Jun 5 '13 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, – Theo Johnson-Freyd Jun 5 '13 at 6:56
• Or at least, spell Gödel's name correctly... – Zhen Lin Jun 5 '13 at 7:27
• These are fair points. @Bauer: I did mean qualifier not quantifier, as an adjective qualifies. – Mozibur Ullah Jun 5 '13 at 11:03
• arxiv.org/abs/math/0305282 – uhbif19 Mar 26 '15 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! – Mozibur Ullah Jun 5 '13 at 12:27

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.

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. – Mozibur Ullah Jun 15 '13 at 0:56