Incompleteness theorems via Turing category

TL;DR

This paper reinterprets Godel's incompleteness theorems using category theory, providing a more direct diagonalization approach and explicitly computable Godel sentences for certain theories.

Contribution

It introduces a categorical framework for Godel's theorems, replacing traditional provability conditions with a diagonalization argument rooted in category theory.

Findings

Explicitly computable Godel sentences for $ ext{Sigma}^0_2$ theories

A new categorical proof of Godel's incompleteness theorems

Analysis of the connection to Penrose's arguments

Abstract

We give a reframing of Godel's first and second incompleteness theorems that applies even to some undefinable theories of arithmetic. The usual Hilbert-Bernays provability conditions and the diagonal lemma are replaced by a more direct diagonalization argument, from first principles, based in category theory and in a sense analogous to Cantor's original argument. To this end, we categorify the theory G\"odel encodings, which might be of independent interest. In our setup, the G\"odel sentence is computable explicitly by construction even for $\Sigma ^{0} _{2}$ theories (likely extending to $\Sigma ^{0} _{n}$). In an appendix, we study the relationship of our reframed second incompleteness theorem with arguments of Penrose.