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

Theorem bj-babygodel 30743
Description: See the section header comments for the context.

The first hypothesis reads " ph 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  ph 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  ph, 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 F. 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  |-  ( ph  <->  -. Prv  ph )
bj-babygodel.1  |-  -. Prv F.
Assertion
Ref Expression
bj-babygodel  |- F.

Proof of Theorem bj-babygodel
StepHypRef Expression
1 bj-babygodel.1 . . 3  |-  -. Prv F.
21ax-prv1 30738 . 2  |- Prv  -. Prv F.
3 bj-babygodel.s . . . . . . . . . 10  |-  ( ph  <->  -. Prv  ph )
43biimpi 194 . . . . . . . . 9  |-  ( ph  ->  -. Prv  ph )
54prvlem1 30741 . . . . . . . 8  |-  (Prv  ph  -> Prv 
-. Prv  ph )
6 ax-prv3 30740 . . . . . . . 8  |-  (Prv  ph  -> Prv Prv  ph )
7 pm2.21 108 . . . . . . . . 9  |-  ( -. Prv  ph  ->  (Prv  ph  -> F.  ) )
87prvlem2 30742 . . . . . . . 8  |-  (Prv  -. Prv  ph 
->  (Prv Prv  ph  -> Prv F.  ) )
95, 6, 8sylc 59 . . . . . . 7  |-  (Prv  ph  -> Prv F.  )
109con3i 135 . . . . . 6  |-  ( -. Prv F.  ->  -. Prv  ph )
1110, 3sylibr 212 . . . . 5  |-  ( -. Prv F.  ->  ph )
1211prvlem1 30741 . . . 4  |-  (Prv  -. Prv F. 
-> Prv  ph )
1312, 9syl 17 . . 3  |-  (Prv  -. Prv F. 
-> Prv F.  )
141, 13mto 176 . 2  |-  -. Prv  -. Prv F.
152, 14pm2.24ii 132 1  |- F.
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    <-> wb 184   F. wfal 1410  Prv cprvb 30737
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-prv1 30738  ax-prv2 30739  ax-prv3 30740
This theorem depends on definitions:  df-bi 185
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator