Skip to content

14.5 Extensions and Refinements

Stronger forms of incompleteness, Rosser’s improvement, Löb’s theorem, and connections to computability.

14.5 Extensions and Refinements

Gödel’s original theorems admit stronger forms and alternative formulations. These refinements clarify exactly which assumptions are needed and how incompleteness behaves across different systems.

Rosser’s Improvement

Gödel’s first theorem used a strengthened consistency assumption. Rosser showed that this can be weakened.

Instead of the original Gödel sentence, Rosser constructs a sentence RR that balances proofs of a statement and its negation.

Informally, RR says:

“if there is a proof of RR, then there is a smaller proof of ¬R¬R

This construction avoids the need for stronger assumptions such as ω\omega-consistency.

The result is:

If a system is consistent, then there exists a sentence RR such that:

⊬Rand⊬¬R \not\vdash R \quad \text{and} \quad \not\vdash ¬R

So plain consistency is enough to obtain incompleteness.

Different Formalizations of Consistency

The statement “the system is consistent” can be expressed in multiple ways.

One form is:

Con(T)¬Prov(0=1) \mathrm{Con}(T) \equiv ¬\mathrm{Prov}(\ulcorner 0 = 1 \urcorner)

Another approach encodes consistency as:

“There is no number that codes a proof of both AA and ¬A¬A

These formulations are not always equivalent inside weak systems. The second incompleteness theorem depends on choosing a formulation that the system can properly express.

This leads to the study of derivability conditions, which specify how the provability predicate must behave.

Löb’s Theorem

Löb’s theorem refines the behavior of provability.

If a system proves:

Prov(A)A \mathrm{Prov}(\ulcorner A \urcorner) \to A

then it already proves:

A A

So:

Prov(A)AA \vdash \mathrm{Prov}(\ulcorner A \urcorner) \to A \quad \Longrightarrow \quad \vdash A

This result explains why internal reasoning about provability is delicate. Statements that look like “if AA is provable, then AA is true” cannot be freely used inside the system.

Löb’s theorem is a key component in the proof of the second incompleteness theorem.

Gödel–Rosser Variants

The incompleteness phenomenon can be adapted to different logical systems.

  • weaker systems still exhibit incompleteness if they encode enough arithmetic
  • stronger systems produce more complex undecidable sentences
  • different encodings lead to different forms of self-reference

The exact boundary depends on how much arithmetic the system can represent.

Incompleteness Beyond Arithmetic

The phenomenon is not limited to number theory.

Any theory that can interpret a fragment of arithmetic inherits incompleteness.

Examples include:

  • theories of sets
  • theories of computation
  • many algebraic structures

If a theory can simulate arithmetic, then Gödel-type arguments apply.

Strengthening the Second Theorem

The second incompleteness theorem can be sharpened.

Not only can a system not prove its own consistency, it also cannot prove many related reflection principles.

For example, the system cannot prove general statements of the form:

A,(Prov(A)A) \forall A, (\mathrm{Prov}(\ulcorner A \urcorner) \to A)

This would assert that all provable statements are true inside the system, which leads to contradiction under the same reasoning as before.

Hierarchies of Reflection

Although full reflection is impossible, restricted forms are often provable.

For example, a system may prove:

  • reflection for simple formulas
  • reflection up to a certain complexity

This leads to a hierarchy of reflection principles, each increasing the strength of the system.

These hierarchies are closely studied in proof theory.

Connection to Computability

Gödel’s methods connect directly to computability theory.

The construction of undecidable sentences parallels the construction of undecidable problems, such as the halting problem.

Both rely on:

  • encoding syntax or computation as numbers
  • constructing self-referential objects
  • applying diagonalization

This shared structure explains why incompleteness and undecidability appear together.

Perspective

The refinements show that incompleteness is not fragile. It does not depend on a particular encoding or a special construction.

Instead, it appears across a wide range of systems whenever three ingredients are present:

  • arithmetic expressiveness
  • representability of syntax
  • self-reference via diagonalization

These conditions are common in formal theories. As a result, incompleteness is a general feature of formal reasoning rather than an isolated phenomenon.