This is a list of

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

topics, by Wikipedia page. For traditional syllogistic logic, see the list of topics in logic. See also the list of computability and complexity topics for more theory of

algorithm In mathematics and computer science, an algorithm () is a finite sequence of rigorous instructions, typically used to solve a class of specific problems or to perform a computation. Algorithms are used as specifications for performing ...

Working foundations

Peano axioms In mathematical logic, the Peano axioms, also known as the Dedekind–Peano axioms or the Peano postulates, are axioms for the natural numbers presented by the 19th century Italian mathematician Giuseppe Peano. These axioms have been used nearly ...

Giuseppe Peano Giuseppe Peano (; ; 27 August 1858 – 20 April 1932) was an Italian mathematician and glottologist. The author of over 200 books and papers, he was a founder of mathematical logic and set theory, to which he contributed much notation. The sta ...

Mathematical induction Mathematical induction is a method for proving that a statement ''P''(''n'') is true for every natural number ''n'', that is, that the infinitely many cases ''P''(0), ''P''(1), ''P''(2), ''P''(3), ... all hold. Informal metaphors help ...

Structural induction Structural induction is a proof method that is used in mathematical logic (e.g., in the proof of Łoś' theorem), computer science, graph theory, and some other mathematical fields. It is a generalization of mathematical induction over natural nu ...

Recursive definition In mathematics and computer science, a recursive definition, or inductive definition, is used to define the elements in a set in terms of other elements in the set ( Aczel 1977:740ff). Some examples of recursively-definable objects include facto ...

* Naive set theory **

Element (mathematics) In mathematics, an element (or member) of a set is any one of the distinct objects that belong to that set. Sets Writing A = \ means that the elements of the set are the numbers 1, 2, 3 and 4. Sets of elements of , for example \, are subsets o ...

***

Ur-element In set theory, a branch of mathematics, an urelement or ur-element (from the German prefix ''ur-'', 'primordial') is an object that is not a set, but that may be an element of a set. It is also referred to as an atom or individual. Theory There ...

** Singleton (mathematics) ** Simple theorems in the algebra of sets ** Algebra of sets **

Power set In mathematics, the power set (or powerset) of a set is the set of all subsets of , including the empty set and itself. In axiomatic set theory (as developed, for example, in the ZFC axioms), the existence of the power set of any set is post ...

** Empty set **

Non-empty set In mathematics, the empty set is the unique set having no elements; its size or cardinality (count of elements in a set) is zero. Some axiomatic set theories ensure that the empty set exists by including an axiom of empty set, while in other ...

Empty function In mathematics, a function from a set to a set assigns to each element of exactly one element of .; the words map, mapping, transformation, correspondence, and operator are often used synonymously. The set is called the domain of the functi ...

Universe (mathematics) In mathematics, and particularly in set theory, category theory, type theory, and the foundations of mathematics, a universe is a collection that contains all the entities one wishes to consider in a given situation. In set theory, universes ar ...

* Axiomatization *

Axiomatic system In mathematics and logic, an axiomatic system is any set of axioms from which some or all axioms can be used in conjunction to logically derive theorems. A theory is a consistent, relatively-self-contained body of knowledge which usually contains ...

Axiom schema In mathematical logic, an axiom schema (plural: axiom schemata or axiom schemas) generalizes the notion of axiom. Formal definition An axiom schema is a formula in the metalanguage of an axiomatic system, in which one or more schematic variables ap ...

* Axiomatic method *

Formal system A formal system is an abstract structure used for inferring theorems from axioms according to a set of rules. These rules, which are used for carrying out the inference of theorems from axioms, are the logical calculus of the formal system. A form ...

Mathematical proof A mathematical proof is an inferential argument for a mathematical statement, showing that the stated assumptions logically guarantee the conclusion. The argument may use other previously established statements, such as theorems; but every proo ...

** Direct proof **

Reductio ad absurdum In logic, (Latin for "reduction to absurdity"), also known as (Latin for "argument to absurdity") or ''apagogical arguments'', is the form of argument that attempts to establish a claim by showing that the opposite scenario would lead to absu ...

Proof by exhaustion Proof by exhaustion, also known as proof by cases, proof by case analysis, complete induction or the brute force method, is a method of mathematical proof in which the statement to be proved is split into a finite number of cases or sets of equiv ...

Constructive proof In mathematics, a constructive proof is a method of proof that demonstrates the existence of a mathematical object by creating or providing a method for creating the object. This is in contrast to a non-constructive proof (also known as an existenc ...

Nonconstructive proof In mathematics, a constructive proof is a method of proof that demonstrates the existence of a mathematical object by creating or providing a method for creating the object. This is in contrast to a non-constructive proof (also known as an existenc ...

* Tautology *

Consistency proof In classical deductive logic, a consistent theory is one that does not lead to a logical contradiction. The lack of contradiction can be defined in either semantic or syntactic terms. The semantic definition states that a theory is consistent ...

Arithmetization of analysis The arithmetization of analysis was a research program in the foundations of mathematics carried out in the second half of the 19th century. History Kronecker originally introduced the term ''arithmetization of analysis'', by which he meant its c ...

Foundations of mathematics 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 mathe ...

Formal language In logic, mathematics, computer science, and linguistics, a formal language consists of words whose letters are taken from an alphabet and are well-formed according to a specific set of rules. The alphabet of a formal language consists of sy ...

*''

Principia Mathematica The ''Principia Mathematica'' (often abbreviated ''PM'') is a three-volume work on the foundations of mathematics written by mathematician–philosophers Alfred North Whitehead and Bertrand Russell and published in 1910, 1912, and 1913. ...

'' *

Hilbert's program In mathematics, Hilbert's program, formulated by German mathematician David Hilbert in the early part of the 20th century, was a proposed solution to the foundational crisis of mathematics, when early attempts to clarify the foundations of mathema ...

* Impredicative *

Definable real number Informally, a definable real number is a real number that can be uniquely specified by its description. The description may be expressed as a construction or as a formula of a formal language. For example, the positive square root of 2, \sqrt, ca ...

* Algebraic logic ** Boolean algebra (logic) *

Dialectica space Dialectica spaces are a categorical way of constructing models of linear logic. They were introduced by Valeria de Paiva, Martin Hyland's student, in her doctoral thesis, as a way of modeling both linear logic and Gödel's Dialectica interpretat ...

categorical logic __NOTOC__ Categorical logic is the branch of mathematics in which tools and concepts from category theory are applied to the study of mathematical logic. It is also notable for its connections to theoretical computer science. In broad terms, categ ...

Model theory

* Finite model theory **

Descriptive complexity theory Descriptive complexity is a branch of computational complexity theory and of finite model theory that characterizes complexity classes by the type of logic needed to express the languages in them. For example, PH, the union of all complexity clas ...

** Model checking ** Trakhtenbrot's theorem * Computable model theory ** Tarski's exponential function problem **

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

* Institutional model theory ** Institution (computer science) *

Non-standard analysis The history of calculus is fraught with philosophical debates about the meaning and logical validity of fluxions or infinitesimal numbers. The standard way to resolve these debates is to define the operations of calculus using epsilon–delta ...

** Non-standard calculus **

Hyperinteger In nonstandard analysis, a hyperinteger ''n'' is a hyperreal number that is equal to its own integer part. A hyperinteger may be either finite or infinite. A finite hyperinteger is an ordinary integer. An example of an infinite hyperinteger is g ...

Hyperreal number In mathematics, the system of hyperreal numbers is a way of treating infinite and infinitesimal (infinitely small but non-zero) quantities. The hyperreals, or nonstandard reals, *R, are an extension of the real numbers R that contains numbers ...

Transfer principle In model theory, a transfer principle states that all statements of some language that are true for some structure are true for another structure. One of the first examples was the Lefschetz principle, which states that any sentence in the first- ...

** Overspill ** Elementary Calculus: An Infinitesimal Approach ** Criticism of non-standard analysis ** Standard part function *

Set theory Set theory is the branch of mathematical logic that studies sets, which can be informally described as collections of objects. Although objects of any kind can be collected into a set, set theory, as a branch of mathematics, is mostly conce ...

Forcing (mathematics) In the mathematical discipline of set theory, forcing is a technique for proving consistency and independence results. It was first used by Paul Cohen in 1963, to prove the independence of the axiom of choice and the continuum hypothesis from Ze ...

*** Boolean-valued model *

Kripke semantics Kripke semantics (also known as relational semantics or frame semantics, and often confused with possible world semantics) is a formal semantics for non-classical logic systems created in the late 1950s and early 1960s by Saul Kripke and André Jo ...

General frame In logic, general frames (or simply frames) are Kripke frames with an additional structure, which are used to model modal and intermediate logics. The general frame semantics combines the main virtues of Kripke semantics and algebraic semantics: ...

Predicate logic First-order logic—also known as predicate logic, quantificational logic, and first-order predicate calculus—is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quantifie ...

First-order logic First-order logic—also known as predicate logic, quantificational logic, and first-order predicate calculus—is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quantifie ...

***

Infinitary logic An infinitary logic is a logic that allows infinitely long statements and/or infinitely long proofs. Some infinitary logics may have different properties from those of standard first-order logic. In particular, infinitary logics may fail to be co ...

***

Many-sorted logic Many-sorted logic can reflect formally our intention not to handle the universe as a homogeneous collection of objects, but to partition it in a way that is similar to types in typeful programming. Both functional and assertive " parts of speech ...

Higher-order logic mathematics and logic, a higher-order logic is a form of predicate logic that is distinguished from first-order logic by additional quantifiers and, sometimes, stronger semantics. Higher-order logics with their standard semantics are more express ...

*** Lindström quantifier ***

Second-order logic In logic and mathematics, second-order logic is an extension of first-order logic, which itself is an extension of propositional logic. Second-order logic is in turn extended by higher-order logic and type theory. First-order logic quantifies on ...

Soundness theorem In logic or, more precisely, deductive reasoning, an argument is sound if it is both valid in form and its premises are true. Soundness also has a related meaning in mathematical logic, wherein logical systems are sound if and only if every formul ...

Gödel's completeness theorem Gödel's completeness theorem is a fundamental theorem in mathematical logic that establishes a correspondence between semantic truth and syntactic provability in first-order logic. The completeness theorem applies to any first-order theory: ...

Original proof of Gödel's completeness theorem The proof of Gödel's completeness theorem given by Kurt Gödel in his doctoral dissertation of 1929 (and a shorter version of the proof, published as an article in 1930, titled "The completeness of the axioms of the functional calculus of logic" ( ...

Compactness theorem 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 (but generally ...

* Löwenheim–Skolem theorem **

Skolem's paradox 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 ...

* Gödel's incompleteness theorems *

Structure (mathematical logic) In universal algebra and in model theory, a structure consists of a set along with a collection of finitary operations and relations that are defined on it. Universal algebra studies structures that generalize the algebraic structures such as g ...

Interpretation (logic) An interpretation is an assignment of meaning to the symbols of a formal language. Many formal languages used in mathematics, logic, and theoretical computer science are defined in solely syntactic terms, and as such do not have any meaning un ...

* Substructure (mathematics) * Elementary substructure ** Skolem hull * Non-standard model * Atomic model (mathematical logic) * Prime model *

Saturated model In mathematical logic, and particularly in its subfield model theory, a saturated model ''M'' is one that realizes as many complete types as may be "reasonably expected" given its size. For example, an ultrapower model of the hyperreals is \ ...

* Existentially closed model *

Ultraproduct The ultraproduct is a mathematical construction that appears mainly in abstract algebra and mathematical logic, in particular in model theory and set theory. An ultraproduct is a quotient of the direct product of a family of structures. All factor ...

* Age (model theory) ** Amalgamation property ** Hrushovski construction * Potential isomorphism *

Theory (mathematical logic) In mathematical logic, a theory (also called a formal theory) is a set of sentences in a formal language. In most scenarios, a deductive system is first understood from context, after which an element \phi\in T of a deductively closed theory T is ...

Complete theory In mathematical logic, a theory is complete if it is consistent and for every closed formula in the theory's language, either that formula or its negation is provable. That is, for every sentence \varphi, the theory T contains the sentence or it ...

*** Vaught's test **

Morley's categoricity theorem In mathematical logic, a theory is categorical if it has exactly one model ( up to isomorphism). Such a theory can be viewed as ''defining'' its model, uniquely characterizing the model's structure. In first-order logic, only theories with a ...

***

Stability spectrum In model theory, a branch of mathematical logic, a complete theory, complete first-order theory ''T'' is called stable in λ (an infinite cardinal number), if the Type (model theory)#Stone spaces, Stone space of every structure (mathematical logic), ...

**** Morley rank **** Stable theory ***** Forking extension *****

Strongly minimal theory In model theory—a branch of mathematical logic—a minimal structure is an infinite one-sorted structure such that every subset of its domain that is definable with parameters is either finite or cofinite. A strongly minimal theory is ...

***** Stable group ****** Tame group *** o-minimal theory ***

Weakly o-minimal structure In model theory, a weakly o-minimal structure is a model-theoretic structure whose definable sets in the domain are just finite unions of convex sets. Definition A linearly ordered structure, ''M'', with language ''L'' including an ordering rel ...

***

C-minimal theory In model theory, a branch of mathematical logic, a C-minimal theory is a theory that is "minimal" with respect to a ternary relation ''C'' with certain properties. Algebraically closed fields with a (Krull) valuation are perhaps the most important ...

***

Spectrum of a theory In model theory, a branch of mathematical logic, the spectrum of a theory is given by the number of isomorphism classes of models in various cardinalities. More precisely, for any complete theory ''T'' in a language we write ''I''(''T'', ''κ'' ...

**** Vaught conjecture **

Model complete theory In model theory, a first-order theory is called model complete if every embedding of its models is an elementary embedding. Equivalently, every first-order formula is equivalent to a universal formula. This notion was introduced by Abraham Robinson ...

List of first-order theories In first-order logic, a first-order theory is given by a set of axioms in some language. This entry lists some of the more common examples used in model theory and some of their properties. Preliminaries For every natural mathematical structure ...

Conservative extension In mathematical logic, a conservative extension is a supertheory of a theory which is often convenient for proving theorems, but proves no new theorems about the language of the original theory. Similarly, a non-conservative extension is a superthe ...

** Elementary class ***

Pseudoelementary class In logic, a pseudoelementary class is a class of structures derived from an elementary class (one definable in first-order logic) by omitting some of its sorts and relations. It is the mathematical logic counterpart of the notion in category theory ...

***

Strength (mathematical logic) The relative strength of two systems of formal logic can be defined via model theory. Specifically, a logic \alpha is said to be as strong as a logic \beta if every elementary class in \beta is an elementary class in \alpha.Heinz-Dieter Ebbinghaus ...

Differentially closed field In mathematics, a differential field ''K'' is differentially closed if every finite system of differential equations with a solution in some differential field extending ''K'' already has a solution in ''K''. This concept was introduced by . Differ ...

* Exponential field * Ax–Grothendieck theorem * Ax–Kochen theorem *

* Non-standard model of arithmetic *

First-order arithmetic In first-order logic, a first-order theory is given by a set of axioms in some language. This entry lists some of the more common examples used in model theory and some of their properties. Preliminaries For every natural mathematical structure ...

Second-order arithmetic In mathematical logic, second-order arithmetic is a collection of axiomatic systems that formalize the natural numbers and their subsets. It is an alternative to axiomatic set theory as a foundation for much, but not all, of mathematics. A precur ...

Presburger arithmetic Presburger arithmetic is the first-order theory of the natural numbers with addition, named in honor of Mojżesz Presburger, who introduced it in 1929. The signature of Presburger arithmetic contains only the addition operation and equality, omit ...

* Wilkie's theorem *

Functional predicate In formal logic and related branches of mathematics, a functional predicate, or function symbol, is a logical symbol that may be applied to an object term to produce another object term. Functional predicates are also sometimes called mappings, but ...

T-schema The T-schema ("truth schema", not to be confused with " Convention T") is used to check if an inductive definition of truth is valid, which lies at the heart of any realisation of Alfred Tarski's semantic theory of truth. Some authors refer to it ...

* Back-and-forth method * Barwise compactness theorem *

Skolemization In mathematical logic, a formula of first-order logic is in Skolem normal form if it is in prenex normal form with only universal first-order quantifiers. Every first-order formula may be converted into Skolem normal form while not changing its ...

* Lindenbaum–Tarski algebra *

Löb's theorem In mathematical logic, Löb's theorem states that in Peano arithmetic (PA) (or any formal system including PA), for any formula ''P'', if it is provable in PA that "if ''P'' is provable in PA then ''P'' is true", then ''P'' is provable in PA. If Pr ...

Arithmetical set In mathematical logic, an arithmetical set (or arithmetic set) is a set of natural numbers that can be defined by a formula of first-order Peano arithmetic. The arithmetical sets are classified by the arithmetical hierarchy. The definition can be ...

Definable set In mathematical logic, a definable set is an ''n''-ary relation on the domain of a structure whose elements satisfy some formula in the first-order language of that structure. A set can be defined with or without parameters, which are elements ...

Ehrenfeucht–Fraïssé game In the mathematical discipline of model theory, the Ehrenfeucht–Fraïssé game (also called back-and-forth games) is a technique based on game semantics for determining whether two structures are elementarily equivalent. The main application of ...

Herbrand interpretation In mathematical logic, a Herbrand interpretation is an interpretation in which all constants and function symbols are assigned very simple meanings. Specifically, every constant is interpreted as itself, and every function symbol is interpreted a ...

Herbrand structure In first-order logic, a Herbrand structure ''S'' is a structure over a vocabulary σ that is defined solely by the syntactical properties of σ. The idea is to take the symbols of terms as their values, e.g. the denotation of a constant symbol ' ...

* Imaginary element * Indiscernibles *

Interpretation (model theory) In model theory, interpretation of a structure ''M'' in another structure ''N'' (typically of a different signature) is a technical notion that approximates the idea of representing ''M'' inside ''N''. For example every reduct or definitional exp ...

/ Interpretable structure * Pregeometry (model theory) *

Quantifier elimination Quantifier elimination is a concept of simplification used in mathematical logic, model theory, and theoretical computer science. Informally, a quantified statement "\exists x such that \ldots" can be viewed as a question "When is there an x such t ...

Reduct In universal algebra and in model theory, a reduct of an algebraic structure is obtained by omitting some of the operations and relations of that structure. The opposite of "reduct" is "expansion." Definition Let ''A'' be an algebraic struc ...

* Signature (logic) *

Skolem normal form In mathematical logic, a formula of first-order logic is in Skolem normal form if it is in prenex normal form with only universal first-order quantifiers. Every first-order formula may be converted into Skolem normal form while not changing i ...

* Type (model theory) * Zariski geometry

Set theory

* Algebra of sets *

Axiom of choice In mathematics, the axiom of choice, or AC, is an axiom of set theory equivalent to the statement that ''a Cartesian product of a collection of non-empty sets is non-empty''. Informally put, the axiom of choice says that given any collection ...

Axiom of countable choice The axiom of countable choice or axiom of denumerable choice, denoted ACω, is an axiom of set theory that states that every countable collection of non-empty sets must have a choice function. That is, given a function ''A'' with domain N (where ...

** Axiom of dependent choice ** Zorn's lemma * Boolean algebra (structure) * Boolean-valued model *

Burali-Forti paradox In set theory, a field of mathematics, the Burali-Forti paradox demonstrates that constructing "the set of all ordinal numbers" leads to a contradiction and therefore shows an antinomy in a system that allows its construction. It is named after Ces ...

* Cantor's back-and-forth method *

Cantor's diagonal argument In set theory, Cantor's diagonal argument, also called the diagonalisation argument, the diagonal slash argument, the anti-diagonal argument, the diagonal method, and Cantor's diagonalization proof, was published in 1891 by Georg Cantor as a m ...

Cantor's first uncountability proof Cantor's first set theory article contains Georg Cantor's first theorems of transfinite set theory, which studies infinite sets and their properties. One of these theorems is his "revolutionary discovery" that the set of all real numbers is unco ...

Cantor's theorem In mathematical set theory, Cantor's theorem is a fundamental result which states that, for any set A, the set of all subsets of A, the power set of A, has a strictly greater cardinality than A itself. For finite sets, Cantor's theorem can be ...

* Cantor–Bernstein–Schroeder theorem * Cardinality **

Aleph number In mathematics, particularly in set theory, the aleph numbers are a sequence of numbers used to represent the cardinality (or size) of infinite sets that can be well-ordered. They were introduced by the mathematician Georg Cantor and are named a ...

***

Aleph-null In mathematics, particularly in set theory, the aleph numbers are a sequence of numbers used to represent the cardinality (or size) of infinite sets that can be well-ordered. They were introduced by the mathematician Georg Cantor and are named af ...

*** Aleph-one **

Beth number In mathematics, particularly in set theory, the beth numbers are a certain sequence of infinite cardinal numbers (also known as transfinite numbers), conventionally written \beth_0,\ \beth_1,\ \beth_2,\ \beth_3,\ \dots, where \beth is the second H ...

Cardinal number In mathematics, cardinal numbers, or cardinals for short, are a generalization of the natural numbers used to measure the cardinality (size) of sets. The cardinality of a finite set is a natural number: the number of elements in the set. T ...

Hartogs number In mathematics, specifically in axiomatic set theory, a Hartogs number is an ordinal number associated with a set. In particular, if ''X'' is any set, then the Hartogs number of ''X'' is the least ordinal α such that there is no injection from � ...

* Cartesian product * Class (set theory) * Complement (set theory) *

Complete Boolean algebra In mathematics, a complete Boolean algebra is a Boolean algebra in which every subset has a supremum (least upper bound). Complete Boolean algebras are used to construct Boolean-valued models of set theory in the theory of forcing. Every Boolea ...

Continuum (set theory) In the mathematical field of set theory, the continuum means the real numbers, or the corresponding (infinite) cardinal number, denoted by \mathfrak. Georg Cantor proved that the cardinality \mathfrak is larger than the smallest infinity, namely, ...

Suslin's problem In mathematics, Suslin's problem is a question about totally ordered sets posed by and published posthumously. It has been shown to be independent of the standard axiomatic system of set theory known as ZFC: showed that the statement can neit ...

Continuum hypothesis In mathematics, the continuum hypothesis (abbreviated CH) is a hypothesis about the possible sizes of infinite sets. It states that or equivalently, that In Zermelo–Fraenkel set theory with the axiom of choice (ZFC), this is equivalent to ...

* Countable set * Descriptive set theory **

Analytic set In the mathematical field of descriptive set theory, a subset of a Polish space X is an analytic set if it is a continuous image of a Polish space. These sets were first defined by and his student . Definition There are several equivalent ...

Analytical hierarchy In mathematical logic and descriptive set theory, the analytical hierarchy is an extension of the arithmetical hierarchy. The analytical hierarchy of formulas includes formulas in the language of second-order arithmetic, which can have quantifiers ...

Borel equivalence relation In mathematics, a Borel equivalence relation on a Polish space ''X'' is an equivalence relation on ''X'' that is a Borel subset of ''X'' × ''X'' (in the product topology). Formal definition Given Borel equivalence relations ''E'' and '' ...

** Infinity-Borel set ** Lightface analytic game **

Perfect set property In descriptive set theory, a subset of a Polish space has the perfect set property if it is either countable or has a nonempty perfect subset (Kechris 1995, p. 150). Note that having the perfect set property is not the same as being a p ...

Polish space In the mathematical discipline of general topology, a Polish space is a separable completely metrizable topological space; that is, a space homeomorphic to a complete metric space that has a countable dense subset. Polish spaces are so named be ...

** Prewellordering ** Projective set **

Property of Baire A subset A of a topological space X has the property of Baire (Baire property, named after René-Louis Baire), or is called an almost open set, if it differs from an open set by a meager set; that is, if there is an open set U\subseteq X such th ...

** Uniformization (set theory) ** Universally measurable set * Determinacy ** AD+ **

Axiom of determinacy In mathematics, the axiom of determinacy (abbreviated as AD) is a possible axiom for set theory introduced by Jan Mycielski and Hugo Steinhaus in 1962. It refers to certain two-person topological games of length ω. AD states that every game of ...

** Axiom of projective determinacy **

Axiom of real determinacy In mathematics, the axiom of real determinacy (abbreviated as ADR) is an axiom in set theory. It states the following: The axiom of real determinacy is a stronger version of the axiom of determinacy (AD), which makes the same statement about gam ...

* Empty set *

Fuzzy set In mathematics, fuzzy sets (a.k.a. uncertain sets) are sets whose elements have degrees of membership. Fuzzy sets were introduced independently by Lotfi A. Zadeh in 1965 as an extension of the classical notion of set. At the same time, defined ...

* Internal set theory * Intersection (set theory) * L *

L(R) In set theory, L(R) (pronounced L of R) is the smallest transitive inner model of ZF containing all the ordinals and all the reals. Construction It can be constructed in a manner analogous to the construction of L (that is, Gödel's constructi ...

Large cardinal property In the mathematical field of set theory, a large cardinal property is a certain kind of property of transfinite cardinal numbers. Cardinals with such properties are, as the name suggests, generally very "large" (for example, bigger than the least ...

Musical set theory Musical set theory provides concepts for categorizing musical objects and describing their relationships. Howard Hanson first elaborated many of the concepts for analyzing tonal music. Other theorists, such as Allen Forte, further developed th ...

* Ordinal number ** Infinite descending chain **

Limit ordinal In set theory, a limit ordinal is an ordinal number that is neither zero nor a successor ordinal. Alternatively, an ordinal λ is a limit ordinal if there is an ordinal less than λ, and whenever β is an ordinal less than λ, then there exists a ...

Successor ordinal In set theory, the successor of an ordinal number ''α'' is the smallest ordinal number greater than ''α''. An ordinal number that is a successor is called a successor ordinal. Properties Every ordinal other than 0 is either a successor ordin ...

Transfinite induction Transfinite induction is an extension of mathematical induction to well-ordered sets, for example to sets of ordinal numbers or cardinal numbers. Its correctness is a theorem of ZFC. Induction by cases Let P(\alpha) be a property defined for ...

*** ∈-induction ** Well-founded set **

Well-order In mathematics, a well-order (or well-ordering or well-order relation) on a set ''S'' is a total order on ''S'' with the property that every non-empty subset of ''S'' has a least element in this ordering. The set ''S'' together with the well-or ...

Russell's paradox In mathematical logic, Russell's paradox (also known as Russell's antinomy) is a set-theoretic paradox discovered by the British philosopher and mathematician Bertrand Russell in 1901. Russell's paradox shows that every set theory that contains ...

Alternative set theory In a general sense, an alternative set theory is any of the alternative mathematical approaches to the concept of set and any alternative to the de facto standard set theory described in axiomatic set theory by the axioms of Zermelo–Fraenkel set ...

** Axiomatic set theory **

Kripke–Platek set theory with urelements The Kripke–Platek set theory with urelements (KPU) is an axiom system for set theory with urelements, based on the traditional (urelement-free) Kripke–Platek set theory. It is considerably weaker than the (relatively) familiar system ZFU. The ...

** Morse–Kelley set theory ** Naive set theory ** New Foundations **

Positive set theory In mathematical logic, positive set theory is the name for a class of alternative set theories in which the axiom of comprehension holds for at least the positive formulas \phi (the smallest class of formulas containing atomic membership and equal ...

Zermelo–Fraenkel set theory In set theory, Zermelo–Fraenkel set theory, named after mathematicians Ernst Zermelo and Abraham Fraenkel, is an axiomatic system that was proposed in the early twentieth century in order to formulate a theory of sets free of paradoxes such ...

Zermelo set theory Zermelo set theory (sometimes denoted by Z-), as set out in a seminal paper in 1908 by Ernst Zermelo, is the ancestor of modern Zermelo–Fraenkel set theory (ZF) and its extensions, such as von Neumann–Bernays–Gödel set theory (NBG). It be ...

Set (mathematics) A set is the mathematical model for a collection of different things; a set contains '' elements'' or ''members'', which can be mathematical objects of any kind: numbers, symbols, points in space, lines, other geometrical shapes, variables, or ...

* Simple theorems in the algebra of sets * Subset * Θ (set theory) *

Tree (descriptive set theory) In descriptive set theory, a tree on a set X is a collection of finite sequences of elements of X such that every prefix of a sequence in the collection also belongs to the collection. Definitions Trees The collection of all finite sequences of ...

Tree (set theory) In set theory, a tree is a partially ordered set (''T'', <) such that for each ''t'' ∈ ''T'', the set is well-ordered by the relation <. Frequently tre ...

Union (set theory) In set theory, the union (denoted by ∪) of a collection of sets is the set of all elements in the collection. It is one of the fundamental operations through which sets can be combined and related to each other. A refers to a union of ze ...

Von Neumann universe In set theory and related branches of mathematics, the von Neumann universe, or von Neumann hierarchy of sets, denoted by ''V'', is the class of hereditary well-founded sets. This collection, which is formalized by Zermelo–Fraenkel set theory (ZF ...

* Zero sharp

Descriptive set theory

Large cardinals

* Almost Ramsey cardinal *

Erdős cardinal In mathematics, an Erdős cardinal, also called a partition cardinal is a certain kind of large cardinal number introduced by . The Erdős cardinal is defined to be the least cardinal such that for every function there is a set of order type tha ...

* Extendible cardinal *

Huge cardinal In mathematics, a cardinal number κ is called huge if there exists an elementary embedding ''j'' : ''V'' → ''M'' from ''V'' into a transitive inner model ''M'' with critical point κ and :^M \subset M.\! Here, ''αM'' is the class of al ...

* Hyper-Woodin cardinal *

Inaccessible cardinal In set theory, an uncountable cardinal is inaccessible if it cannot be obtained from smaller cardinals by the usual operations of cardinal arithmetic. More precisely, a cardinal is strongly inaccessible if it is uncountable, it is not a sum of ...

Ineffable cardinal In the mathematics of transfinite numbers, an ineffable cardinal is a certain kind of large cardinal number, introduced by . In the following definitions, \kappa will always be a regular uncountable cardinal number. A cardinal number \kappa is ...

* Mahlo cardinal *

Measurable cardinal In mathematics, a measurable cardinal is a certain kind of large cardinal number. In order to define the concept, one introduces a two-valued measure on a cardinal , or more generally on any set. For a cardinal , it can be described as a subdivisi ...

* N-huge cardinal *

Ramsey cardinal In mathematics, a Ramsey cardinal is a certain kind of large cardinal number introduced by and named after Frank P. Ramsey, whose theorem establishes that ω enjoys a certain property that Ramsey cardinals generalize to the uncountable case. L ...

* Rank-into-rank * Remarkable cardinal * Shelah cardinal *

Strong cardinal In set theory, a strong cardinal is a type of large cardinal. It is a weakening of the notion of a supercompact cardinal. Formal definition If λ is any ordinal, κ is λ-strong means that κ is a cardinal number and ther ...

* Strongly inaccessible cardinal * Subtle cardinal * Supercompact cardinal * Superstrong cardinal * Totally indescribable cardinal *

Weakly compact cardinal In mathematics, a weakly compact cardinal is a certain kind of cardinal number introduced by ; weakly compact cardinals are large cardinals, meaning that their existence cannot be proven from the ZFC, standard axioms of set theory. (Tarski original ...

* Weakly hyper-Woodin cardinal * Weakly inaccessible cardinal * Woodin cardinal *

Unfoldable cardinal In mathematics, an unfoldable cardinal is a certain kind of large cardinal number. Formally, a cardinal number κ is λ-unfoldable if and only if for every inner model, transitive model ''M'' of cardinality κ of ZFC-minus-power set such that κ is ...

Recursion theory

Entscheidungsproblem In mathematics and computer science, the ' (, ) 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 state ...

Decision problem In computability theory and computational complexity theory, a decision problem is a computational problem that can be posed as a yes–no question of the input values. An example of a decision problem is deciding by means of an algorithm wheth ...

Decidability (logic) In logic, a true/false decision problem is decidable if there exists an effective method for deriving the correct answer. Zeroth-order logic (propositional logic) is decidable, whereas first-order and higher-order logic are not. Logical systems ar ...

* Church-Turing thesis *

Computable function Computable functions are the basic objects of study in computability theory. Computable functions are the formalized analogue of the intuitive notion of algorithms, in the sense that a function is computable if there exists an algorithm that can do ...

Algorithm In mathematics and computer science, an algorithm () is a finite sequence of rigorous instructions, typically used to solve a class of specific problems or to perform a computation. Algorithms are used as specifications for performing ...

Recursion Recursion (adjective: ''recursive'') occurs when a thing is defined in terms of itself or of its type. Recursion is used in a variety of disciplines ranging from linguistics to logic. The most common application of recursion is in mathemati ...

Primitive recursive function In computability theory, a primitive recursive function is roughly speaking a function that can be computed by a computer program whose loops are all "for" loops (that is, an upper bound of the number of iterations of every loop can be determined ...

** Mu operator ** Ackermann function **

Turing machine A Turing machine is a mathematical model of computation describing an abstract machine that manipulates symbols on a strip of tape according to a table of rules. Despite the model's simplicity, it is capable of implementing any computer algori ...

Halting problem In computability theory, the halting problem is the problem of determining, from a description of an arbitrary computer program and an input, whether the program will finish running, or continue to run forever. Alan Turing proved in 1936 that a ...

** Computability theory, computation **

Herbrand Universe In first-order logic, a Herbrand structure ''S'' is a structure over a vocabulary σ that is defined solely by the syntactical properties of σ. The idea is to take the symbols of terms as their values, e.g. the denotation of a constant symbol '' ...

** Markov algorithm ** Lambda calculus *** Church-Rosser theorem ***

Calculus of constructions In mathematical logic and computer science, the calculus of constructions (CoC) is a type theory created by Thierry Coquand. It can serve as both a typed programming language and as constructive foundation for mathematics. For this second reason, ...

** Combinatory logic **

Post correspondence problem The Post correspondence problem is an undecidable decision problem that was introduced by Emil Post in 1946. Because it is simpler than the halting problem and the ''Entscheidungsproblem'' it is often used in proofs of undecidability. Definiti ...

* Kleene's recursion theorem *

Recursively enumerable set In computability theory, a set ''S'' of natural numbers is called computably enumerable (c.e.), recursively enumerable (r.e.), semidecidable, partially decidable, listable, provable or Turing-recognizable if: *There is an algorithm such that th ...

Recursively enumerable language In mathematics, logic and computer science, a formal language is called recursively enumerable (also recognizable, partially decidable, semidecidable, Turing-acceptable or Turing-recognizable) if it is a recursively enumerable subset in the set o ...

Decidable language In mathematics, logic and computer science, a formal language (a set of finite sequences of symbols taken from a fixed alphabet) is called recursive if it is a recursive subset of the set of all possible finite sequences over the alphabet of the ...

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

Rice's theorem In computability theory, Rice's theorem states that all non-trivial semantic properties of programs are undecidable. A semantic property is one about the program's behavior (for instance, does the program terminate for all inputs), unlike a synta ...

Post's theorem In computability theory Post's theorem, named after Emil Post, describes the connection between the arithmetical hierarchy and the Turing degrees. Background The statement of Post's theorem uses several concepts relating to definability and ...

Turing degree In computer science and mathematical logic the Turing degree (named after Alan Turing) or degree of unsolvability of a set of natural numbers measures the level of algorithmic unsolvability of the set. Overview The concept of Turing degree is fund ...

Effective results in number theory For historical reasons and in order to have application to the solution of Diophantine equations, results in number theory have been scrutinised more than in other branches of mathematics to see if their content is effectively computable. Where ...

Diophantine set In mathematics, a Diophantine equation is an equation of the form ''P''(''x''1, ..., ''x'j'', ''y''1, ..., ''y'k'') = 0 (usually abbreviated ''P''(', ') = 0) where ''P''(', ') is a polynomial with integer coefficients, where ''x''1, ..., '' ...

* Matiyasevich's theorem *

Word problem for groups In mathematics, especially in the area of abstract algebra known as combinatorial group theory, the word problem for a finitely generated group ''G'' is the algorithmic problem of deciding whether two words in the generators represent the same el ...

Arithmetical hierarchy In mathematical logic, the arithmetical hierarchy, arithmetic hierarchy or Kleene–Mostowski hierarchy (after mathematicians Stephen Cole Kleene and Andrzej Mostowski) classifies certain sets based on the complexity of formulas that define th ...

* Subrecursion theory **

Computational complexity theory In theoretical computer science and mathematics, computational complexity theory focuses on classifying computational problems according to their resource usage, and relating these classes to each other. A computational problem is a task solved ...

** Polynomial time **

Exponential time In computer science, the time complexity is the computational complexity that describes the amount of computer time it takes to run an algorithm. Time complexity is commonly estimated by counting the number of elementary operations performed by t ...

Complexity class In computational complexity theory, a complexity class is a set (mathematics), set of computational problems of related resource-based computational complexity, complexity. The two most commonly analyzed resources are time complexity, time and spa ...

*** Complexity classes P and NP *** Cook's theorem ***

List of complexity classes This is a list of complexity classes in computational complexity theory In theoretical computer science and mathematics, computational complexity theory focuses on classifying computational problems according to their resource usage, and rela ...

***

Polynomial hierarchy In computational complexity theory, the polynomial hierarchy (sometimes called the polynomial-time hierarchy) is a hierarchy of complexity classes that generalize the classes NP and co-NP. Each class in the hierarchy is contained within PSPACE. ...

***

Exponential hierarchy In computational complexity theory, the exponential hierarchy is a hierarchy of complexity classes, which is an exponential time analogue of the polynomial hierarchy. As elsewhere in complexity theory, “exponential” is used in two different me ...

NP-complete In computational complexity theory, a problem is NP-complete when: # it is a problem for which the correctness of each solution can be verified quickly (namely, in polynomial time) and a brute-force search algorithm can find a solution by trying ...

** Time hierarchy theorem **

Space hierarchy theorem In computational complexity theory, the space hierarchy theorems are separation results that show that both deterministic and nondeterministic machines can solve more problems in (asymptotically) more space, subject to certain conditions. For exampl ...

* Natural proof *

Hypercomputation Hypercomputation or super-Turing computation refers to models of computation that can provide outputs that are not Turing-computable. Super-Turing computing, introduced at the early 1990's by Hava Siegelmann, refers to such neurological inspired, b ...

Oracle machine In complexity theory and computability theory, an oracle machine is an abstract machine used to study decision problems. It can be visualized as a Turing machine with a black box, called an oracle, which is able to solve certain problems in a ...

Rózsa Péter Rózsa Péter, born Rózsa Politzer, (17 February 1905 – 16 February 1977) was a Hungarian mathematician and logician. She is best known as the "founding mother of recursion theory". Early life and education Péter was born in Budapest, ...

Alonzo Church Alonzo Church (June 14, 1903 – August 11, 1995) was an American mathematician, computer scientist, logician, philosopher, professor and editor who made major contributions to mathematical logic and the foundations of theoretical computer scien ...

Emil Post Emil Leon Post (; February 11, 1897 – April 21, 1954) was an American mathematician and logician. He is best known for his work in the field that eventually became known as computability theory. Life Post was born in Augustów, Suwałki Gove ...

Alan Turing Alan Mathison Turing (; 23 June 1912 – 7 June 1954) was an English mathematician, computer scientist, logician, cryptanalyst, philosopher, and theoretical biologist. Turing was highly influential in the development of theoretical co ...

Jacques Herbrand Jacques Herbrand (12 February 1908 – 27 July 1931) was a French mathematician. Although he died at age 23, he was already considered one of "the greatest mathematicians of the younger generation" by his professors Helmut Hasse and Richard Coura ...

Haskell Curry Haskell Brooks Curry (; September 12, 1900 – September 1, 1982) was an American mathematician and logician. Curry is best known for his work in combinatory logic. While the initial concept of combinatory logic was based on a single paper by ...

Stephen Cole Kleene Stephen Cole Kleene ( ; January 5, 1909 – January 25, 1994) was an American mathematician. One of the students of Alonzo Church, Kleene, along with Rózsa Péter, Alan Turing, Emil Post, and others, is best known as a founder of the branch of ...

Proof theory

* Metamathematics *

Cut-elimination The cut-elimination theorem (or Gentzen's ''Hauptsatz'') is the central result establishing the significance of the sequent calculus. It was originally proved by Gerhard Gentzen in his landmark 1934 paper "Investigations in Logical Deduction" for ...

* Tarski's undefinability theorem *

Diagonal lemma In mathematical logic, the diagonal lemma (also known as diagonalization lemma, self-reference lemma or fixed point theorem) establishes the existence of self-referential sentences in certain formal theories of the natural numbers—specificall ...

Provability logic Provability logic is a modal logic, in which the box (or "necessity") operator is interpreted as 'it is provable that'. The point is to capture the notion of a proof predicate of a reasonably rich formal theory, such as Peano arithmetic. Examples ...

* Interpretability logic *

Sequent In mathematical logic, a sequent is a very general kind of conditional assertion. : A_1,\,\dots,A_m \,\vdash\, B_1,\,\dots,B_n. A sequent may have any number ''m'' of condition formulas ''Ai'' (called " antecedents") and any number ''n'' of ass ...

Sequent calculus In mathematical logic, sequent calculus is a style of formal logical argumentation in which every line of a proof is a conditional tautology (called a sequent by Gerhard Gentzen) instead of an unconditional tautology. Each conditional tautology i ...

* Analytic proof * Structural proof theory * Self-verifying theories *

Substructural logic In logic, a substructural logic is a logic lacking one of the usual structural rules (e.g. of classical and intuitionistic logic), such as weakening, contraction, exchange or associativity. Two of the more significant substructural logics are r ...

s ** Structural rule *** Weakening *** Contraction ** Linear logic *** Intuitionistic linear logic *** Proof net **

Affine logic Affine logic is a substructural logic whose proof theory rejects the structural rule of contraction. It can also be characterized as linear logic with weakening. The name "affine logic" is associated with linear logic, to which it differs by all ...

** Strict logic **

Relevant logic Relevance logic, also called relevant logic, is a kind of non-classical logic requiring the antecedent and consequent of implications to be relevantly related. They may be viewed as a family of substructural or modal logics. It is generally, but ...

* Proof-theoretic semantics *

Ludics In proof theory, ludics is an analysis of the principles governing inference rules of mathematical logic. Key features of ludics include notion of compound connectives, using a technique known as ''focusing'' or ''focalisation'' (invented by the ...

System F System F (also polymorphic lambda calculus or second-order lambda calculus) is a typed lambda calculus that introduces, to simply typed lambda calculus, a mechanism of universal quantification over types. System F formalizes parametric polymorph ...

Gerhard Gentzen Gerhard Karl Erich Gentzen (24 November 1909 – 4 August 1945) was a German mathematician and logician. He made major contributions to the foundations of mathematics, proof theory, especially on natural deduction and sequent calculus. He died ...

* Gentzen's consistency proof *

Reverse mathematics Reverse mathematics is a program in mathematical logic that seeks to determine which axioms are required to prove theorems of mathematics. Its defining method can briefly be described as "going backwards from the theorems to the axioms", in cont ...

Nonfirstorderizability In formal logic, nonfirstorderizability is the inability of a natural-language statement to be adequately captured by a formula of first-order logic. Specifically, a statement is nonfirstorderizable if there is no formula of first-order logic whic ...

* Interpretability * Weak interpretability * Cointerpretability * Tolerant sequence * Cotolerant sequence *

Deduction theorem In mathematical logic, a deduction theorem is a metatheorem that justifies doing conditional proofs—to prove an implication ''A'' → ''B'', assume ''A'' as an hypothesis and then proceed to derive ''B''—in systems that do not have an ...

Cirquent calculus Cirquent calculus is a proof calculus that manipulates graph-style constructs termed ''cirquents'', as opposed to the traditional tree-style objects such as formulas or sequents. Cirquents come in a variety of forms, but they all share one main c ...

Mathematical constructivism

* Existence theorem *

Intuitionistic logic Intuitionistic logic, sometimes more generally called constructive logic, refers to systems of symbolic logic that differ from the systems used for classical logic by more closely mirroring the notion of constructive proof. In particular, systems ...

Intuitionistic type theory Intuitionistic type theory (also known as constructive type theory, or Martin-Löf type theory) is a type theory and an alternative foundation of mathematics. Intuitionistic type theory was created by Per Martin-Löf, a Swedish mathematician an ...

Type theory In mathematics, logic, and computer science, a type theory is the formal presentation of a specific type system, and in general type theory is the academic study of type systems. Some type theories serve as alternatives to set theory as a fou ...

* Lambda calculus **

Church–Rosser theorem In lambda calculus, the Church–Rosser theorem states that, when applying reduction rules to terms, the ordering in which the reductions are chosen does not make a difference to the eventual result. More precisely, if there are two distinct red ...

Simply typed lambda calculus The simply typed lambda calculus (\lambda^\to), a form of type theory, is a typed interpretation of the lambda calculus with only one type constructor (\to) that builds function types. It is the canonical and simplest example of a typed lambda c ...

Typed lambda calculus A typed lambda calculus is a typed formalism that uses the lambda-symbol (\lambda) to denote anonymous function abstraction. In this context, types are usually objects of a syntactic nature that are assigned to lambda terms; the exact nature of a ...

* Curry–Howard isomorphism *

* Constructivist analysis *

Lambda cube In mathematical logic and type theory, the λ-cube (also written lambda cube) is a framework introduced by Henk Barendregt to investigate the different dimensions in which the calculus of constructions is a generalization of the simply typed ...

* Introduction to topos theory *

LF (logical framework) In logic, a logical framework provides a means to define (or present) a logic as a signature in a higher-order type theory in such a way that provability of a formula in the original logic reduces to a type inhabitation problem in the framework ty ...

* Computability logic * Computable measure theory *

Finitism Finitism is a philosophy of mathematics that accepts the existence only of finite mathematical objects. It is best understood in comparison to the mainstream philosophy of mathematics where infinite mathematical objects (e.g., infinite sets) are ...

* Ultraintuitionism *

Luitzen Egbertus Jan Brouwer Luitzen Egbertus Jan Brouwer (; ; 27 February 1881 – 2 December 1966), usually cited as L. E. J. Brouwer but known to his friends as Bertus, was a Dutch mathematician and philosopher, who worked in topology, set theory, measure theory and compl ...

Modal logic

* Sahlqvist formula * Interior algebra

Theorem provers

First-order resolution In mathematical logic and automated theorem proving, resolution is a rule of inference leading to a refutation complete theorem-proving technique for sentences in propositional logic and first-order logic. For propositional logic, systematically ...

Automated theorem proving Automated theorem proving (also known as ATP or automated deduction) is a subfield of automated reasoning and mathematical logic dealing with proving mathematical theorems by computer programs. Automated reasoning over mathematical proof was a ma ...

* ACL2 theorem prover * E equational theorem prover * Gandalf theorem prover *

HOL theorem prover HOL (Higher Order Logic) denotes a family of interactive theorem proving systems using similar (higher-order) logics and implementation strategies. Systems in this family follow the LCF approach as they are implemented as a library which defin ...

Isabelle theorem prover The Isabelle automated theorem prover is a higher-order logic (HOL) theorem prover, written in Standard ML and Scala. As an LCF-style theorem prover, it is based on a small logical core (kernel) to increase the trustworthiness of proofs withou ...

LCF theorem prover Logic for Computable Functions (LCF) is an interactive automated theorem prover developed at Stanford and Edinburgh by Robin Milner and collaborators in early 1970s, based on the theoretical foundation of logic of computable functions previously ...

* Otter theorem prover * Paradox theorem prover *

Vampire theorem prover Vampire is an automatic theorem prover for first-order classical logic developed in the Department of Computer Science at the University of Manchester. Up to Version 3, it was developed by Andrei Voronkov together with Kryštof Hoder and previo ...

Interactive proof system In computational complexity theory, an interactive proof system is an abstract machine that models computation as the exchange of messages between two parties: a ''prover'' and a ''verifier''. The parties interact by exchanging messages in order t ...

Mizar system The Mizar system consists of a formal language for writing mathematical definitions and proofs, a proof assistant, which is able to mechanically check proofs written in this language, and a library of formalized mathematics, which can be used in ...

QED project The QED manifesto was a proposal for a computer-based database of all mathematical knowledge, strictly formalized and with all proofs having been checked automatically. (Q.E.D. means in Latin, meaning "which was to be demonstrated.") Overview Th ...

Coq Coq is an interactive theorem prover first released in 1989. It allows for expressing mathematical assertions, mechanically checks proofs of these assertions, helps find formal proofs, and extracts a certified program from the constructive proof ...

Discovery systems

* Automated Mathematician * Eurisko

Historical

*''

Begriffsschrift ''Begriffsschrift'' (German for, roughly, "concept-script") is a book on logic by Gottlob Frege, published in 1879, and the formal system set out in that book. ''Begriffsschrift'' is usually translated as ''concept writing'' or ''concept notatio ...

'' *'' Systems of Logic Based on Ordinals'' – Alan Turing's Ph.D. thesis