Löb's theorem
Teorema de Löb
- Date
- 1955 · confidence high
- Place
- Amsterdam, North Holland, Netherlands
- Credited to
- Martin Löb
- Field
- Knowledge & symbols
What was discovered
A theorem of mathematical logic stating that, in Peano arithmetic or any formal system including it, if it is provable that "if P is provable then P is true", then P is provable; solves a problem posed by Leon Henkin about self-reference in formal systems; proved by Martin Löb.
What it led to
- Fundamental result in provability logic (the GL system)
- Influenced the study of self-reference and Gödel's theorems
- Applications in type theory and program verification