It is not so easy to determine exactly which meta-mathematical theorems are to be identified as Gödel's First and Second Incompleteness Theorems. Indeed, many differing meta-mathematical theorems of varying strength and generality have been claimed to be either Gödel's First or Second Incompleteness Theorem by different authors. In fact, the original incompleteness theorems which Gödel formulated in his 1931 paper entitled "Über formal unentscheidbare Satze der Principia Mathematica und verwandter Systeme I" (On formally undecidable propositions of Principia Mathematica and related Systems I) applied only to (that part which is required to obtain arithmetic of) the formal system presented in Russell's and Whitehead's Principia Mathematica. These theorems, however, were soon generalized by his contemporaries. The most general of these generalizations are equivalent to the following:

  1. Every consistent axiomatized strengthening of first order Peano arithmetic without the induction schema, which itself is an incomplete theory, is incomplete. (Gödel I)
  2. The consistency of any consistent axiomatized extension of first order Peano arithmetic is not provable in that extension. (Gödel II)

Gödel in a note added to his 1931 paper in 1963:

... it can be proved rigorously that in every consistent formal system that contains a certain amount of finitary number theory there exist undecidable arithmetic propositions [Gödel's First Incompleteness Theorem] and that, moreover, the consistency of any such system cannot be proved in the system [Gödel's Second Incompleteness Theorem].
What precisely do we mean by an undecidable sentence:
A sentence a of a theory T is undecidable in T if neither T|-a nor T|-¬a.
For more info, see standard textbooks on the philosophy of mathematics.


What others say

Several philosophers have commented on and written about Gödel's theorems. Some follow.


G1 and G2 show that for any correct system containing arithmetic there are 'correct' inferences - inferences to whose acceptability the user of the system is rationally committed - that cannot be captured by it. There is, thus, an absolute epistemic notion of provability, according to which Gödel's undecidable sentences are provable. Hence, this notion of absolute provability is not farmalizable.


Refines Myhill and argues that if 'humanly provable' means 'formally provable' there must be absolutely undecidable sentences of arithmetic. And more ...


Uses G1 to argue that mathematical proof is an 'indefinitely extensible concept', and cannot, therefore, be identified with derivation in any formal system. Since, he believes, the meanings of mathematical statements are to be given in terms of a concept of proof, this means that the notion of proof that determines the meanings of mathematical statements must be an essentially vague and unformalizable one.