Gödel's first incompleteness theorem shows that any consistent logical theory expressive enough for elementary arithmetic, i.e. with addition, multiplication and quantifiers could express true sentences unprovable in the theory.
Gödel's second incompleteness theorem tells that the consistency of the system is one of these unprovable sentences.
The basis of Gödel's proof was the fact that the syntactic computations involved in combining formulas and verifying that a sequence of formulas is a proof can be imitated by arithmetic computations on ``Gödel numbers'' of formulas. If we have axioms for symbolic computations, e.g. for Lisp computations, then the proofs of Gödel's theorems become much shorter. Shankar [Shankar, 1986] has demonstrated this using the Boyer-Moore prover. Among the unprovable true sentences is the statement of the theory's own consistency. We can interpret this as saying that the theory lacks self-confidence. Turing, in his PhD thesis, studied what happens if we add to a theory T the statement consis(T) asserting that T is consistent, getting a stronger theory T'. While the new theory has consis(T) as a theorem, it doesn't have consis(T') as a theorem--provided it is consistent. The process can be iterated, and the union of all these theories is . Indeed the process can again be iterated, as Turing showed, to any constructive ordinal number.