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 that balances proofs of a statement and its negation.
Informally, says:
“if there is a proof of , then there is a smaller proof of ”
This construction avoids the need for stronger assumptions such as -consistency.
The result is:
If a system is consistent, then there exists a sentence such that:
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:
Another approach encodes consistency as:
“There is no number that codes a proof of both and ”
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:
then it already proves:
So:
This result explains why internal reasoning about provability is delicate. Statements that look like “if is provable, then 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:
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.