Lob's Theorem
Summary
Lob's Theorem asserts that no formal system T can prove statements of the form "If A is provable in T, then A is true" unless it is also capable of proving A directly. It can be seen as a generalization of Godel's Second Incompleteness Theorem.
Context
This concept has the prerequisites:
- semantics of first-order logic (Lob's Theorem is a statement about the semantics of first-order logic.)
- proofs in first-order logic (Lob's Theorem is a statement about proofs in first-order logic.)
- Godel numbering (Stating Lob's Theorem requires Godel numbering.)
- Godel's Incompleteness Theorems (Lob's Theorem is a generalization of Godel's Second Incompleteness Theorem, and the proof is analogous.)
Goals
- Know the statement of Lob's Theorem and why it is significant
- Show how to derive Godel's Second Incompleteness Theorem as a special case of Lob's Theorem
- Prove Lob's Theorem
Core resources (read/watch one of the following)
-Free-
→ Notes on Logic (2013)
Lecture notes for a course on first order logic.
→ Wikipedia
-Paid-
→ A Mathematical Introduction to Logic
An undergraduate textbook in mathematical logic, with proofs.
Location:
Part of Section 3.7, "Second Incompleteness Theorem," from pages 268-270
See also
-No Additional Notes-