Misplaced Pages

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.
• 1915 - Leopold Löwenheim publishes a proof of the (downward) Löwenheim-Skolem theorem, implicitly using the axiom of choice.
• 1918 - C. I. Lewis writes A Survey of Symbolic Logic, introducing the modal logic system later called S3.
• 1920 - Thoralf Skolem proves the (downward) Löwenheim-Skolem theorem using the axiom of choice explicitly.
• 1922 - Thoralf Skolem proves a weaker version of the Löwenheim-Skolem theorem without the axiom of choice.
• 1929 - Mojzesj Presburger introduces Presburger arithmetic and proving its decidability and completeness.
• 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).
• 1930 - Kurt Gödel proves the completeness and countable compactness of first-order logic for countable languages.
• 1930 - Oskar Becker introduces the modal logic systems now called S4 and S5 as variations of Lewis's system.
• 1930 - Arend Heyting develops an intuitionistic propositional calculus.
• 1931 – Kurt Gödel proves his incompleteness theorem which shows that every axiomatic system for mathematics is either incomplete or inconsistent.
• 1932 - C. I. Lewis and C. H. Langford's Symbolic Logic contains descriptions of the modal logic systems S1-5.
• 1933 - Kurt Gödel develops two interpretations of intuitionistic logic in terms of a provability logic, which would become the standard axiomatization of S4.
• 1934 - Thoralf Skolem constructs a non-standard model of arithmetic.
• 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.
• 1936 - Anatoly Maltsev proves the full compactness theorem for first-order logic, and the "upwards" version of the Löwenheim–Skolem theorem.
• 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.
• 1944 - McKinsey and Alfred Tarski study the relationship between topological closure and Boolean closure algebras.
• 1944 - Emil Leon Post introduces the partial order of the Turing degrees, and also introduces Post's problem: to determine if there are computably enumerable degrees lying in between the degree of computable functions and the degree of the halting problem.
• 1947 - Andrey Markov Jr. and Emil Post independently prove the undecidability of the word problem for semigroups.
• 1948 - McKinsey and Alfred Tarski study closure algebras for S4 and intuitionistic logic.

1950-1999

• 1950 - Boris Trakhtenbrot proves that validity in all finite models (the finite-model version of the Entscheidungsproblem) is also undecidable; here validity corresponds to non-halting, rather than halting as in the usual case.
• 1952 - Kleene presents "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ś and Robert Lawson Vaught independently proved that a first-order theory which has only infinite models and is categorical in any infinite cardinal at least equal to the language cardinality is complete. Łoś further conjectures that, in the case where the language is countable, if the theory is categorical in an uncountable cardinal, it is categorical in all uncountable cardinals.
• 1955 - Jerzy Łoś uses the ultraproduct construction to construct the hyperreals and prove the transfer principle.
• 1955 - Pyotr Novikov finds a (finitely presented) group whose word problem is undecidable.
• 1955 - Evertt William Beth develops semantic tableaux.
• 1958 - William Boone independently proves the undecidability of the uniform word problem for groups.
• 1959 - Saul Kripke develops a semantics for quantified S5 based on multiple models.
• 1959 - Stanley Tennenbaum proves that all countable nonstandard models of Peano arithmetic are nonrecursive.
• 1960 - Ray Solomonoff develops the concept of what would come to be called Kolmogorov complexity as part of his theory of Solomonoff induction.
• 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.
• 1963 - Saul Kripke extends his possible-world semantics to normal modal logics.
• 1965 - Michael D. Morley introduces the beginnings of stable theory in order to prove Morley's categoricity theorem confirming Łoś' conjecture.
• 1965 - Andrei Kolmogorov independently develops the theory of Kolmogorov complexity and uses it to analyze the concept of randomness.
• 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.
• 1969 - Saharon Shelah introduces the concept of stable and superstable theories.
• 1970 - Yuri Matiyasevich proves that the existence of solutions to Diophantine equations is undecidable
• 1975 - Harvey Friedman introduces the Reverse Mathematics program.

