research36 min studyLesson 978 in Mathematics

Representability and first incompleteness

Construct the diagonal sentence and separate Gödel’s original hypothesis from Rosser’s improvement.

Before you begin

On this page

The question for today

What you’ll understand

Distinguish numeralwise representability from unrestricted semantic truth.
Derive the diagonal fixed-point equivalence with effective substitution.
State the exact consistency assumptions for Gödel and Rosser incompleteness.

Arithmetic can describe finite calculations about its own syntax once the coding operations are represented inside it. This does not give arithmetic an unrestricted truth predicate. It does let a sentence assert that its own code has no proof. The resulting argument has precise effectiveness and consistency assumptions. We will isolate the formal fixed-point mechanism, prove the unprovability direction, and explain why the opposite direction needs extra care unless one uses Rosser’s modified sentence.

Represent concrete computations before making internal claims

Robinson arithmetic Q is a fixed finite theory of zero, successor, addition, and multiplication strong enough to represent computable finite syntactic operations. For a decidable relation, numeralwise representation means true concrete instances are provable and false concrete instances have provable negations, using the numerals for the actual inputs. For a represented total function, concrete input numerals determine the correct output uniquely in the specified representing formula. This does not mean Q proves every universal totality statement about that function.

Let T be a consistent c.e. extension of Q in an effective arithmetic language. Use a standard certified finite proof predicate, including axiom-enumeration witnesses when needed. Its numeralwise correctness permits checking any actual proof code internally. Provability is the existential assertion that some such code exists. Distinguish this formula from semantic truth in the standard natural numbers, and distinguish the external assertion that T is consistent from an internal arithmetic sentence intended to express that assertion.

\operatorname{Prov}_T(z)\equiv\exists p\,\operatorname{Prf}_T(p,z),\qquad T\supseteq Q.

The proof predicate describes certified finite syntactic evidence; it is not a predicate for all arithmetic truth.↔ Scroll wide equations horizontally.

Diagonal substitution creates a fixed point without literal self-quotation

For each one-free-variable formula theta, the diagonal lemma constructs a sentence G such that Q proves G equivalent to theta applied to the numeral for G's code. The construction uses the computable substitution operation: given a formula code x, substitute its own numeral into its designated free variable. Since Q represents that operation, the apparently self-referential sentence is produced by ordinary finite coding and substitution. Printed quotation marks alone would not establish this formal equivalence.

Choose theta to deny T-provability. Then T proves that G is equivalent to its own unprovability. If T actually proved G, its finite proof would yield a numeral instance of the proof predicate, hence T would prove its provability as well. The equivalence would then give both provability and its negation inside T, contradicting consistency. This direction requires no assumption that every theorem of T is true in the intended standard model.

Q\vdash G\leftrightarrow\neg\operatorname{Prov}_T(\ulcorner G\urcorner),\qquad\operatorname{Con}(T)\text{ externally }\Longrightarrow T\nvdash G.

The corner notation stands for the numeral coding the displayed sentence, under the fixed effective encoding.↔ Scroll wide equations horizontally.

Negating the Gödel sentence needs a stronger hypothesis

For the ordinary Gödel sentence just constructed, consistency alone establishes unprovability of G. Gödel's original argument rules out a proof of its negation using omega-consistency: T must not prove an existential assertion while refuting every standard numeral instance. A suitable Sigma-one soundness assumption also suffices for the usual Sigma-one provability predicate. These are stronger assumptions than plain syntactic consistency, and must not be silently attached to every consistent theory.

Rosser changes the proof-comparison sentence and obtains an independent sentence for every consistent c.e. extension of Q, without omega-consistency. His sentence compares a proposed proof with earlier codes of proofs of its negation; finite comparisons replace the stronger global assumption. This is the Gödel–Rosser theorem, cited here rather than fully proved. The theorem concerns effective sufficiently expressive theories: complete true arithmetic is not a counterexample because its axioms are not c.e., and weak decidable theories need not represent the required syntax.

T\text{ consistent, c.e., }T\supseteq Q\ \Longrightarrow\ \exists R\ (T\nvdash R\ \land\ T\nvdash\neg R).

Rosser’s conclusion uses a modified sentence R; it must not be attributed automatically to the ordinary G under consistency alone.↔ Scroll wide equations horizontally.

Work it through

Construct a diagonal denial and prove its unprovability

