Incompleteness theorems via Turing category
Yasha Savelyev
TL;DR
The paper reframes Gödel's incompleteness theorems through a category-theoretic lens by introducing a Turing category of Gödel encodings and defining stable computability (stably c.e. sets). It replaces classical provability conditions with a Cantor-like diagonalization argument embedded in this categorical framework, enabling explicit computable Gödel sentences for theories beyond standard definability (e.g., $Σ^{0}_{2}$). It develops decision-map machinery and a stable halting problem to establish stable incompleteness theorems, including a second-incompleteness analogue and a Penrose-inspired corollary. This approach connects computability, logic, and category theory, offering a principled first-principles route to incompleteness for undefinable theories and suggesting implications for physical processes and the foundations of computation in nature.
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ödel encodings, which might be of independent interest. In our setup, the Gödel sentence is computable explicitly by construction even for $Σ^{0} _{2}$ theories (likely extending to $Σ^{0} _{n}$). In an appendix, we study the relationship of our reframed second incompleteness theorem with arguments of Penrose.