Description: Proof of Gödel's theorem from Löb's theorem (see comments at bj-babygodel and bj-babylob for details). (Contributed by BJ, 20-Apr-2019) (Proof modification is discouraged.) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | bj-godellob.s | |- ( ph <-> -. Prv ph ) |
|
bj-godellob.1 | |- -. Prv F. |
||
Assertion | bj-godellob | |- F. |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bj-godellob.s | |- ( ph <-> -. Prv ph ) |
|
2 | bj-godellob.1 | |- -. Prv F. |
|
3 | dfnot | |- ( -. Prv ph <-> ( Prv ph -> F. ) ) |
|
4 | 1 3 | bitri | |- ( ph <-> ( Prv ph -> F. ) ) |
5 | 2 | pm2.21i | |- ( Prv F. -> F. ) |
6 | 4 5 | bj-babylob | |- F. |