| 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.) |
Prv 
