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?

  • 1
    $\begingroup$ 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/… $\endgroup$
    – David Roberts
    Jun 5, 2013 at 5:06
  • 2
    $\begingroup$ 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, $\endgroup$ Jun 5, 2013 at 6:56
  • 4
    $\begingroup$ Or at least, spell Gödel's name correctly... $\endgroup$
    – Zhen Lin
    Jun 5, 2013 at 7:27
  • 1
    $\begingroup$ These are fair points. @Bauer: I did mean qualifier not quantifier, as an adjective qualifies. $\endgroup$ Jun 5, 2013 at 11:03
  • 2
    $\begingroup$ arxiv.org/abs/math/0305282 $\endgroup$
    – uhbif19
    Mar 26, 2015 at 22:51

4 Answers 4


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.

  • 1
    $\begingroup$ Your assumption is correct, this is close to what I was looking for! $\endgroup$ Jun 5, 2013 at 12:27
  • 3
    $\begingroup$ 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 $\endgroup$ 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.

  • $\begingroup$ I think thats only a categorical formulation of the diagonal lemma there. $\endgroup$ 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}$.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.