Incompleteness for stably computable formal systems

TL;DR

This paper extends G"odel's incompleteness theorems to stably computably enumerable formal systems, including non-classically computable ones, with implications for the limits of formal systems modeling physical processes.

Contribution

It proves analogues of G"odel's incompleteness theorems for stably computably enumerable systems, broadening their applicability beyond classical computability.

Findings

First and second incompleteness theorems extended to non-classically computable systems.

Demonstrates that certain sets like Diophantine equations with no solutions are not computably enumerable.

Provides a sharper version of G"odel's disjunction for systems modeling physical processes.

Abstract

We prove, for stably computably enumerable formal systems, direct analogues of the first and second incompleteness theorems of G\"odel. A typical stably computably enumerable set is the set of Diophantine equations with no integer solutions, and in particular such sets are generally not computably enumerable. And so this gives the first extension of the second incompleteness theorem to non classically computable formal systems. Let's motivate this with a somewhat physical application. Let $\mathcal{H} $ be the suitable infinite time limit (stabilization in the sense of the paper) of the mathematical output of humanity, specializing to first order sentences in the language of arithmetic (for simplicity), and understood as a formal system. Suppose that all the relevant physical processes in the formation of $\mathcal{H} $ are Turing computable. Then as defined $\mathcal{H} $ may \emph{not} be computably enumerable, but it is stably computably enumerable. Thus, the classical G\"odel disjunction applied to $\mathcal{H} $ is meaningless, but applying our incompleteness theorems to $\mathcal{H} $ we then get a sharper version of G\"odel's disjunction: assume $\mathcal{H} \vdash PA$ then either $\mathcal{H} $ is not stably computably enumerable or $\mathcal{H} $ is not 1-consistent (in particular is not sound) or $\mathcal{H} $ cannot prove a certain true statement of arithmetic (and cannot disprove it if in addition $\mathcal{H} $ is 2-consistent).