section_path: Career/Incompleteness theorems
section_name: Incompleteness theorems
paragraph_text: Incompleteness theorems
  
  Kurt Gödel's achievement in modern logic is singular and monumental—indeed it is more than a monument, it is a landmark which will remain visible far in space and time.... The subject of logic has certainly completely changed its nature and possibilities with Gödel's achievement.
  
  In 1930 Gödel attended the Second Conference on the Epistemology of the Exact Sciences, held in Königsberg, 5–7 September. Here he delivered his incompleteness theorems.
  
  Gödel published his incompleteness theorems in Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme (called in English " On Formally Undecidable Propositions of Principia Mathematica and Related Systems "). In that article, he proved for any computable axiomatic system that is powerful enough to describe the arithmetic of the natural numbers (e.g., the Peano axioms or Zermelo–Fraenkel set theory with the axiom of choice), that:
  
  These theorems ended a half-century of attempts, beginning with the work of Gottlob Frege and culminating in Principia Mathematica and Hilbert's program, to find a non- relatively consistent axiomatization sufficient for number theory (that was to serve as the foundation for other fields of mathematics).
  
  Gödel constructed a formula that claims it is unprovable in a given formal system. If it were provable, it would be false. Thus there will always be at least one true but unprovable statement. That is, for any computably enumerable set of axioms for arithmetic (that is, a set that can in principle be printed out by an idealized computer with unlimited resources), there is a formula that is true of arithmetic, but not provable in that system. To make this precise, Gödel had to produce a method to encode (as natural numbers) statements, proofs, and the concept of provability; he did this by a process known as Gödel numbering.
  
  In his two-page paper Zum intuitionistischen Aussagenkalkül (1932), Gödel refuted the finite-valuedness of intuitionistic logic. In the proof, he implicitly used what has later become known as Gödel–Dummett intermediate logic (or Gödel fuzzy logic).