What did godel prove?

Kurt Gödel, answered from the texts and cited to the page.

Kurt Gödel answers

The central result is this: any consistent formal system that contains a sufficient portion of finitary number theory must contain arithmetic propositions that are undecidable within it — and moreover, the consistency of any such system cannot be proved within the system itself.1 The second theorem is the sharper philosophical result. No one can set up a formal system and consistently claim, with mathematical certitude, that its axioms and rules are correct and that they contain all of mathematics.

The reason is precise: anyone who claims to perceive the correctness of the axioms must also claim to perceive their consistency; but the consistency of the system is not provable within it; therefore the person is claiming to perceive the truth of something the system cannot prove, and is thereby obliged to abandon the claim that the system contains all of mathematics.2

The consequence for Hilbert's program follows directly. Hilbert sought finitary consistency proofs for formal systems sufficient to formalize mathematics. By the second theorem, no such system can prove its own consistency unless it is inconsistent — and all finitary proof methods that had ever been constructed could be expressed within classical arithmetic, with good reason to believe no finitary method would ever go beyond it.3

The program, as originally conceived, cannot be carried out. One clarification I was careful to make in 1931: the theorems do not, by themselves, contradict Hilbert's formalistic viewpoint outright, since it remained conceivable in principle that finitary proofs might exist that cannot be expressed in the relevant formal systems.4 I later convinced myself, and said so explicitly, that this possibility offered no real hope — but the logical gap between the theorem and that stronger conclusion was real, and I did not paper over it.

Von Neumann saw the second result almost simultaneously. He wrote to me in November 1930 that the unprovability of the consistency statement follows from my considerations, and called the discovery the greatest logical result in a long time.5

Sources

  1. 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 and that, moreover, the consistency of any such system cannot be proved in the system.
    Volume I, p. 195
  2. No one can set up a formal system and consistently state about it that he perceives (with mathematical certitude) that its axioms and rules are correct and that he believes that they contain all of mathematics, for anyone who claims to perceive the correctness of the axioms and rules must also claim to perceive their consistency; but since the consistency of the axioms is not provable in the system, the person is claiming to perceive the truth of something that cannot be proved in the system, and is therefore obliged to abandon the claim that the system contains all of mathematics.
    Collected Works Vol III - Unpublished Essays and Lectures, pp. 312–313
  3. no formal system S which contains PA can prove its own consistency, unless it is inconsistent... all the intuitionistic [finitary] proofs complying with the requirements of the system A [of finitistically allowable methods] which have ever been constructed can easily be expressed in the system of classical analysis and even in the system of classical arithmetic, and there are reasons for believing that this will hold for any proof which one will ever be able to construct.
    Collected Works Vol III - Unpublished Essays and Lectures, p. 61
  4. I wish to note expressly that Theorem XI (and the corresponding results for M and A) do not contradict Hilbert's formalistic viewpoint. For this viewpoint presupposes only the existence of a consistency proof in which nothing but unitary means of proof is used, and it is conceivable that there exist finitary proofs that cannot be expressed in the formalism of P.
    Volume I, p. 195
  5. E. Schmidt, to whom I communicated your result as you had presented it in Königsberg, was delighted by it. He considers it, as I do, to be the greatest logical discovery in a long time.
    John von Neumann, pp. 364–365