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 | ||
bj-babylob.1 | |||
Assertion | bj-babylob |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bj-babylob.s | ||
2 | bj-babylob.1 | ||
3 | ax-prv3 | ||
4 | 1 | biimpi | |
5 | 4 | prvlem2 | |
6 | 3 5 | mpd | |
7 | 6 2 | syl | |
8 | 7 1 | mpbir | |
9 | 8 | ax-prv1 | |
10 | 9 7 | ax-mp |