Gödel, Rosser, and Incompleteness

The completeness theorem establishes that first-order proof rules can capture semantic consequence. Every sentence true in all models of a theory is derivable from its axioms. It does not establish that the axioms decide every sentence.

Gödel's 1931 incompleteness theorem concerns that second question. Under suitable hypotheses, a theory of arithmetic cannot prove or refute every sentence in its language. Its strength is part of the reason: arithmetic can represent enough of the operations on expressions to make statements about formal proofs.

The argument is not a paradox caused by using an ambiguous sentence. It constructs an ordinary arithmetical formula by explicit syntactic methods.

Which theories are covered?

A standard modern formulation says that every consistent, computably enumerable theory extending a suitable elementary arithmetic is incomplete.

Each qualification matters.

The theory must be consistent: it cannot derive a contradiction. Its axioms must be effectively enumerable, so there is a mechanical way to generate them. And it must express enough arithmetic to represent the elementary computations used in coding syntax.

Peano arithmetic is a familiar example of the relevant strength. Very weak logical theories need not meet the arithmetic condition. The theory of the natural numbers with addition alone, studied by Presburger, is decidable and complete.

The complete theory $\operatorname{Th}(\mathbb N)$, consisting of every first-order truth about the standard natural numbers, is also a useful comparison. It is complete by definition. It escapes the theorem because its axioms cannot be effectively enumerated.

The incompleteness result therefore concerns a particular combination of effectiveness, consistency, and expressive strength. Removing the hypotheses changes the question.

Encoding expressions by numbers

A finite alphabet can be assigned positive integer codes. A finite sequence of codes

can then be encoded, for example, by

where $p_k$ is the corresponding prime. The exact coding is unimportant provided the relevant operations can be carried out effectively.

Formulas and proofs are finite arrangements of symbols, so they can receive numerical codes. Questions such as “Is this a well-formed formula?” and “Does this line follow from these earlier lines by a specified rule?” become questions about natural numbers.

For a suitably presented theory $T$, one obtains a relation

meaning that $p$ codes a proof in $T$ of the formula coded by $n$.

If the axioms are only computably enumerable rather than immediately decidable, proof certificates can include evidence of the stage at which an axiom was enumerated. The relation used for checking these enriched finite certificates can still be made effective in the required manner.

The key step is representability: the relevant coding relations can themselves be expressed by formulas of arithmetic. Arithmetic can consequently talk about proofs without introducing a new primitive object called “a proof.”

Provability is an arithmetical predicate

Define

This expresses that a proof of the sentence with code $n$ exists. The quantifier ranges over numbers; the numbers are being interpreted as possible codes.

The predicate is not an unrestricted truth predicate. It concerns whether a finite derivation exists in one specified formal system. A sentence can be true in the standard natural numbers without being provable in that system.

It is also necessary to distinguish an external statement that $T$ proves $A$ from the internal arithmetical formula saying that $A$ is provable. The relation between them depends on the chosen coding and on the arithmetic available in $T$.

Confusing those levels can make the incompleteness argument look either trivial or contradictory. Its force comes from carefully connecting them, not from treating them as the same relation.

How the diagonal lemma produces self-reference

Let $F(x)$ be a formula with one free numerical variable. The diagonal lemma produces a sentence $G$ such that an appropriate arithmetic proves

where $\ulcorner G\urcorner$ is a numeral for the code of $G$.

The mechanism is syntactic substitution. There is an effective function that takes the code of a one-variable formula and returns the code of the sentence obtained by substituting the formula's own code into its free position.

Using a formula representing that substitution function, define a new formula that applies $F$ to the result of self-substitution. Substitute the code of this new formula into itself. The resulting sentence is $G$. The representability of substitution proves that its argument is exactly the code of $G$.

This sketch omits the bookkeeping needed to express the coding function in the chosen arithmetic, but identifies the mathematical operation that makes the construction work. It is not an appeal to an English sentence mysteriously able to refer to itself.

Taking

gives a Gödel sentence satisfying

The sentence has been built to express its own unprovability in $T$.

Why the Gödel sentence cannot be proved

Suppose $T$ proved $G$. There would then be a particular finite proof, with a particular numerical code $p$.

The elementary arithmetic of proof checking allows $T$ to verify that this code is a proof of $G$, and hence to prove

But the fixed-point equivalence and the assumed proof of $G$ also give

