A timeline of ** mathematical logic **; see also history of logic.

- 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.

- 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 - 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.

- History of logic
- History of mathematics
- Philosophy of mathematics
- Timeline of ancient Greek mathematicians – Timeline and summary of ancient Greek mathematicians and their discoveries
- Timeline of mathematics

**Automated theorem proving** is a subfield of automated reasoning and mathematical logic dealing with proving mathematical theorems by computer programs. Automated reasoning over mathematical proof was a major impetus for the development of computer science.

In mathematics and computer science, the * Entscheidungsproblem* is a challenge posed by David Hilbert and Wilhelm Ackermann in 1928. The problem asks for an algorithm that considers, as input, a statement and answers "yes" or "no" according to whether the statement is

In the philosophy of mathematics, **intuitionism**, or **neointuitionism**, is an approach where mathematics is considered to be purely the result of the constructive mental activity of humans rather than the discovery of fundamental principles claimed to exist in an objective reality. That is, logic and mathematics are not considered analytic activities wherein deep properties of objective reality are revealed and applied, but are instead considered the application of internally consistent methods used to realize more complex mental constructs, regardless of their possible independent existence in an objective reality.

**Mathematical logic** is the study of formal logic within mathematics. Major subareas include model theory, proof theory, set theory, and recursion theory. Research in mathematical logic commonly addresses the mathematical properties of formal systems of logic such as their expressive or deductive power. However, it can also include uses of logic to characterize correct mathematical reasoning or to establish foundations of mathematics.

In mathematical logic, **model theory** is the study of the relationship between formal theories, and their models. The aspects investigated include the number and size of models of a theory, the relationship of different models to each other, and their interaction with the formal language itself. In particular, model theorists also investigate the sets that can be defined in a model of a theory, and the relationship of such definable sets to each other. As a separate discipline, model theory goes back to Alfred Tarski, who first used the term "Theory of Models" in publication in 1954. Since the 1970s, the subject has been shaped decisively by Saharon Shelah's stability theory.

**Gödel's incompleteness theorems** are two theorems of mathematical logic that are concerned with the limits of provability in formal axiomatic theories. These results, published by Kurt Gödel in 1931, are important both in mathematical logic and in the philosophy of mathematics. The theorems are widely, but not universally, interpreted as showing that Hilbert's program to find a complete and consistent set of axioms for all mathematics is impossible.

In mathematical logic, the **compactness theorem** states that a set of first-order sentences has a model if and only if every finite subset of it has a model. This theorem is an important tool in model theory, as it provides a useful method for constructing models of any set of sentences that is finitely consistent.

**Computability theory**, also known as **recursion theory**, is a branch of mathematical logic, computer science, and the theory of computation that originated in the 1930s with the study of computable functions and Turing degrees. The field has since expanded to include the study of generalized computability and definability. In these areas, computability theory overlaps with proof theory and effective descriptive set theory.

**Foundations of mathematics** is the study of the philosophical and logical and/or algorithmic basis of mathematics, or, in a broader sense, the mathematical investigation of what underlies the philosophical theories concerning the nature of mathematics. In this latter sense, the distinction between foundations of mathematics and philosophy of mathematics turns out to be vague. Foundations of mathematics can be conceived as the study of the basic mathematical concepts and how they form hierarchies of more complex structures and concepts, especially the fundamentally important structures that form the language of mathematics also called metamathematical concepts, with an eye to the philosophical aspects and the unity of mathematics. The search for foundations of mathematics is a central question of the philosophy of mathematics; the abstract nature of mathematical objects presents special philosophical challenges.

**Metamathematics** is the study of mathematics itself using mathematical methods. This study produces metatheories, which are mathematical theories about other mathematical theories. Emphasis on metamathematics owes itself to David Hilbert's attempt to secure the foundations of mathematics in the early part of the 20th century. Metamathematics provides "a rigorous mathematical technique for investigating a great variety of foundation problems for mathematics and logic". An important feature of metamathematics is its emphasis on differentiating between reasoning from inside a system and from outside a system. An informal illustration of this is categorizing the proposition "2+2=4" as belonging to mathematics while categorizing the proposition "'2+2=4' is valid" as belonging to metamathematics.

In mathematical logic, the **Löwenheim–Skolem theorem** is a theorem on the existence and cardinality of models, named after Leopold Löwenheim and Thoralf Skolem.

**Thoralf Albert Skolem** was a Norwegian mathematician who worked in mathematical logic and set theory.

In logic, a true/false decision problem is **decidable** if there exists an effective method for deriving the correct answer. Zeroth-order logic is decidable, whereas first-order and higher-order logic are not. Logical systems are decidable if membership in their set of logically valid formulas can be effectively determined. A theory in a fixed logical system is decidable if there is an effective method for determining whether arbitrary formulas are included in the theory. Many important problems are undecidable, that is, it has been proven that no effective method for determining membership can exist for them.

In mathematical logic, a theory is **categorical** if it has exactly one model. Such a theory can be viewed as *defining* its model, uniquely characterizing the model's structure.

In mathematical logic and philosophy, **Skolem's paradox** is a seeming contradiction that arises from the downward Löwenheim–Skolem theorem. Thoralf Skolem (1922) was the first to discuss the seemingly contradictory aspects of the theorem, and to discover the relativity of set-theoretic notions now known as non-absoluteness. Although it is not an actual antinomy like Russell's paradox, the result is typically called a paradox and was described as a "paradoxical state of affairs" by Skolem.

In mathematical logic, a **non-standard model of arithmetic** is a model of (first-order) Peano arithmetic that contains non-standard numbers. The term **standard model of arithmetic** refers to the standard natural numbers 0, 1, 2, …. The elements of any model of Peano arithmetic are linearly ordered and possess an initial segment isomorphic to the standard natural numbers. A non-standard model is one that has additional elements outside this initial segment. The construction of such models is due to Thoralf Skolem (1934).

**Logic** is the formal science of using reason and is considered a branch of both philosophy and mathematics and to a lesser extent computer science. Logic investigates and classifies the structure of statements and arguments, both through the study of formal systems of inference and the study of arguments in natural language. The scope of logic can therefore be very large, ranging from core topics such as the study of fallacies and paradoxes, to specialized analyses of reasoning such as probability, correct reasoning, and arguments involving causality. One of the aims of logic is to identify the correct and incorrect inferences. Logicians study the criteria for the evaluation of arguments.

In computability theory and computational complexity theory, an **undecidable problem** is a decision problem for which it is proved to be impossible to construct an algorithm that always leads to a correct yes-or-no answer. The halting problem is an example: it can be proven that there is no algorithm that correctly determines whether arbitrary programs eventually halt when run.

This page is based on this Wikipedia article

Text is available under the CC BY-SA 4.0 license; additional terms may apply.

Images, videos and audio are available under their respective licenses.

Text is available under the CC BY-SA 4.0 license; additional terms may apply.

Images, videos and audio are available under their respective licenses.