Description: See the section header comments for the context, as well as the comments for bj-babygodel .
Löb's theorem when the Löb sentence is given as a hypothesis (the hard part of the proof of Löb's theorem is to construct this Löb sentence; this can be done, using Gödel diagonalization, for any first-order effectively axiomatizable theory containing Robinson arithmetic). More precisely, the present theorem states that if a first-order theory proves that the provability of a given sentence entails its truth (and if one can construct in this theory a provability predicate and a Löb sentence, given here as the first hypothesis), then the theory actually proves that sentence.
See for instance, Eliezer Yudkowsky,The Cartoon Guide to Löb's Theorem (available at http://yudkowsky.net/rational/lobs-theorem/ ).
(Contributed by BJ, 20-Apr-2019)
Ref | Expression | ||
---|---|---|---|
Hypotheses | bj-babylob.s | ⊢ ( 𝜓 ↔ ( Prv 𝜓 → 𝜑 ) ) | |
bj-babylob.1 | ⊢ ( Prv 𝜑 → 𝜑 ) | ||
Assertion | bj-babylob | ⊢ 𝜑 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bj-babylob.s | ⊢ ( 𝜓 ↔ ( Prv 𝜓 → 𝜑 ) ) | |
2 | bj-babylob.1 | ⊢ ( Prv 𝜑 → 𝜑 ) | |
3 | ax-prv3 | ⊢ ( Prv 𝜓 → Prv Prv 𝜓 ) | |
4 | 1 | biimpi | ⊢ ( 𝜓 → ( Prv 𝜓 → 𝜑 ) ) |
5 | 4 | prvlem2 | ⊢ ( Prv 𝜓 → ( Prv Prv 𝜓 → Prv 𝜑 ) ) |
6 | 3 5 | mpd | ⊢ ( Prv 𝜓 → Prv 𝜑 ) |
7 | 6 2 | syl | ⊢ ( Prv 𝜓 → 𝜑 ) |
8 | 7 1 | mpbir | ⊢ 𝜓 |
9 | 8 | ax-prv1 | ⊢ Prv 𝜓 |
10 | 9 7 | ax-mp | ⊢ 𝜑 |