Godel’s First Incompleteness Theorem

Godel’s First Incompleteness Theorem. Any adequate axiomatizable theory is incomplete.   In particular the sentence “This sentence is not provable” is true but not provable in the theory.
Proof. Given a computably generated set of axioms, let PROVABLE be the set of numbers which encode sentences which are provable from the given axioms.
Thus for any sentence   s,
(1)   < s > is in PROVABLE   iff   s is provable.
Since the set of axioms is computably generable,
so is the set of proofs which use these axioms and
so is the set of provable theorems and hence
so is PROVABLE, the set of encodings of provable theorems.
Since computable implies definable in adequate theories, PROVABLE is definable.
Let s be the sentence “This sentence is unprovable”.
By Tarski, s exists since it is the solution of:
(2)   s   iff   < s > is not in PROVABLE.
(3)   s   iff   < s > is not in PROVABLE   iff   s is not provable.
Now (excluded middle again) s is either true or false.
If   s   is false, then by (3),   s   is provable.
This is impossible since provable sentences are true.
Thus   s   is true.
Thus by (3),   s   is not provable.
Hence   s   is true but unprovable.
Note 1. An analysis of the proof shows that the axioms don’t have to be true. It suffices that (a) the system is consistent and (b) it can prove the basic facts needed to do arithmetical computations, e.g., prove that 2+2=4. The latter is needed to encode sequences of numbers and insure that computable sets are definable.Note 2. Godel discovered that the sentence “This sentence is unprovable” was provably equivalent to the sentence   CON:
“There is no   < s >   with both   < s >   and   < not s >   in PROVABLE”.
CON is the formal statement that the system is consistent.
Since   s   was not provable, and since   s   and   CON   are equivalent,
CON is not provable.   Thus —

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out /  Change )

Google photo

You are commenting using your Google account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s

This site uses Akismet to reduce spam. Learn how your comment data is processed.