Timeline of mathematical logic

A timeline of mathematical logic. See also History of logic.

19th century

• 1847 – George Boole proposes symbolic logic in The Mathematical Analysis of Logic, defining what is now called Boolean algebra.
• 1854 – George Boole perfects his ideas, with the publication of An Investigation of the Laws of Thought.
• 1874 – Georg Cantor proves that the set of all real numbers is uncountably infinite but the set of all real algebraic numbers is countably infinite. His proof does not use his famous diagonal argument, which he published in 1891.
• 1895 – Georg Cantor publishes a book about set theory containing the arithmetic of infinite cardinal numbers and the continuum hypothesis.
• 1899 – Georg Cantor discovers a contradiction in his set theory.

20th century

• 1904 - Edward Vermilye Huntington develops the back-and-forth method to prove Cantor's result that countable dense linear orders (without endpoints) are isomorphic.
• 1908 – Ernst Zermelo axiomatizes set theory, thus avoiding Cantor's contradictions.
• 1928 - Hilbert and Wilhelm Ackermann propose the Entscheidungsproblem: to determine, for a statement of first-order logic whether it is universally valid (in all models).
• 1931 – Kurt Gödel proves his incompleteness theorem which shows that every axiomatic system for mathematics is either incomplete or inconsistent.
• 1936 - Alonzo Church develops the lambda calculus. Alan Turing introduces the Turing machine model proves the existence of universal Turing machines, and uses these results to settle the Entscheidungsproblem by proving it equivalent to (what is now called) the halting problem.
• 1940 – Kurt Gödel shows that neither the continuum hypothesis nor the axiom of choice can be disproven from the standard axioms of set theory.
• 1943 - Stephen Kleene introduces the assertion he calls "Church's Thesis" asserting the identity of general recursive functions with effective calculable ones.
• 1950 - Boris Trakhtenbrot proves that validity in all finite models (the finite-model version of the Entscheidungsproblem) is also undecidable; here validity sorresponds to non-halting, rather than halting as in the usual case.
• 1952 - Kleene presenets "Turing's Thesis", asserting the identity of computability in general with computability by Turing machines, as an equivalent form of Church's Thesis.
• 1954 - Jerzy Łoś conjectures that a first-order theory with a countable language (and only infinite models) is either categorical in all uncountable cardinals, or not categorical in any uncountable cardinal.
• 1961 – Abraham Robinson creates non-standard analysis.
• 1963 – Paul Cohen uses his technique of forcing to show that neither the continuum hypothesis nor the axiom of choice can be proven from the standard axioms of set theory.
• 1965 - Morley's categoricity theorem confirms Łoś' conjecture.
• 1966 - Grothendieck proves the Ax-Grothendieck theorem: any injective polynomial self-map of algebraic varieties over algebraically closed fields is bijective.
• 1968 - James Ax independently proves the Ax-Grothendieck theorem.
• 1975 - Harvey Friedman introduces the Reverse Mathematics program.