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.
Thus
(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 —