Mathbox for BJ |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > bj-babylob | Structured version Visualization version Unicode version |
Description: See the section header
comments for the context, as well as the comments
for bj-babygodel 32588.
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 |
---|---|
bj-babylob.s | Prv |
bj-babylob.1 | Prv |
Ref | Expression |
---|---|
bj-babylob |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-prv3 32585 | . . . . . 6 Prv Prv Prv | |
2 | bj-babylob.s | . . . . . . . 8 Prv | |
3 | 2 | biimpi 206 | . . . . . . 7 Prv |
4 | 3 | prvlem2 32587 | . . . . . 6 Prv Prv Prv Prv |
5 | 1, 4 | mpd 15 | . . . . 5 Prv Prv |
6 | bj-babylob.1 | . . . . 5 Prv | |
7 | 5, 6 | syl 17 | . . . 4 Prv |
8 | 7, 2 | mpbir 221 | . . 3 |
9 | 8 | ax-prv1 32583 | . 2 Prv |
10 | 9, 7 | ax-mp 5 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wb 196 Prv cprvb 32582 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-prv1 32583 ax-prv2 32584 ax-prv3 32585 |
This theorem depends on definitions: df-bi 197 |
This theorem is referenced by: bj-godellob 32590 |
Copyright terms: Public domain | W3C validator |