Users' Mathboxes Mathbox for BJ < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  bj-babygodel Structured version   Visualization version   GIF version

Theorem bj-babygodel 35121
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.)

Hypotheses
Ref Expression
bj-babygodel.s (πœ‘ ↔ Β¬ Prv πœ‘)
bj-babygodel.1 Β¬ Prv βŠ₯
Assertion
Ref Expression
bj-babygodel βŠ₯

Proof of Theorem bj-babygodel
StepHypRef Expression
1 bj-babygodel.1 . . . 4 Β¬ Prv βŠ₯
21ax-prv1 35116 . . 3 Prv Β¬ Prv βŠ₯
3 bj-babygodel.s . . . . . . . . 9 (πœ‘ ↔ Β¬ Prv πœ‘)
43biimpi 215 . . . . . . . 8 (πœ‘ β†’ Β¬ Prv πœ‘)
54prvlem1 35119 . . . . . . 7 (Prv πœ‘ β†’ Prv Β¬ Prv πœ‘)
6 ax-prv3 35118 . . . . . . 7 (Prv πœ‘ β†’ Prv Prv πœ‘)
7 pm2.21 123 . . . . . . . 8 (Β¬ Prv πœ‘ β†’ (Prv πœ‘ β†’ βŠ₯))
87prvlem2 35120 . . . . . . 7 (Prv Β¬ Prv πœ‘ β†’ (Prv Prv πœ‘ β†’ Prv βŠ₯))
95, 6, 8sylc 65 . . . . . 6 (Prv πœ‘ β†’ Prv βŠ₯)
109con3i 154 . . . . 5 (Β¬ Prv βŠ₯ β†’ Β¬ Prv πœ‘)
1110, 3sylibr 233 . . . 4 (Β¬ Prv βŠ₯ β†’ πœ‘)
1211prvlem1 35119 . . 3 (Prv Β¬ Prv βŠ₯ β†’ Prv πœ‘)
132, 12, 9mp2b 10 . 2 Prv βŠ₯
1413, 1pm2.24ii 120 1 βŠ₯
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   ↔ wb 205  βŠ₯wfal 1554  Prv cprvb 35115
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-prv1 35116  ax-prv2 35117  ax-prv3 35118
This theorem depends on definitions:  df-bi 206
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator