What Gödel Really Showed: Provability, Model-Satisfaction, and Finite Observers
★ Giulio Ruffini
★ guarantor: Giulio Ruffini · vouches for the paper per WP0084 §6
The slogan that Gödel established the existence of {true but unprovable} statements is useful only if true is qualified. This note separates four notions that are often run together: derivability in a formal theory, satisfaction in a specified model, semantic consequence over all models of a theory, and effective determination or certification by a finite observer. Incompleteness establishes limits on derivability, while algorithmic undecidability establishes limits on uniform effective determination. Neither result, by itself, establishes classical bivalence, mathematical realism, or a physical ontology of inaccessible facts. Under standard classical semantics, each sentence in a fixed structure is assigned a truth value. Constructive and intuitionistic accounts do not in general identify an unresolved proposition with a hidden Boolean value. In physics, whether an uncertifiable value assigned by an idealized infinite model is also an observer-independent fact about nature is a further realism question.
We therefore formulate the core result observer-side: no single terminating procedure determines or certifies every instance in the relevant family. The halting problem makes the asymmetry precise: halting has a finite witness; continued non-halting never supplies a final observational certificate. We revisit Tarski's definition of satisfaction, Gödel and Rosser incompleteness, Tennenbaum's theorem, and Chaitin incompleteness with their assumptions and interpretive limits made explicit. We then connect these distinctions to Kolmogorov Theory and to physical undecidability results, especially Gu et al.'s infinite periodic Ising-lattice construction. The resulting KT claim is one of non-closure for finite algorithmic observers, not a legislated ontology of inaccessible truth.
Gödel's incompleteness theorems are about the limits of formal proof, not about the existence of hidden truths — and conflating those two things causes most of the philosophical confusion.
The paper's central move is surgical: it separates four things that people routinely smear together. First, derivability — whether a statement has a finite proof in some formal system. Second, model-satisfaction — whether a statement is true in some specific mathematical structure. Third, semantic consequence — whether a statement holds in every model of a theory. Fourth, effective certification — whether a finite observer running an algorithm can actually determine the answer. These are genuinely different relations. Gödel's theorem is directly about the first. The famous phrase "true but unprovable" silently imports the second (specifically: true in the standard natural numbers, under classical semantics) and then presents that import as if it were a consequence of the theorem itself. It isn't.
Why does this matter? Because once you keep the levels separate, the philosophical conclusions change dramatically. Incompleteness doesn't establish that there's a Platonic realm of mathematical facts forever beyond human reach. It establishes something more precise and more useful: a sufficiently strong, consistent, computably axiomatized theory cannot settle every arithmetical question it can formulate. That's a structural limit on formal systems, not a metaphysical claim about inaccessible truth. Similarly, Turing's halting problem says no single terminating algorithm decides every instance of a certain family of questions. Neither result, by itself, forces you to accept classical bivalence (the idea that every proposition is either true or false, even if we can never know which). Intuitionistic mathematics, for instance, simply doesn't accept that an unresolved proposition must have a hidden Boolean value waiting to be discovered.
The paper then traces this discipline through several classical results — Tarski's definition of satisfaction, Tennenbaum's theorem (the standard natural numbers are the only countable model of Peano Arithmetic with computable arithmetic operations), and Chaitin's incompleteness (a sound formal theory can only certify complexity lower bounds up to a coding-dependent ceiling). Each result is stated with its assumptions made explicit and its philosophical overreach trimmed back. The halting problem gets particular attention because it illustrates an important asymmetry: a halting computation eventually produces a finite witness you can check; non-halting never produces a final moment of confirmation. There is no "answer at infinity" available to a finite observer — that's a semantic idealization, not an observable event.
The paper connects all of this to Kolmogorov Theory (KT), BCOM's framework for modeling finite algorithmic agents. The KT reading reframes incompleteness not as a discovery about hidden ontology but as a constitutive constraint on agents that build, compress, and extend models under finite resources. An agent can't possess a universal procedure that, for every environment in a sufficiently expressive family, constructs a model and certifies it's globally optimal — that's what uncomputability of Kolmogorov complexity means in practice. The paper also engages Gu et al.'s result on infinite periodic Ising lattices, where macroscopic observables like magnetization are undecidable from the microscopic specification. The careful reading: no uniform terminating procedure extracts those observables from every specification in the family. Whether the classically-assigned-but-uncertifiable value is also an observer-independent physical fact about nature is a separate realism question the theorem doesn't answer.
- Zenodo
- 10.5281/zenodo.21008790
- WP ID
- WP0126
- Lifecycle
- ongoing
- Visibility
- internal
- Access level
- open
- Embargo until
- —
- Priority
- —
- Collab
- closed
- Venue
- —
- DOI
- —
- Deadline
- —
- Owner
- —
- Source
- drive_legacy
- Repo path
- WP0126
- v0.2.0 (draft) · cut-versionv1.3.0 (paper-internal numbering): separates derivability, model satisfaction, semantic consequence, and effective determination; states undecidability as absence of a uniform solver rather than classical bivalence; adds halting asymmetry and the finite-witness gradient; distinguishes Goedel from Rosser; narrows Tennenbaum, Chaitin, and Gu et al. to warranted conclusions; self-contained bibliography.
- 0.1.0 (draft) · auto-run-placeholder · zenodo:21008791