See also

• History of logic
• History of mathematics
• Philosophy of mathematics
• Timeline of ancient Greek mathematicians
• Timeline of mathematics

References

v t e Mathematical logic
General	Axiom list Cardinality First-order logic Formal proof Formal semantics Foundations of mathematics Information theory Lemma Logical consequence Model Theorem Theory Type theory
Theorems (list)  and paradoxes	Gödel's completeness and incompleteness theorems Tarski's undefinability Banach–Tarski paradox Cantor's theorem, paradox and diagonal argument Compactness Halting problem Lindström's Löwenheim–Skolem Russell's paradox
Logics	Traditional Classical logic Logical truth Tautology Proposition Inference Logical equivalence Consistency Equiconsistency Argument Soundness Validity Syllogism Square of opposition Venn diagram Propositional Boolean algebra Boolean functions Logical connectives Propositional calculus Propositional formula Truth tables Many-valued logic 3 finite ∞ Predicate First-order list Second-order Monadic Higher-order Fixed-point Free Quantifiers Predicate Monadic predicate calculus
Set theory	Set hereditary Class (Ur-)Element Ordinal number Extensionality Forcing Relation equivalence partition Set operations: intersection union complement Cartesian product power set identities Types of sets Countable Uncountable Empty Inhabited Singleton Finite Infinite Transitive Ultrafilter Recursive Fuzzy Universal Universe constructible Grothendieck Von Neumann Maps and cardinality Function/Map domain codomain image In/Sur/Bi-jection Schröder–Bernstein theorem Isomorphism Gödel numbering Enumeration Large cardinal inaccessible Aleph number Operation binary Set theories Zermelo–Fraenkel axiom of choice continuum hypothesis General Kripke–Platek Morse–Kelley Naive New Foundations Tarski–Grothendieck Von Neumann–Bernays–Gödel Ackermann Constructive
Formal systems (list), language and syntax	Alphabet Arity Automata Axiom schema Expression ground Extension by definition conservative Relation Formation rule Grammar Formula atomic closed ground open Free/bound variable Language Metalanguage Logical connective ¬ ∨ ∧ → ↔ = Predicate functional variable propositional variable Proof Quantifier ∃ ! ∀ rank Sentence atomic spectrum Signature String Substitution Symbol function logical/constant non-logical variable Term Theory list Example axiomatic systems (list) of arithmetic: Peano second-order elementary function primitive recursive Robinson Skolem of the real numbers Tarski's axiomatization of Boolean algebras canonical minimal axioms of geometry: Euclidean: Elements Hilbert's Tarski's non-Euclidean Principia Mathematica
Proof theory	Formal proof Natural deduction Logical consequence Rule of inference Sequent calculus Theorem Systems axiomatic deductive Hilbert list Complete theory Independence (from ZFC) Proof of impossibility Ordinal analysis Reverse mathematics Self-verifying theories
Model theory	Interpretation function of models Model equivalence finite saturated spectrum submodel Non-standard model of arithmetic Diagram elementary Categorical theory Model complete theory Satisfiability Semantics of logic Strength Theories of truth semantic Tarski's Kripke's T-schema Transfer principle Truth predicate Truth value Type Ultraproduct Validity
Computability theory	Church encoding Church–Turing thesis Computably enumerable Computable function Computable set Decision problem decidable undecidable P NP P versus NP problem Kolmogorov complexity Lambda calculus Primitive recursive function Recursion Recursive set Turing machine Type theory
Related	Abstract logic Algebraic logic Automated theorem proving Category theory Concrete/Abstract category Category of sets History of logic History of mathematical logic timeline Logicism Mathematical object Philosophy of mathematics Supertask
Mathematics portal

• History of mathematics
• Mathematics timelines
• Mathematical logic