1935 ⟶ Church Proves the Undecidability of the Decision Problem and Develops Lambda Calculus

Alonzo Church extended Gödel's proof and showed that the dec...
Timelines Logo
Year
1931
1935
1937

♾️ Gödel Proves Limits of Algorithmic Theorem Proving

Kurt Gödel encoded mathematical statements and proofs as integers, and showed that there are true theorems that are unprovable by any consistent theorem-proving machine. Thus "he identified fundamental limits of algorithmic theorem proving, computing, and any type of computation-based AI," laying foundations of Theoretical computer science and AI theory.⟶
Gödel Proves Limits of Algorithmic Theorem Proving (1931)
Gödel's incompleteness theoremsMathematicsLogicComputabilityTheorem provingLimits of computationTheoretical computer scienceFoundations
AustriaAustria

λ Church Proves the Undecidability of the Decision Problem and Develops Lambda Calculus

Alonzo Church extended Gödel's proof and showed that the Decision problem of computer science does not have a general solution. He developed the Lambda calculus, which will eventually be fundamental to the theory of computer languages.⟶
Church Proves the Undecidability of the Decision Problem and Develops Lambda Calculus (1935)
UndecidabilityDecision problemLambda calculusComputabilityTheoretical computer scienceProgramming languagesAlgorithmsChurch-Turing thesis
USAUSA

💻 Turing Introduces the Turing Machine and Proves the Halting Problem Undecidable

Alan Turing published "On Computable Numbers", which laid the foundations of the modern Theory of computation by introducing the Turing machine, a physical interpretation of "computability". He used it to confirm Gödel by proving that the Halting problem is undecidable.⟶
Turing Introduces the Turing Machine and Proves the Halting Problem Undecidable (1937)
Turing machineHalting problemComputabilityTheoretical computer scienceAlgorithmsFoundationsAlan TuringComputation
United KingdomUnited Kingdom