OCTALLIUM
home > foundations > logic

Gödel did not prove what you think he proved

by Anil Kulkarni••14 min read•FOUNDATIONS

No theorem gets borrowed more often, or returned in worse condition. Gödel's incompleteness results are invoked to show that minds outrun machines, that truth outruns science, that certainty was always an illusion. What Gödel actually proved in 1931 is narrower than any of that — and stranger, and better.

The first incompleteness theorem has three conditions, and every one of them is load-bearing. Take any formal system that is consistent, that is effectively axiomatized — meaning a mechanical procedure could list its axioms — and that contains a modest amount of arithmetic. Then there is a sentence of that system's own language which it can neither prove nor refute [1]. Not a hazy sentence about consciousness or beauty: a specific, finite statement about whole numbers, engineered to encode "this sentence is not provable here."1

Remove any condition and the theorem evaporates. An inconsistent system happily proves everything, its own Gödel sentence included. The set of all true arithmetic statements is a complete theory — but no algorithm can list its axioms, so it is not effectively axiomatized and no one can use it. Presburger arithmetic, which has addition but no multiplication, is consistent, effectively axiomatized, and provably complete. #incompleteness is not a fog that settles over all formal thought. It is a precise trade-off that switches on at a precise threshold.

Nested systems, each proving the Gödel sentence of the one inside it S3 = S2 + Con(S2) S2 = S1 + Con(S1) S1 = PA cannot decide G(S1) G(S1) provable here G(S2) provable here G(S3) → S4 … every escape opens into a larger room with its own locked door
FIG 1 Each system's Gödel sentence sits just beyond its reach and comfortably inside the next system up. Nothing here is unknowable; what is impossible is a final, all-deciding box.

True where, provable where

The pop summary — "there are true statements that can never be proved" — fails on both verbs. The Gödel sentence of Peano arithmetic is true in the standard natural numbers, and we can see that it is, by the very argument Gödel gave: if PA is consistent, then G says precisely that G is unprovable in PA, and so it is. That reasoning is itself a proof — just not one that lives inside PA. Formalize it and you get a stronger system, PA plus a statement of PA's consistency, which proves G outright. The new system has its own Gödel sentence; the next system up proves that one; the ladder never terminates.2

So nothing here is "unknowable" in the pop sense. Each Gödel sentence is unprovable in one named system and provable one rung up, at the price of assuming a little more. What the theorem forbids is a final rung: a single consistent, mechanically listable set of axioms that settles every question of arithmetic from nothing. Mathematical certainty is not destroyed. It is shown to be irreducibly relative to a starting point — a statement about #formal-systems, not about truth.

What the theorem does not license

It says nothing about human minds. The argument pressed by Lucas and later by @Penrose — we can see that the Gödel sentence is true, a machine cannot, therefore we are not machines — needs the premise that we can certify our own #consistency. The second incompleteness theorem is precisely the observation that no consistent system of the relevant kind can do that for itself, and there is no evidence that humans are the exception rather than merely the overconfident.3

And it says nothing about physics, ethics, God, or the general futility of knowledge, because none of those is an effectively axiomatized theory containing arithmetic. The conditions are not fine print to be skipped; they are the theorem. @Gödel drew a sharp boundary around one specific tool — finite lists of axioms cranked by mechanical rules — and showed that arithmetic truth will not fit inside any single instance of it. Within its actual borders, the result is as solid as mathematics gets. It is the exports that are counterfeit.

Notes

  1. "Modest" is startlingly modest. Robinson arithmetic — a system with seven axioms and no induction at all — is already enough. The proof needs just enough arithmetic to encode statements about the system as statements about numbers, the trick now called Gödel numbering, so that the system can be made to talk about itself. ↩
  2. This is not hypothetical bookkeeping. Gentzen did it concretely in 1936, proving the consistency of Peano arithmetic from outside it, using induction along a transfinite ordering known as epsilon-zero [3]. The proof is finitist in spirit everywhere except that single, carefully isolated assumption — a precise measurement of exactly how much more you have to buy. ↩
  3. Franzén's short book [2] is the definitive field guide to the theorem's misuses, written with the patience of a man who had read all of them. His test is worth keeping: if an invocation of Gödel does not specify which formal system is meant, it is decoration, not argument. ↩

References

  1. Gödel, K. (1931). "Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I." Monatshefte für Mathematik und Physik 38, 173–198. doi:10.1007/BF01700692
  2. Franzén, T. (2005). Gödel's Theorem: An Incomplete Guide to Its Use and Abuse. A K Peters.
  3. Gentzen, G. (1936). "Die Widerspruchsfreiheit der reinen Zahlentheorie." Mathematische Annalen 112, 493–565.