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

Question

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?

Answer 1

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.

Answer 2

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.

Answer 3

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.

Answer 4

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}$.