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?



Is there a categorical proof of Gödel's incompleteness theorem?
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](https://mathoverflow.net/questions/126513/categories-of-recursive-functions/126782#126782).


