CALLIOPE · BCOM

This work argues that the standard popular reading of Gödel's incompleteness theorems — that they reveal "true but unprovable" statements in some system-independent metaphysical sense — conflates distinct notions of truth and obscures the deeper structural lesson. Through careful separation of formal provability, model-satisfaction, and metatheoretic commitment, the analysis shows that Gödelian incompleteness is precisely the gap between satisfaction in a chosen finite-computational interpretation and derivability within a fixed effective axiomatic theory; the phrase "true but unprovable" is legitimate only once that interpretive choice is made explicit. The work then draws a precise analogy between this structural non-closure and the uncomputability of Kolmogorov complexity, situating both results within the Kolmogorov Theory (KT) framework for algorithmic agents: just as no sufficiently rich formal system achieves complete effective closure over arithmetic, no computable agent can certify optimal compression of its environment. This perspective reframes emergence as the agent-relative discovery of compact macro-level descriptions that cannot in general be derived algorithmically from micro-level rules, and it grounds the Good Algorithmic Regulator Theorem as a permission rather than a guarantee. The broader conclusion is that mathematics, properly understood, is the open-ended artifact of finite agents extending their compressive models under irreducible incompleteness — not a closed repository of pre-existing truths.

"True but unprovable" is a sloppy slogan — here's what Gödel actually proved, and why it matters for any agent trying to model the world.

The popular version of Gödel's incompleteness theorems implies that mathematical truth floats free of all formal systems, and that Gödel somehow glimpsed it from outside. This paper pushes back on that reading carefully and without mysticism. The key move is separating three things that get conflated: provability (what a formal system can derive), model-satisfaction (what holds in a particular mathematical structure), and metatheoretic commitment (the background assumptions you bring when you pick that structure). Once you make those distinctions, "true but unprovable" stops being mysterious and becomes precise: the Gödel sentence is satisfied in the standard finite-computational model of arithmetic — the one where numbers are actual counting numbers — but not derivable within the formal system. That's a real and important gap, but it's a gap relative to a chosen interpretation, not a window onto Platonic truth.

Why does the standard model feel special, then? Because arithmetic isn't just another mathematical topic — it's the scaffolding agents use to talk about finite proofs, finite programs, and finite computation. When you ask arithmetic to play that meta-role, the standard natural numbers get privileged not by metaphysical decree but by the practical needs of finite agents checking finite proofs. Nonstandard models of arithmetic are perfectly legitimate mathematics; they just can't serve as the theory of actual finite syntax. The paper makes this concrete by pointing to proof assistants like Lean: nonstandard arithmetic can appear inside Lean as an object of study, while Lean's own kernel still checks proofs as ordinary finite strings.

The paper then draws a careful analogy to Kolmogorov complexity — the length of the shortest program that produces a given string. That quantity is uncomputable: no algorithm can certify the optimal compression of arbitrary data. The structural parallel to Gödel is exact. A formal system is like a fixed computable model class; an undecidable sentence is like a compression question the current model can't settle internally; extending the axiom system is like acquiring a new compressive hypothesis. Both results are instances of the same phenomenon: fixed effective description systems cannot achieve complete closure over the domain they describe. Solomonoff induction and AIXI — the theoretical ideals of perfect inductive inference — are uncomputable for the same reason Hilbert's program failed.

This reframes what agents actually do. They don't find the final theory; they keep extending. The Good Algorithmic Regulator Theorem (cited from Ruffini's P13) says a regulator must contain a model of what it regulates — but optimality of that model is uncertifiable. It's a permission to act, not a guarantee of correctness. Emergence fits the same picture: a macro-level description that compresses micro-level data is an empirical discovery, not something derivable algorithmically from the micro-rules. Incompleteness isn't a bug in mathematics or in agents — it's the structural condition they both operate under.

The conclusion is blunt: mathematics is the open-ended artifact of finite agents extending their compressive models, not a closed repository of pre-existing truths. Gödel didn't show that formal systems miss ghostly facts. He showed that once a system is rich enough to encode finite proof, its own proof predicate outruns its derivability. The job of an agent — mathematical or otherwise — is not to find the last theory. It's to keep compressing better.