Let d(x) be the code obtained by substituting numeral x into the designated variable of the formula coded by x, with a harmless default on malformed codes. Use represented substitution to build a Gödel sentence and prove that a consistent T cannot prove it.

Write beta(x) to express $\neg\operatorname{Prov}_T(d(x))$ , eliminating d as a function abbreviation through its representing formula. Let k be beta's code and let G be beta evaluated at numeral k. By construction the code of G is d(k).
Representability of the concrete substitution computation proves in Q that evaluating d at numeral k gives numeral d(k). Substituting that result into beta yields $Q\vdash G\leftrightarrow\neg\operatorname{Prov}_T(\ulcorner G\urcorner)$ . This is a finite fixed-point construction, not a truth assertion about arbitrary strings.
Suppose T proves G with actual certified proof code p. Numeralwise proof checking gives $Q\vdash\operatorname{Prf}_T(\bar p,\ulcorner G\urcorner)$ , hence T proves Prov of G. But T also proves its negation using G and the fixed-point equivalence. Consistency excludes this pair, so T cannot prove G.

\ulcorner G\urcorner=d(k),\qquad T\vdash G\ \Longrightarrow\ T\vdash\operatorname{Prov}_T(\ulcorner G\urcorner)\land\neg\operatorname{Prov}_T(\ulcorner G\urcorner).

The contradiction is internal to T, while the assumption that T is consistent is made externally.↔ Scroll wide equations horizontally.

The result

The ordinary Gödel sentence is unprovable in any consistent c.e. extension of Q. Independence of this same sentence requires a stronger assumption on the opposite direction.

The living notebook

Explore the model

Interactive lab

Interactive lab · modular

Check every transition of a finite certificate

Pause and Reset, set modulus 9 and step 4, then take four Steps. The prefix is 0,4,8,3,7; check each local addition modulo nine. Reset for a fresh comparison and set both modulus 9 and step 3; the prefix becomes 0,3,6,0,3. Each finite prefix can be encoded and verified, but the lab neither constructs a Gödel sentence nor decides whether any arithmetic sentence has a proof. Each Step is one addition; editing retains time, so Reset before each comparison.

Additive orbitCurrent residue / next edge

Residue r0: 0
Orbit period · m/gcd(m,a): 12
Distinct residues visited: 1 of 12

Modulus m12Additive step a5

t = 0 s

Addition modulo m starts at zero: rₙ = na mod m. Playback advances two additions per second. The orbit has period m/gcd(m,a), including period one for a = 0. This is not a cryptographic security test or a primality algorithm. Parameter changes pause playback and recompute the model at the current elapsed time. Reset restores both parameters and returns time to zero. Playback starts paused. Adjust either parameter, then choose Play or Step.

Look forFinite syntactic verification is the effective ingredient used by arithmetization; incompleteness requires an additional formal argument.

Pause & reason

Check your understanding

Interactive checks need JavaScript. You can still read the explanation.

Read the checkpoint explanation

The distinction is between a complete calculus and a complete theory, and between Gödel’s ordinary sentence and Rosser’s modified one. Plain consistency does not imply standard-model soundness.

Your turn

Try it yourself

Assume T is consistent but suppose it proves $\neg G$ for the ordinary Gödel sentence. Show why T then exhibits omega-inconsistency. Identify which claims are about actual finite proof codes and which are internal quantifiers.

Take a moment to make a prediction or work it out on paper. Open a hint when you need one.

Give me a hint

The earlier consistency argument rules out any actual T-proof of G. Examine each standard numeral instance of the certified proof predicate separately.

Compare with the solution

There is no actual certified proof of G. For every standard natural n, numeralwise checking therefore gives $T\vdash\neg\operatorname{Prf}_T(\bar n,\ulcorner G\urcorner)$ . On the other hand the fixed-point equivalence and the assumed proof of not-G give $T\vdash\exists p\operatorname{Prf}_T(p,\ulcorner G\urcorner)$ . Thus T asserts an existential witness while refuting each standard numeral instance, exactly the prohibited omega-inconsistent pattern. The existential quantifier is internal to T; no standard proof code has been exhibited.

Keep the idea

Take it with you

Representing concrete syntax does not supply an unrestricted arithmetic truth predicate.
The diagonal lemma uses computable substitution and represented finite calculations.
Gödel’s ordinary sentence and Rosser’s modified sentence have different consistency requirements.

Read further

Original sources and deeper explanations to follow at your own pace.

Optional progress, saved in this browser when available. Revisit any lesson at any time.

Lesson not marked complete.