Thus $T$ would be inconsistent. Under consistency, $G$ is not provable.

In the standard natural-number interpretation of the coding, this means that no actual finite proof of $G$ exists. The fixed-point construction then explains the familiar assertion that $G$ is true but unprovable, subject to the stated assumptions and interpretation.

That phrase should not replace the proof. The important content lies in effectiveness, representability, and the carefully specified provability predicate.

Why Rosser's refinement matters

Showing that $T$ cannot prove $G$ is not yet enough to show that $G$ is undecidable in $T$. One must also exclude a proof of $\neg G$.

Gödel's original argument used omega-consistency. Informally, omega-consistency excludes a theory that proves an existential numerical assertion while proving, for each standard numeral separately, that it is not a witness.

In the present setting, a proof of $\neg G$ would yield the assertion that some proof of $G$ exists. Yet consistency allows the theory to reject each particular standard number as such a proof. Omega-consistency rules out this combination.

In 1936, J. Barkley Rosser modified the self-referential sentence so that ordinary consistency suffices. His construction compares proofs of a sentence with sufficiently short proofs of its negation. The finite comparison provides leverage in both directions without requiring Gödel's stronger original hypothesis.

It is therefore appropriate to distinguish “Gödel's 1931 theorem” from the common modern formulation using only consistency. The latter incorporates Rosser's refinement.

The second incompleteness theorem

The second theorem concerns the internal statement

For an appropriately strong, consistent, effectively axiomatized theory equipped with its standard provability predicate, $T$ does not prove this sentence.

The argument requires more than the first theorem's informal interpretation. The theory must be able to formalize enough reasoning about its own proofs. Standard derivability conditions describe how the provability predicate interacts with theorems, implication, and iterated provability.

For example, it must support an internal version of the fact that proofs of $A\to B$ and $A$ can be combined into a proof of $B$. Later work by Hilbert, Bernays, and Löb clarified this internal analysis.

Under the standard conditions, the theory can formalize the reasoning that its own consistency implies the unprovability represented by the Gödel sentence. If $T$ proved its consistency, it would consequently prove a sentence excluded by the first theorem.

The reference to the standard consistency statement matters. An arbitrary formula labeled “consistency” need not express the same property, and unusual provability predicates require separate analysis.

What this means for Hilbert's program

If a proposed finitary consistency proof can be formalized inside $T$, then it would give an internal proof of $\operatorname{Con}(T)$. The second theorem shows why this is impossible under the relevant hypotheses.

The conclusion does not exclude relative consistency proofs. A stronger theory may prove that a weaker theory is consistent. Gentzen's analysis of arithmetic, for example, makes the strength of a transfinite-induction principle explicit.

Nor does the theorem say that every mathematical question is undecidable in every theory. Particular problems may be settled by existing axioms. Some theories are complete. Others become stronger when new axioms are added, although any resulting effective theory satisfying the hypotheses again has undecidable sentences.

Incompleteness therefore creates a continuing question about the choice and justification of principles. It does not identify one final axiom whose addition completes all effective arithmetic.

Boundaries of the result

Gödel's theorems do not by themselves prove that human reasoning exceeds every machine. Such an argument would require additional premises about human consistency, mathematical knowledge, and which formal system is being compared with which human capacities.

They also do not establish the independence of every difficult statement. The continuum hypothesis required particular model constructions; its independence does not follow merely from the existence of some undecidable sentence.

Tarski's undefinability theorem addresses a related but distinct boundary: sufficiently rich arithmetic cannot define its own full standard truth predicate in the required way. Provability and truth must remain separate even when both are studied through arithmetization.

The effectiveness condition now becomes a subject in its own right. What exactly can an algorithm compute, and how can one prove the nonexistence of an algorithm for a given task? The next note follows Church, Turing, Kleene, Post, and the development of computability theory.

Sources and further reading

• Kurt Gödel, “Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I” (1931).
• J. Barkley Rosser, “Extensions of Some Theorems of Gödel and Church” (1936).
• David Hilbert and Paul Bernays, Grundlagen der Mathematik, volume II (1939); Martin H. Löb, “Solution of a Problem of Leon Henkin” (1955).
• Alfred Tarski, the work on truth and definability collected in Logic, Semantics, Metamathematics.
• Gödel's Incompleteness Theorems, for precise hypotheses, historical formulations, and common misinterpretations.