![]() |
Mathbox for BJ |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > bj-babygodel | Structured version Visualization version GIF version |
Description: See the section header
comments for the context.
The first hypothesis reads "π is true if and only if it is not provable in T" (and having this first hypothesis means that we can prove this fact in T). The wff π is a formal version of the sentence "This sentence is not provable". The hard part of the proof of GΓΆdel's theorem is to construct such a π, called a "GΓΆdelβRosser sentence", for a first-order theory T which is effectively axiomatizable and contains Robinson arithmetic, through GΓΆdel diagonalization (this can be done in primitive recursive arithmetic). The second hypothesis means that β₯ is not provable in T, that is, that the theory T is consistent (and having this second hypothesis means that we can prove in T that the theory T is consistent). The conclusion is the falsity, so having the conclusion means that T can prove the falsity, that is, T is inconsistent. Therefore, taking the contrapositive, this theorem expresses that if a first-order theory is consistent (and one can prove in it that some formula is true if and only if it is not provable in it), then this theory does not prove its own consistency. This proof is due to George Boolos, GΓΆdel's Second Incompleteness Theorem Explained in Words of One Syllable, Mind, New Series, Vol. 103, No. 409 (January 1994), pp. 1--3. (Contributed by BJ, 3-Apr-2019.) |
Ref | Expression |
---|---|
bj-babygodel.s | β’ (π β Β¬ Prv π) |
bj-babygodel.1 | β’ Β¬ Prv β₯ |
Ref | Expression |
---|---|
bj-babygodel | β’ β₯ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bj-babygodel.1 | . . . 4 β’ Β¬ Prv β₯ | |
2 | 1 | ax-prv1 35476 | . . 3 β’ Prv Β¬ Prv β₯ |
3 | bj-babygodel.s | . . . . . . . . 9 β’ (π β Β¬ Prv π) | |
4 | 3 | biimpi 215 | . . . . . . . 8 β’ (π β Β¬ Prv π) |
5 | 4 | prvlem1 35479 | . . . . . . 7 β’ (Prv π β Prv Β¬ Prv π) |
6 | ax-prv3 35478 | . . . . . . 7 β’ (Prv π β Prv Prv π) | |
7 | pm2.21 123 | . . . . . . . 8 β’ (Β¬ Prv π β (Prv π β β₯)) | |
8 | 7 | prvlem2 35480 | . . . . . . 7 β’ (Prv Β¬ Prv π β (Prv Prv π β Prv β₯)) |
9 | 5, 6, 8 | sylc 65 | . . . . . 6 β’ (Prv π β Prv β₯) |
10 | 9 | con3i 154 | . . . . 5 β’ (Β¬ Prv β₯ β Β¬ Prv π) |
11 | 10, 3 | sylibr 233 | . . . 4 β’ (Β¬ Prv β₯ β π) |
12 | 11 | prvlem1 35479 | . . 3 β’ (Prv Β¬ Prv β₯ β Prv π) |
13 | 2, 12, 9 | mp2b 10 | . 2 β’ Prv β₯ |
14 | 13, 1 | pm2.24ii 120 | 1 β’ β₯ |
Colors of variables: wff setvar class |
Syntax hints: Β¬ wn 3 β wb 205 β₯wfal 1554 Prv cprvb 35475 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-prv1 35476 ax-prv2 35477 ax-prv3 35478 |
This theorem depends on definitions: df-bi 206 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |