Kurt Gödel

Kurt Gödel was a logician and mathematician whose incompleteness theorems showed that sufficiently expressive, consistent formal systems cannot prove every arithmetical truth or establish their own consistency.

Formal system: A formal system consists of symbols, axioms, and rules for deriving theorems. Gödel’s results apply to formal systems capable of expressing enough arithmetic.
Gödel numbering: A method that assigns natural numbers to symbols, formulas, and proofs in a formal language. It lets arithmetic represent the syntax and proof relations of a formal system.
Vienna Circle: A group of philosophers and scientists in interwar Vienna who promoted logical empiricism. Gödel discussed logic and foundations with members while developing his early work.
John von Neumann: A Hungarian-American mathematician whose work spanned set theory, quantum mechanics, computing, and economics. Von Neumann recognized the force of Gödel’s second incompleteness theorem soon after its announcement.
Completeness theorem: Gödel’s completeness theorem states that every logically valid first-order sentence is provable in first-order logic. It contrasts with incompleteness: first-order logic is complete even though arithmetic theories can be incomplete.
First-order logic: A logical language with quantifiers over objects and predicates describing their properties and relations. First-order theories provide a standard setting for stating arithmetic and its axioms.
Gödel's incompleteness theorems: Two theorems showing limits on provability in consistent formal systems that can express elementary arithmetic. These are the central results Gödel established using arithmetized syntax.
Hilbert's program: David Hilbert’s project to formalize mathematics and prove the consistency of its foundations by finitary methods. Gödel’s incompleteness theorems established limits on the program’s original ambitions.
Alonzo Church: An American mathematician and logician who developed lambda calculus and results on undecidability. Church’s work established a parallel route to limits on formal decision procedures.
Entscheidungsproblem: The decision problem asks whether an algorithm can determine the validity of every statement in a formal logic. Gödel’s work helped clarify the limits of formal proof that later undecidability results made explicit.

Linked from 23 pages