Advanced Theorems and Extensions
Explore related theorems including Löb's theorem, Rosser's theorem, and Tarski's undefinability theorem
Listen to summary
Advanced Theorems and Extensions
Gödel's incompleteness theorems opened the door to a rich landscape of related results in mathematical logic. In this lesson, we'll explore three fundamental extensions that deepen our understanding of the limitations of formal systems: Löb's theorem, Rosser's theorem, and Tarski's undefinability theorem.
Löb's Theorem
Löb's theorem, named after Martin Löb, provides a profound insight into provability within formal systems. It states that for any consistent theory T containing primitive recursive arithmetic:
If T proves "if T proves φ, then φ", then T proves φ.
Formally: If T ⊢ (Prov_T(⌜φ⌝) → φ), then T ⊢ φ
This theorem reveals something counterintuitive about self-reference in mathematics. It shows that within a sufficiently strong formal system, saying "if this statement is provable, then it's true" actually makes the statement provable.
The Löb Paradox
Consider the statement L: "If L is provable, then God exists." By Löb's theorem, if we can prove this conditional statement, then we can prove God exists! This paradox illustrates the subtle dangers of self-reference in formal systems.
Rosser's Theorem
Rosser's theorem, developed by J. Barkley Rosser, strengthens Gödel's first incompleteness theorem by removing the consistency assumption. While Gödel showed that consistent systems containing arithmetic are incomplete, Rosser proved:
Any formal system containing primitive recursive arithmetic is either inconsistent or incomplete.
Rosser achieved this by constructing a more sophisticated undecidable sentence. Instead of Gödel's sentence G that says "I am not provable," Rosser's sentence R says:
"If I am provable, then there is a shorter proof of my negation."
This clever construction eliminates the need to assume consistency. If the system is consistent, then R is true but unprovable (making the system incomplete). If the system is inconsistent, then it proves everything anyway.
Rosser's Construction
The key insight in Rosser's proof is using the length of proofs. Let Prov_n(x) mean "x has a proof of length at most n." Rosser's sentence R can be expressed as:
∀n [Prov_n(⌜R⌝) → ∃m < n (Prov_m(⌜¬R⌝))]
Tarski's Undefinability Theorem
Alfred Tarski's undefinability theorem addresses the concept of truth itself. It states:
Arithmetic truth cannot be defined in arithmetic.
More precisely, there is no formula True(x) in the language of arithmetic such that for any arithmetic sentence φ:
True(⌜φ⌝) is true if and only if φ is true.
The Liar Paradox Connection
Tarski's proof elegantly uses a version of the liar paradox. Suppose such a truth predicate existed. We could construct a sentence L that says:
"L is not true."
Formally: L ↔ ¬True(⌜L⌝)
If L is true, then by its definition, ¬True(⌜L⌝) is true, so L is not true—contradiction! If L is false, then ¬True(⌜L⌝) is false, so True(⌜L⌝) is true, so L is true—contradiction!
Implications for Computer Science
Tarski's theorem has profound implications for computational theory. It shows that no program can correctly determine the truth of all arithmetic statements about itself. This connects to the halting problem and demonstrates fundamental limitations in self-analyzing systems.
Connections and Implications
These three theorems form a trilogy of limitation results:
- Gödel: Consistent arithmetic is incomplete
- Rosser: Arithmetic is either inconsistent or incomplete
- Tarski: Truth in arithmetic cannot be arithmetically defined
- Löb: Provability predicates have counterintuitive properties
Together, they reveal that mathematical systems have inherent boundaries—there are fundamental questions they cannot answer about themselves, truths they cannot prove, and concepts they cannot define.
These results continue to influence modern computer science, particularly in areas like program verification, automated theorem proving, and the theory of computation. They remind us that even in the precise world of mathematics, there are essential limits to what formal reasoning can achieve.
Resources
stackoverflow
What is the mathematical significance of "all (==1) [1,1..]" not ...
https://stackoverflow.com/questions/40145318/what-is-the-mathematical-significance-of-all-1-1-1-not-terminating
stackoverflow
How can one define a language which does not fit in the Chomsky ...
https://stackoverflow.com/questions/62865324/how-can-one-define-a-language-which-does-not-fit-in-the-chomsky-hierarchy
other
[PDF] An Introduction to G\"odel's Theorems - - Logic Matters
https://www.logicmatters.net/resources/pdfs/godelbook/GodelBookLM.pdf
Practice
Explain why Rosser's theorem is considered stronger than Gödel's first incompleteness theorem. In your answer, describe the key difference in assumptions and explain how Rosser's construction of the undecidable sentence differs from Gödel's.
💡 Consider what assumptions each theorem requires about the formal system, and think about how the statements 'I am not provable' versus 'If I'm provable, there's a shorter proof of my negation' behave differently.
According to Löb's theorem, if a theory T proves 'if T proves φ, then φ', what can we conclude? A) φ is true but not provable B) T proves φ C) T is inconsistent D) φ is undecidable
💡 Löb's theorem tells us what happens when we can prove a conditional statement about provability.
Construct an argument explaining why Tarski's undefinability theorem implies that no computer program can serve as a universal truth-checker for arithmetic statements. Connect this to the broader implications for automated theorem proving.
💡 Think about what it would mean for a program to be a 'truth-checker' and how this relates to defining truth within arithmetic itself.