List of mathematical logic topics
Encyclopedia
This is a list of mathematical logic 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
Algorithm
In mathematics and computer science, an algorithm is an effective method expressed as a finite list of well-defined instructions for calculating a function. Algorithms are used for calculation, data processing, and automated reasoning...

s.

Working foundations

  • Peano axioms
    Peano axioms
    In mathematical logic, the Peano axioms, also known as the Dedekind–Peano axioms or the Peano postulates, are a set of axioms for the natural numbers presented by the 19th century Italian mathematician Giuseppe Peano...

    • Giuseppe Peano
      Giuseppe Peano
      Giuseppe Peano was an Italian mathematician, whose work was of philosophical value. 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 standard axiomatization of the natural numbers is named the Peano axioms in...

  • Mathematical induction
    Mathematical induction
    Mathematical induction is a method of mathematical proof typically used to establish that a given statement is true of all natural numbers...

    • Structural induction
      Structural induction
      Structural induction is a proof method that is used in mathematical logic , computer science, graph theory, and some other mathematical fields. It is a generalization of mathematical induction...

    • Recursive definition
      Recursive definition
      In mathematical logic and computer science, a recursive definition is used to define an object in terms of itself ....

  • Naive set theory
    Naive set theory
    Naive set theory is one of several theories of sets used in the discussion of the foundations of mathematics. The informal content of this naive set theory supports both the aspects of mathematical sets familiar in discrete mathematics , and the everyday usage of set theory concepts in most...

    • Element (mathematics)
      • Ur-element
        Ur-element
        In set theory, a branch of mathematics, an urelement or ur-element is an object which is not a set, but that may be an element of a set...

    • Singleton (mathematics)
    • Simple theorems in the algebra of sets
      Simple theorems in the algebra of sets
      The simple theorems in the algebra of sets are some of the elementary properties of the algebra of union , intersection , and set complement of sets....

    • Algebra of sets
      Algebra of sets
      The algebra of sets develops and describes the basic properties and laws of sets, the set-theoretic operations of union, intersection, and complementation and the relations of set equality and set inclusion...

    • Power set
    • Empty set
      Empty set
      In mathematics, and more specifically set theory, the empty set is the unique set having no elements; its size or cardinality is zero. Some axiomatic set theories assure that the empty set exists by including an axiom of empty set; in other theories, its existence can be deduced...

    • Non-empty set
    • Empty function
      Empty function
      In mathematics, an empty function is a function whose domain is the empty set. For each set A, there is exactly one such empty functionf_A: \varnothing \rightarrow A....

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

  • Axiomatization
  • Axiomatic system
    Axiomatic system
    In mathematics, an axiomatic system is any set of axioms from which some or all axioms can be used in conjunction to logically derive theorems. A mathematical theory consists of an axiomatic system and all its derived theorems...

    • Axiom schema
      Axiom schema
      In mathematical logic, an axiom schema generalizes the notion of axiom.An axiom schema is a formula in the language of an axiomatic system, in which one or more schematic variables appear. These variables, which are metalinguistic constructs, stand for any term or subformula of the system, which...

  • Axiomatic method
  • Formal system
    Formal system
    In formal logic, a formal system consists of a formal language and a set of inference rules, used to derive an expression from one or more other premises that are antecedently supposed or derived . The axioms and rules may be called a deductive apparatus...

  • Mathematical proof
    Mathematical proof
    In mathematics, a proof is a convincing demonstration that some mathematical statement is necessarily true. Proofs are obtained from deductive reasoning, rather than from inductive or empirical arguments. That is, a proof must demonstrate that a statement is true in all cases, without a single...

    • Direct proof
      Direct proof
      In mathematics and logic, a direct proof is a way of showing the truth or falsehood of a given statement by a straightforward combination of established facts, usually existing lemmas and theorems, without making any further assumptions...

    • Reductio ad absurdum
      Reductio ad absurdum
      In logic, proof by contradiction is a form of proof that establishes the truth or validity of a proposition by showing that the proposition's being false would imply a contradiction...

    • Proof by exhaustion
      Proof by exhaustion
      Proof by exhaustion, also known as proof by cases, perfect 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 and each case is checked to see if the proposition in question holds...

    • Constructive proof
      Constructive proof
      In mathematics, a constructive proof is a method of proof that demonstrates the existence of a mathematical object with certain properties by creating or providing a method for creating such an object...

    • Nonconstructive proof
  • Tautology
    Tautology (logic)
    In logic, a tautology is a formula which is true in every possible interpretation. Philosopher Ludwig Wittgenstein first applied the term to redundancies of propositional logic in 1921; it had been used earlier to refer to rhetorical tautologies, and continues to be used in that alternate sense...

  • Consistency proof
    Consistency proof
    In logic, a consistent theory is one that does not contain a contradiction. The lack of contradiction can be defined in either semantic or syntactic terms. The semantic definition states that a theory is consistent if and only if it has a model, i.e. there exists an interpretation under which all...

  • Arithmetization of analysis
    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. Kronecker originally introduced the term arithmetization of analysis, by which he meant its constructivization in the context of the natural numbers...

  • Foundations of mathematics
    Foundations of mathematics
    Foundations of mathematics is a term sometimes used for certain fields of mathematics, such as mathematical logic, axiomatic set theory, proof theory, model theory, type theory and recursion theory...

  • Formal language
    Formal language
    A formal language is a set of words—that is, finite strings of letters, symbols, or tokens that are defined in the language. The set from which these letters are taken is the alphabet over which the language is defined. A formal language is often defined by means of a formal grammar...

  • Principia Mathematica
    Principia Mathematica
    The Principia Mathematica is a three-volume work on the foundations of mathematics, written by Alfred North Whitehead and Bertrand Russell and published in 1910, 1912, and 1913...

  • Hilbert's program
    Hilbert's program
    In mathematics, Hilbert's program, formulated by German mathematician David Hilbert, was a proposed solution to the foundational crisis of mathematics, when early attempts to clarify the foundations of mathematics were found to suffer from paradoxes and inconsistencies...

  • Impredicative
    Impredicative
    In mathematics and logic, impredicativity is the property of a self-referencing definition. More precisely, a definition is said to be impredicative if it invokes the set being defined, or another set which contains the thing being defined.Russell's paradox is a famous example of an impredicative...

  • Definable real number
  • Algebraic logic
    Algebraic logic
    In mathematical logic, algebraic logic is the study of logic presented in an algebraic style.What is now usually called classical algebraic logic focuses on the identification and algebraic description of models appropriate for the study of various logics and connected problems...

    • Boolean algebra (logic)
  • Dialectica space
    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 interpretation—hence the name.Given a category C and a...

  • categorical logic
    Categorical logic
    Categorical logic is a branch of category theory within mathematics, adjacent to mathematical logic but more notable for its connections to theoretical computer science. In broad terms, categorical logic represents both syntax and semantics by a category, and an interpretation by a functor...


Model theory

  • Finite model theory
    Finite model theory
    Finite Model Theory is a subarea of model theory . MT is the branch of mathematical logic which deals with the relation between a formal language and its interpretations . FMT is a restriction of MT to interpretations of finite structures, i.e...

    • Descriptive complexity theory
    • Model checking
      Model checking
      In computer science, model checking refers to the following problem:Given a model of a system, test automatically whether this model meets a given specification....

    • Trakhtenbrot's theorem
      Trakhtenbrot's theorem
      In logic and finite model theory, Trakhtenbrot's theorem states that the problem of validity in the class of all finite models is undecidable. In fact, the class of valid sentences over finite models is not recursively enumerable .- References :* Boolos, Burgess, Jeffrey...

  • Computable model theory
    Computable model theory
    Computable model theory is a branch of model theory which deals with questions of computability as they apply to model-theoretical structures. It was developed almost simultaneously by mathematicians in the West, primarily located in the United States and Australia, and Soviet Russia during the...

    • Tarski's exponential function problem
      Tarski's exponential function problem
      In model theory, Tarski's exponential function problem asks whether the usual theory of the real numbers together with the exponential function is decidable...

    • Undecidable problem
      Undecidable problem
      In computability theory and computational complexity theory, an undecidable problem is a decision problem for which it is impossible to construct a single algorithm that always leads to a correct yes-or-no answer....

  • Institutional model theory
    Institutional model theory
    Institutional model theory generalizes a large portion of first-order model theory to an arbitrary logical system.- Overview :The notion of "logical system" here is formalized as an institution. Institutions constitute a model-oriented meta-theory on logical systems similar to how the theory of...

    • Institution (computer science)
      Institution (computer science)
      The notion of institution has been created by Joseph Goguen and Rod Burstall in the late 1970sin order to deal with the "population explosion among the logical systems used incomputer science"...

  • Non-standard analysis
    Non-standard analysis
    Non-standard analysis is a branch of mathematics that formulates analysis using a rigorous notion of an infinitesimal number.Non-standard analysis was introduced in the early 1960s by the mathematician Abraham Robinson. He wrote:...

    • Non-standard calculus
      Non-standard calculus
      In mathematics, non-standard calculus is the modern application of infinitesimals, in the sense of non-standard analysis, to differential and integral calculus...

    • Hyperinteger
      Hyperinteger
      In non-standard analysis, a hyperinteger N is a hyperreal number equal to its own integer part. A hyperinteger may be either finite or infinite. A finite hyperinteger is an ordinary integer...

    • Hyperreal number
      Hyperreal number
      The system of hyperreal numbers represents a rigorous method of treating the infinite and infinitesimal quantities. The hyperreals, or nonstandard reals, *R, are an extension of the real numbers R that contains numbers greater than anything of the form1 + 1 + \cdots + 1. \, Such a number is...

    • Transfer principle
      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...

    • Overspill
      Overspill
      In non-standard analysis, a branch of mathematics, overspill is a widely used proof technique...

    • Elementary Calculus: An Infinitesimal Approach
      Elementary Calculus: An Infinitesimal Approach
      Elementary Calculus: An Infinitesimal approach is a textbook by H. Jerome Keisler. The subtitle alludes to the infinitesimal numbers of Abraham Robinson's non-standard analysis...

    • Criticism of non-standard analysis
      Criticism of non-standard analysis
      Non-standard analysis and its offshoot, non-standard calculus, have been criticized by several authors. The evaluation of non-standard analysis in the literature has varied greatly...

    • Standard part function
      Standard part function
      In non-standard analysis, the standard part function is a function from the limited hyperreals to the reals, which associates to every hyperreal, the unique real infinitely close to it. As such, it is a mathematical implementation of the historical concept of adequality introduced by Pierre de...

  • Set theory
    Set theory
    Set theory is the branch of mathematics that studies sets, which are collections of objects. Although any type of object can be collected into a set, set theory is applied most often to objects that are relevant to mathematics...

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

      • Boolean valued model
  • Kripke semantics
    Kripke semantics
    Kripke semantics is a formal semantics for non-classical logic systems created in the late 1950s and early 1960s by Saul Kripke. It was first made for modal logics, and later adapted to intuitionistic logic and other non-classical systems...

    • General frame
      General frame
      In logic, general frames are Kripke frames with an additional structure, which are used to model modal and intermediate logics...


  • Predicate logic
    Predicate logic
    In mathematical logic, predicate logic is the generic term for symbolic formal systems like first-order logic, second-order logic, many-sorted logic or infinitary logic. This formal system is distinguished from other systems in that its formulae contain variables which can be quantified...

    • First-order logic
      First-order logic
      First-order logic is a formal logical system used in mathematics, philosophy, linguistics, and computer science. It goes by many names, including: first-order predicate calculus, the lower predicate calculus, quantification theory, and predicate logic...

      • Infinitary logic
        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 compact or complete. Notions of compactness and...

      • Many-sorted logic
        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...

    • Higher-order logic
      Higher-order logic
      In mathematics and logic, a higher-order logic is a form of predicate logic that is distinguished from first-order logic by additional quantifiers and a stronger semantics...

      • Lindström quantifier
        Lindström quantifier
        In mathematical logic, a Lindström quantifier is a generalized polyadic quantifier. They are a generalization of first-order quantifiers, such as the existential quantifier, the universal quantifier, and the counting quantifiers.They were introduced by Per Lindström in 1966.-Generalization of...

      • Second-order logic
        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....


  • Soundness theorem
  • Gödel's completeness theorem
    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. It was first proved by Kurt Gödel in 1929....

    • Original proof of Gödel's completeness theorem
      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 is not easy to read today; it uses concepts and formalism that are outdated and terminology that is often obscure...

  • Compactness theorem
    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...

  • Löwenheim-Skolem theorem
    • Skolem's paradox
      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 was the first to discuss the seemingly contradictory aspects of the theorem, and to discover the relativity of set-theoretic notions now known as...

  • Gödel's incompleteness theorems
    Gödel's incompleteness theorems
    Gödel's incompleteness theorems are two theorems of mathematical logic that establish inherent limitations of all but the most trivial axiomatic systems capable of doing arithmetic. The theorems, proven by Kurt Gödel in 1931, are important both in mathematical logic and in the philosophy of...


  • Structure (mathematical logic)
    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 which are defined on it....

  • Interpretation (logic)
    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 until they are given some interpretation...

  • Substructure
    Substructure
    In mathematical logic, an substructure or subalgebra is a structure whose domain is a subset of that of a bigger structure, and whose functions and relations are the traces of the functions and relations of the bigger structure...

  • Elementary substructure
    Elementary substructure
    In model theory, a field within mathematical logic, two structures M and N of the same signature σ are called elementarily equivalent if they satisfy the same first-order σ-sentences....

    • Skolem hull
  • Non-standard model
    Non-standard model
    In model theory, a discipline within mathematical logic, a non-standard model is a model of a theory that is not isomorphic to the intended model . If the intended model is infinite and the language is first-order, then the Löwenheim-Skolem theorems guarantee the existence of non-standard models...

  • Atomic model (mathematical logic)
  • Prime model
    Prime model
    In mathematics, and in particular model theory, a prime model is a model which is as simple as possible. Specifically, a model P is prime if it admits an elementary embedding into any model M to which it is elementarily equivalent .- Cardinality :In contrast with the notion of saturated model,...

  • Saturated model
    Saturated model
    In mathematical logic, and particularly in its subfield model theory, a saturated model M is one which realizes as many complete types as may be "reasonably expected" given its size...

  • Existentially closed model
    Existentially closed model
    In model theory, a branch of mathematical logic, the notion of an existentially closed model of a theory generalizes the notions of algebraically closed fields , real closed fields , existentially closed groups , and dense linear orders without endpoints In model theory, a branch of mathematical...

  • Ultraproduct
    Ultraproduct
    The ultraproduct is a mathematical construction that appears mainly in abstract algebra and in model theory, a branch of mathematical logic. An ultraproduct is a quotient of the direct product of a family of structures. All factors need to have the same signature...

  • Age (model theory)
    Age (model theory)
    In model theory, the age of a structure A is the class of all finitely generated structures which are embeddable in A . This concept is central in the construction of a Fraïssé limit....

    • Amalgamation property
      Amalgamation property
      In the mathematical field of model theory, the amalgamation property is a property of collections of structures that guarantees, under certain conditions, that two structures in the collection can be regarded as substructures of a larger one....

    • Hrushovski construction
      Hrushovski construction
      In model theory, a branch of mathematical logic, the Hrushovski construction generalizes the Fraïssé limit by working with a notion of strong substructure \leq rather than \subseteq. It can be thought of as a kind of "model-theoretic forcing", where a stable structure is created, called the generic...

  • Potential isomorphism
    Potential isomorphism
    In mathematical logic and in particular in model theory, a potential isomorphism is a collection of finite partial isomorphisms between two models which satisfies certain closure conditions...


  • Theory (mathematical logic)
    Theory (mathematical logic)
    In mathematical logic, a theory is a set of sentences in a formal language. Usually a deductive system is understood from context. An element \phi\in T of a theory T is then called an axiom of the theory, and any sentence that follows from the axioms is called a theorem of the theory. Every axiom...

    • Complete theory
      Complete theory
      In mathematical logic, a theory is complete if it is a maximal consistent set of sentences, i.e., if it is consistent, and none of its proper extensions is consistent...

      • Vaught's test
    • Morley's categoricity theorem
      Morley's categoricity theorem
      In model theory, a branch of mathematical logic, a theory is κ-categorical if it has exactly one model of cardinality κ up to isomorphism....

      • Stability spectrum
        Stability spectrum
        In model theory, a branch of mathematical logic, a complete first-order theory T is called stable in λ , if the Stone space of every model of T of size ≤ λ has itself size ≤ λ. T is called a stable theory if there is no upper bound for the cardinals κ such that T is stable in κ...

        • Morley rank
          Morley rank
          In mathematical logic, Morley rank, introduced by , is a means of measuring the size of a subset of a model of a theory, generalizing the notion of dimension in algebraic geometry.-Definition:Fix a theory T with a model M...

        • Stable theory
          Stable theory
          In model theory, a complete theory is called stable if it does not have too many types. One goal of classification theory is to divide all complete theories into those whose models can be classified and those whose models are too complicated to classify, and to classify all models in the cases...

          • Forking extension
            Forking extension
            In model theory, a forking extension of a type is an extension that is in some sense not free, and a non-forking extension is an extension that is as free as possible. This can be used to extend the notions of linear or algebraic independence to stable theories. These concepts were introduced by S...

          • Strongly minimal theory
            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 a complete theory all models of that are minimal...

          • Stable group
            Stable group
            In model theory, a stable group is a group that is stable in the sense of stability theory.An important class of examples is provided by groups of finite Morley rank .-Examples:...

            • Tame group
              Tame group
              In mathematical group theory, a tame group is a certain kind of group defined in model theory.Formally, we define a bad field as a structure of the form , where K is an algebraically closed field and T is an infinite, proper, distinguished subgroup of K, such that is of finite Morley rank in its...

      • o-minimal theory
        O-minimal theory
        In mathematical logic, and more specifically in model theory, an infinite structure which is totally ordered by In mathematical logic, and more specifically in model theory, an infinite structure which is totally ordered by...

      • Weakly o-minimal structure
        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 relation...

      • C-minimal theory
        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...

      • Spectrum of a theory
        Spectrum of a theory
        In model theory, a branch of mathematical logic, the spectrum of a theoryis given by the number of isomorphism classes of models in various cardinalities. More precisely,...

        • Vaught conjecture
          Vaught conjecture
          The Vaught conjecture is a conjecture in the mathematical field of model theory originally proposed by Robert Lawson Vaught in 1961. It states that the number of countable models of a first-order complete theory in a countable language is finite or ℵ0 or 2ℵ0...

    • Model complete theory
      Model complete theory
      In model theory, a first-order theory is called model complete if every embedding of 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
    • Conservative extension
      Conservative extension
      In mathematical logic, a logical theory T_2 is a conservative extension of a theory T_1 if the language of T_2 extends the language of T_1; every theorem of T_1 is a theorem of T_2; and any theorem of T_2 which is in the language of T_1 is already a theorem of T_1.More generally, if Γ is a set of...

    • Elementary class
      Elementary class
      In the branch of mathematical logic called model theory, an elementary class is a class consisting of all structures satisfying a fixed first-order theory.- Definition :...

      • Pseudoelementary class
        Pseudoelementary class
        In logic, a pseudoelementary class is a class of structures derived from an elementary class by omitting some of its sorts and relations. It is the mathematical logic counterpart of the notion in category theory of a forgetful functor, and in physics of hidden variable theories purporting to...

      • Strength (mathematical logic)

  • Differentially closed field
    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...

  • Exponential field
    Exponential field
    In mathematics, an exponential field is a field that has an extra operation on its elements which extends the usual idea of exponentiation.-Definition:...

  • Ax-Grothendieck theorem
    Ax-Grothendieck theorem
    In mathematics, the Ax–Grothendieck theorem is a result about injectivity and surjectivity of polynomials that was proved independently by James Ax and Alexander Grothendieck....

  • Ax-Kochen theorem
  • Peano axioms
    Peano axioms
    In mathematical logic, the Peano axioms, also known as the Dedekind–Peano axioms or the Peano postulates, are a set of axioms for the natural numbers presented by the 19th century Italian mathematician Giuseppe Peano...

  • Non-standard model of arithmetic
  • First-order arithmetic
  • Second-order arithmetic
    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. It was introduced by David Hilbert and Paul Bernays in their...

  • Presburger arithmetic
    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, omitting the multiplication operation entirely...

  • Wilkie's theorem
    Wilkie's theorem
    In mathematics, Wilkie's theorem is a result by Alex Wilkie about the theory of ordered fields with an exponential function, or equivalently about the geometric nature of exponential varieties.-Formulations:...


  • Functional predicate
    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....

  • T-schema
    T-schema
    The T-schema or truth schema is used to give an inductive definition of truth which lies at the heart of any realisation of Alfred Tarski's semantic theory of truth...

  • Back-and-forth method
  • Barwise compactness theorem
    Barwise compactness theorem
    In mathematical logic, the Barwise compactness theorem, named after Jon Barwise, is a generalization of the usual compactness theorem for first-order logic to a certain class of infinitary languages. It was stated and proved by Barwise in 1967....

  • Skolemization
    Skolem normal form
    Reduction to Skolem normal form is a method for removing existential quantifiers from formal logic statements, often performed as the first step in an automated theorem prover....

  • Lindenbaum–Tarski algebra
    Lindenbaum–Tarski algebra
    In mathematical logic, the Lindenbaum–Tarski algebra of a logical theory T consists of the equivalence classes of sentences of the theory...

  • Löb's theorem
    Löb's theorem
    In mathematical logic, Löb's theorem states that in a theory with Peano arithmetic, for any formula P, if it is provable that "if P is provable then P", then P is provable...

  • Arithmetical set
    Arithmetical set
    In mathematical logic, an arithmetical set is a set of natural numbers that can be defined by a formula of first-order Peano arithmetic...

  • Definable set
    Definable set
    In mathematical logic, a definable set is an n-ary relation on the domain of a structure whose elements are precisely those elements satisfying some formula in the language of that structure...

  • Ehrenfeucht–Fraïssé game
    Ehrenfeucht–Fraïssé game
    In the mathematical discipline of model theory, the Ehrenfeucht–Fraïssé game is a technique for determining whether two structures...

  • Herbrand interpretation
    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 as the function that applies it...

     / Herbrand structure / Herbrand universe
  • Imaginary element
    Imaginary element
    In mathematical model theory, an imaginary element of a structure is roughly a definable equivalence class.These were introduced by , and elimination of imaginaries was introduced by -Definitions:*M is a model of some theory....

  • Indiscernibles
    Indiscernibles
    In mathematical logic, indiscernibles are objects which cannot be distinguished by any property or relation defined by a formula. Usually only first-order formulas are considered...

  • Interpretation (model theory)
    Interpretation (model theory)
    In model theory, interpretation of a structure M in another structure N is a technical notion that approximates the idea of representing M inside N. For example every reduct or definitional expansion of a structure N has an interpretation in N.Many model-theoretic properties are preserved under...

     / Interpretable structure
  • Pregeometry (model theory)
  • Quantifier elimination
    Quantifier elimination
    Quantifier elimination is a concept of simplification used in mathematical logic, model theory, and theoretical computer science. One way of classifying formulas is by the amount of quantification...

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

  • Signature (logic)
    Signature (logic)
    In logic, especially mathematical logic, a signature lists and describes the non-logical symbols of a formal language. In universal algebra, a signature lists the operations that characterize an algebraic structure. In model theory, signatures are used for both purposes.Signatures play the same...

  • Skolem normal form
    Skolem normal form
    Reduction to Skolem normal form is a method for removing existential quantifiers from formal logic statements, often performed as the first step in an automated theorem prover....

  • Type (model theory)
  • Zariski geometry
    Zariski geometry
    In mathematics, a Zariski geometry consists of an abstract structure introduced by Ehud Hrushovski and Boris Zilber, in order to give a characterisation of the Zariski topology on an algebraic curve, and all its powers. The Zariski topology on a product of algebraic varieties is very rarely the...


Set theory

  • Algebra of sets
    Algebra of sets
    The algebra of sets develops and describes the basic properties and laws of sets, the set-theoretic operations of union, intersection, and complementation and the relations of set equality and set inclusion...

     
  • Axiom of choice 
    • Axiom of countable choice
      Axiom of countable choice
      The axiom of countable choice or axiom of denumerable choice, denoted ACω, is an axiom of set theory, similar to the axiom of choice. It states that any countable collection of non-empty sets must have a choice function...

       
    • Axiom of dependent choice
      Axiom of dependent choice
      In mathematics, the axiom of dependent choices, denoted DC, is a weak form of the axiom of choice which is still sufficient to develop most of real analysis...

       
    • Zorn's lemma
      Zorn's lemma
      Zorn's lemma, also known as the Kuratowski–Zorn lemma, is a proposition of set theory that states:Suppose a partially ordered set P has the property that every chain has an upper bound in P...

       
  • Boolean algebra (structure)
  • Boolean-valued model
    Boolean-valued model
    In mathematical logic, a Boolean-valued model is a generalization of the ordinary Tarskian notion of structure from model theory. In a Boolean-valued model, the truth values of propositions are not limited to "true" and "false", but instead take values in some fixed complete Boolean...

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

     
  • Cantor's back-and-forth method
    Cantor's back-and-forth method
    In mathematical logic, especially set theory and model theory, the back-and-forth method is a method for showing isomorphism between countably infinite structures satisfying specified conditions...

     
  • Cantor's diagonal argument
    Cantor's diagonal argument
    Cantor's diagonal argument, also called the diagonalisation argument, the diagonal slash argument or the diagonal method, was published in 1891 by Georg Cantor as a mathematical proof that there are infinite sets which cannot be put into one-to-one correspondence with the infinite set of natural...

     
  • Cantor's first uncountability proof
    Cantor's first uncountability proof
    Georg Cantor's first uncountability proof demonstrates that the set of all real numbers is uncountable. This proof differs from the more familiar proof that uses his diagonal argument...

     
  • Cantor's theorem
    Cantor's theorem
    In elementary set theory, Cantor's theorem states that, for any set A, the set of all subsets of A has a strictly greater cardinality than A itself...

     
  • Cantor–Bernstein–Schroeder theorem
    Cantor–Bernstein–Schroeder theorem
    In set theory, the Cantor–Bernstein–Schroeder theorem, named after Georg Cantor, Felix Bernstein, and Ernst Schröder, states that, if there exist injective functions and between the sets A and B, then there exists a bijective function...

     
  • Cardinality 
    • Aleph number
      Aleph number
      In set theory, a discipline within mathematics, the aleph numbers are a sequence of numbers used to represent the cardinality of infinite sets. They are named after the symbol used to denote them, the Hebrew letter aleph...

       
      • Aleph-null 
      • Aleph-one 
    • Beth number
      Beth number
      In mathematics, the infinite cardinal numbers are represented by the Hebrew letter \aleph indexed with a subscript that runs over the ordinal numbers...

       
    • Cardinal number
      Cardinal number
      In mathematics, cardinal numbers, or cardinals for short, are a generalization of the natural numbers used to measure the cardinality of sets. The cardinality of a finite set is a natural number – the number of elements in the set. The transfinite cardinal numbers describe the sizes of infinite...

       
    • Hartogs number
      Hartogs number
      In mathematics, specifically in axiomatic set theory, a Hartogs number is a particular kind of cardinal number. It was shown by Friedrich Hartogs in 1915, from ZF alone , that there is a least well-ordered cardinal greater than a given well-ordered cardinal.To define the Hartogs number of a set it...

       
  • Cartesian product
    Cartesian product
    In mathematics, a Cartesian product is a construction to build a new set out of a number of given sets. Each member of the Cartesian product corresponds to the selection of one element each in every one of those sets...

     
  • Class (set theory)
    Class (set theory)
    In set theory and its applications throughout mathematics, a class is a collection of sets which can be unambiguously defined by a property that all its members share. The precise definition of "class" depends on foundational context...

     
  • Complement (set theory)
    Complement (set theory)
    In set theory, a complement of a set A refers to things not in , A. The relative complement of A with respect to a set B, is the set of elements in B but not in A...

     
  • Complete Boolean algebra
    Complete Boolean algebra
    In mathematics, a complete Boolean algebra is a Boolean algebra in which every subset has a supremum . Complete Boolean algebras are used to construct Boolean-valued models of set theory in the theory of forcing...

     
  • Continuum (mathematics) 
    • Suslin's problem
      Suslin's problem
      In mathematics, Suslin's problem is a question about totally ordered sets posed by Mikhail Yakovlevich Suslin in a work published posthumously in 1920....

       
  • Continuum hypothesis
    Continuum hypothesis
    In mathematics, the continuum hypothesis is a hypothesis, advanced by Georg Cantor in 1874, about the possible sizes of infinite sets. It states:Establishing the truth or falsehood of the continuum hypothesis is the first of Hilbert's 23 problems presented in the year 1900...

     
  • Countable set
    Countable set
    In mathematics, a countable set is a set with the same cardinality as some subset of the set of natural numbers. A set that is not countable is called uncountable. The term was originated by Georg Cantor...

     
  • Descriptive set theory
    Descriptive set theory
    In mathematical logic, descriptive set theory is the study of certain classes of "well-behaved" subsets of the real line and other Polish spaces...

     
    • Analytic set
      Analytic set
      In 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 definitions of analytic set...

       
    • Analytical hierarchy
      Analytical hierarchy
      In mathematical logic and descriptive set theory, the analytical hierarchy is a higher type analogue of the arithmetical hierarchy. It thus continues the classification of sets by the formulas that define them.-The analytical hierarchy of formulas:...

       
    • Borel equivalence relation
      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....

       
    • Infinity-Borel set
      Infinity-Borel set
      In set theory, a subset of a Polish space X is ∞-Borel if itcan be obtained by starting with the open subsets of X, and transfinitely iterating the operations of complementation and wellordered union...

       
    • Lightface analytic game 
    • Perfect set property
      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...

       
    • Polish space
      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 because they were first extensively studied by Polish...

       
    • Prewellordering
      Prewellordering
      In set theory, a prewellordering is a binary relation that is transitive, wellfounded, and total. In other words, if \leq is a prewellordering on a set X, and if we define \sim byx\sim y\iff x\leq y \land y\leq x...

       
    • Projective set 
    • Property of Baire 
    • Uniformization (set theory)
      Uniformization (set theory)
      In set theory, the axiom of uniformization, a weak form of the axiom of choice, states that if R is a subset of X\times Y, where X and Y are Polish spaces,...

       
    • Universally measurable set
      Universally measurable set
      In mathematics, a subset A of a Polish space X is universally measurable if it is measurable with respect to every complete probability measure on X that measures all Borel subsets of X. In particular, a universally measurable set of reals is necessarily Lebesgue measurable below.Every analytic...

       
  • Determinacy
    Determinacy
    In set theory, a branch of mathematics, determinacy is the study of under what circumstances one or the other player of a game must have a winning strategy, and the consequences of the existence of such strategies.-Games:...

     
    • AD plus
      AD plus
      In set theory, AD+ is an extension, proposed by W. Hugh Woodin, to the axiom of determinacy. The axiom, which is to be understood in the context of ZF plus DCR , states two things:# Every set of reals is ∞-Borel....

       
    • Axiom of determinacy
      Axiom of determinacy
      The axiom of determinacy is a possible axiom for set theory introduced by Jan Mycielski and Hugo Steinhaus in 1962. It refers to certain two-person games of length ω with perfect information...

       
    • Axiom of projective determinacy
      Axiom of projective determinacy
      In mathematical logic, projective determinacy is the special case of the axiom of determinacy applying only to projective sets.The axiom of projective determinacy, abbreviated PD, states that for any two-player game of perfect information of length ω in which the players play natural numbers, if...

       
    • Axiom of real determinacy
      Axiom of real determinacy
      In mathematics, the axiom of real determinacy is an axiom in set theory. It states the following:The axiom of real determinacy is a stronger version of the axiom of determinacy, which makes the same statement about games where both players choose integers; it is inconsistent with the axiom of choice...

       
  • Empty set
    Empty set
    In mathematics, and more specifically set theory, the empty set is the unique set having no elements; its size or cardinality is zero. Some axiomatic set theories assure that the empty set exists by including an axiom of empty set; in other theories, its existence can be deduced...

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

     
  • Fuzzy set
    Fuzzy set
    Fuzzy sets are sets whose elements have degrees of membership. Fuzzy sets were introduced simultaneously by Lotfi A. Zadeh and Dieter Klaua in 1965 as an extension of the classical notion of set. In classical set theory, the membership of elements in a set is assessed in binary terms according to...

     
  • Internal set theory
    Internal set theory
    Internal set theory is a mathematical theory of sets developed by Edward Nelson that provides an axiomatic basis for a portion of the non-standard analysis introduced by Abraham Robinson. Instead of adding new elements to the real numbers, the axioms introduce a new term, "standard", which can be...

     
  • Intersection (set theory)
    Intersection (set theory)
    In mathematics, the intersection of two sets A and B is the set that contains all elements of A that also belong to B , but no other elements....

     
  • L
    Constructible universe
    In mathematics, the constructible universe , denoted L, is a particular class of sets which can be described entirely in terms of simpler sets. It was introduced by Kurt Gödel in his 1938 paper "The Consistency of the Axiom of Choice and of the Generalized Continuum-Hypothesis"...

     
  • L(R)
    L(R)
    In set theory, L is the smallest transitive inner model of ZF containing all the ordinals and all the reals. It can be constructed in a manner analogous to the construction of L , by adding in all the reals at the start, and then iterating the definable powerset operation through all the...

     
  • Large cardinal property
    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"...

     
  • Musical set theory 
  • Ordinal number
    Ordinal number
    In set theory, an ordinal number, or just ordinal, is the order type of a well-ordered set. They are usually identified with hereditarily transitive sets. Ordinals are an extension of the natural numbers different from integers and from cardinals...

     
    • Infinite descending chain
      Infinite descending chain
      Given a set S with a partial order ≤, an infinite descending chain is a chain V that is a subset of S upon which ≤ defines a total order such that V has no least element, that is, an element m such that for all elements n in V it holds that m ≤ n.As an example, in the set of integers, the chain...

       
    • Limit ordinal 
    • Successor ordinal
      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...

       
    • Transfinite induction
      Transfinite induction
      Transfinite induction is an extension of mathematical induction to well-ordered sets, for instance to sets of ordinal numbers or cardinal numbers.- Transfinite induction :Let P be a property defined for all ordinals α...

       
      • ∈-induction 
    • Well-founded set 
    • Well-order
      Well-order
      In mathematics, a well-order relation on a set S is a strict total order on S with the property that every non-empty subset of S has a least element in this ordering. Equivalently, a well-ordering is a well-founded strict total order...

       
  • Power set 
  • Russell's paradox
    Russell's paradox
    In the foundations of mathematics, Russell's paradox , discovered by Bertrand Russell in 1901, showed that the naive set theory created by Georg Cantor leads to a contradiction...

     
  • Set theory
    Set theory
    Set theory is the branch of mathematics that studies sets, which are collections of objects. Although any type of object can be collected into a set, set theory is applied most often to objects that are relevant to mathematics...

     
    • Alternative set theory
      Alternative set theory
      Generically, an alternative set theory is an alternative mathematical approach to the concept of set. It is a proposed alternative to the standard set theory.Some of the alternative set theories are:*the theory of semisets...

       
    • Axiomatic set theory 
    • Kripke-Platek set theory with urelements 
    • Morse-Kelley set theory 
    • Naive set theory
      Naive set theory
      Naive set theory is one of several theories of sets used in the discussion of the foundations of mathematics. The informal content of this naive set theory supports both the aspects of mathematical sets familiar in discrete mathematics , and the everyday usage of set theory concepts in most...

       
    • New Foundations
      New Foundations
      In mathematical logic, New Foundations is an axiomatic set theory, conceived by Willard Van Orman Quine as a simplification of the theory of types of Principia Mathematica. Quine first proposed NF in a 1937 article titled "New Foundations for Mathematical Logic"; hence the name...

       
    • Positive set theory 
    • Zermelo-Fraenkel set theory 
    • Zermelo set theory
      Zermelo set theory
      Zermelo set theory, as set out in an important paper in 1908 by Ernst Zermelo, is the ancestor of modern set theory. It bears certain differences from its descendants, which are not always understood, and are frequently misquoted...

       
  • Set (mathematics) 
  • Simple theorems in the algebra of sets
    Simple theorems in the algebra of sets
    The simple theorems in the algebra of sets are some of the elementary properties of the algebra of union , intersection , and set complement of sets....

     
  • Subset
    Subset
    In mathematics, especially in set theory, a set A is a subset of a set B if A is "contained" inside B. A and B may coincide. The relationship of one set being a subset of another is called inclusion or sometimes containment...

     
  • Θ (set theory) 
  • Tree (descriptive set theory) 
  • Tree (set theory)
    Tree (set theory)
    In set theory, a tree is a partially ordered set In set theory, a tree is a partially ordered set (poset) In set theory, a tree is a partially ordered set (poset) (T, In set theory, a tree is a partially ordered set (poset) (T, ...

     
  • Union (set theory)
    Union (set theory)
    In set theory, the union of a collection of sets is the set of all distinct elements in the collection. The union of a collection of sets S_1, S_2, S_3, \dots , S_n\,\! gives a set S_1 \cup S_2 \cup S_3 \cup \dots \cup S_n.- Definition :...

     
  • Von Neumann universe
    Von Neumann universe
    In set theory and related branches of mathematics, the von Neumann universe, or von Neumann hierarchy of sets, denoted V, is the class of hereditary well-founded sets...

     
  • Zero sharp
    Zero sharp
    In the mathematical discipline of set theory, 0# is the set of true formulas about indiscernibles in the Gödel constructible universe. It is often encoded as a subset of the integers , or as a subset of the hereditarily finite sets, or as a real number...

     

Large cardinals

  • Almost Ramsey cardinal
  • Erdős cardinal
    Erdos 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...

  • Extendible cardinal
    Extendible cardinal
    In mathematics, extendible cardinals are large cardinals introduced by , who was partly motivated by reflection principles. A cardinal number κ is called η-extendible if for some λ there is a nontrivial elementary embedding j ofinto...

  • Huge cardinal
  • Hyper-Woodin cardinal
  • Inaccessible cardinal
    Inaccessible cardinal
    In set theory, an uncountable regular cardinal number is called weakly inaccessible if it is a weak limit cardinal, and strongly inaccessible, or just inaccessible, if it is a strong limit cardinal. Some authors do not require weakly and strongly inaccessible cardinals to be uncountable...

  • Ineffable cardinal
  • Mahlo cardinal
    Mahlo cardinal
    In mathematics, a Mahlo cardinal is a certain kind of large cardinal number. Mahlo cardinals were first described by . As with all large cardinals, none of these varieties of Mahlo cardinals can be proved to exist by ZFC ....

  • Measurable cardinal
    Measurable cardinal
    - Measurable :Formally, a measurable cardinal is an uncountable cardinal number κ such that there exists a κ-additive, non-trivial, 0-1-valued measure on the power set of κ...

  • N-huge cardinal
  • Ramsey cardinal
    Ramsey cardinal
    In mathematics, a Ramsey cardinal is a certain kind of large cardinal number introduced by and named after Frank P. Ramsey.With [κ]<ω denoting the set of all finite subsets of κ, a cardinal number κ such that for every function...

  • Rank-into-rank
    Rank-into-rank
    In set theory, a branch of mathematics, a rank-into-rank is a large cardinal λ satisfying one of the following four axioms :...

  • Remarkable cardinal
  • Shelah cardinal
  • Strong 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 :...

  • Strongly inaccessible cardinal
  • Subtle cardinal
    Subtle cardinal
    In mathematics, subtle cardinals and ethereal cardinals are closely related kinds of large cardinal number.A cardinal κ is called subtle if for every closed and unbounded C ⊂ κ and for every sequence A of length κ for which element number δ , Aδ ⊂ δ there...

  • Supercompact cardinal
  • Superstrong cardinal
  • Totally indescribable cardinal
    Totally indescribable cardinal
    In mathematics, a Q-indescribable cardinal is a certain kind of large cardinal number that is hard to describe in some language Q. There are many different types of indescribable cardinals corresponding to different choices of languages Q...

  • Weakly compact 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 can not be proven from the standard axioms of set theory....

  • Weakly hyper-Woodin cardinal
  • Weakly inaccessible cardinal
  • Woodin cardinal
    Woodin cardinal
    In set theory, a Woodin cardinal is a cardinal number λ such that for all functionsthere exists a cardinal κ In set theory, a Woodin cardinal is a cardinal number λ such that for all functions...

  • Unfoldable 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 transitive model M of cardinality κ of ZFC-minus-power set such that κ is in M and M contains all its sequences of length less than κ, there is a...


Recursion theory

  • Entscheidungsproblem
    Entscheidungsproblem
    In mathematics, the is a challenge posed by David Hilbert in 1928. The asks for an algorithm that will take as input a description of a formal language and a mathematical statement in the language and produce as output either "True" or "False" according to whether the statement is true or false...

  • Decision problem
    Decision problem
    In computability theory and computational complexity theory, a decision problem is a question in some formal system with a yes-or-no answer, depending on the values of some input parameters. For example, the problem "given two numbers x and y, does x evenly divide y?" is a decision problem...

  • Decidability (logic)
    Decidability (logic)
    In logic, the term decidable refers to the decision problem, the question of the existence of an effective method for determining membership in a set of formulas. Logical systems such as propositional logic are decidable if membership in their set of logically valid formulas can be effectively...

  • Church-Turing thesis
  • Computable function
    Computable function
    Computable functions are the basic objects of study in computability theory. Computable functions are the formalized analogue of the intuitive notion of algorithm. They are used to discuss computability without referring to any concrete model of computation such as Turing machines or register...

    • Algorithm
      Algorithm
      In mathematics and computer science, an algorithm is an effective method expressed as a finite list of well-defined instructions for calculating a function. Algorithms are used for calculation, data processing, and automated reasoning...

    • Recursion
      Recursion
      Recursion is the process of repeating items in a self-similar way. For instance, when the surfaces of two mirrors are exactly parallel with each other the nested images that occur are a form of infinite recursion. The term has a variety of meanings specific to a variety of disciplines ranging from...

    • Primitive recursive function
      Primitive recursive function
      The primitive recursive functions are defined using primitive recursion and composition as central operations and are a strict subset of the total µ-recursive functions...

    • Mu operator
      Mu operator
      In computability theory, the μ operator, minimization operator, or unbounded search operator searches for the least natural number with a given property.- Definition :...

    • Ackermann function
      Ackermann function
      In computability theory, the Ackermann function, named after Wilhelm Ackermann, is one of the simplest and earliest-discovered examples of a total computable function that is not primitive recursive...

    • Turing machine
      Turing machine
      A Turing machine is a theoretical device that manipulates symbols on a strip of tape according to a table of rules. Despite its simplicity, a Turing machine can be adapted to simulate the logic of any computer algorithm, and is particularly useful in explaining the functions of a CPU inside a...

    • Halting problem
      Halting problem
      In computability theory, the halting problem can be stated as follows: Given a description of a computer program, decide whether the program finishes running or continues to run forever...

    • Computability theory
      Computability theory
      Computability theory, also called recursion theory, is a branch of mathematical logic that originated in the 1930s with the study of computable functions and Turing degrees. The field has grown to include the study of generalized computability and definability...

      , computation
      Computation
      Computation is defined as any type of calculation. Also defined as use of computer technology in Information processing.Computation is a process following a well-defined model understood and expressed in an algorithm, protocol, network topology, etc...

    • Herbrand Universe
    • Markov algorithm
      Markov algorithm
      In theoretical computer science, a Markov algorithm is a string rewriting system that uses grammar-like rules to operate on strings of symbols. Markov algorithms have been shown to be Turing-complete, which means that they are suitable as a general model of computation and can represent any...

    • Lambda calculus
      Lambda calculus
      In mathematical logic and computer science, lambda calculus, also written as λ-calculus, is a formal system for function definition, function application and recursion. The portion of lambda calculus relevant to computation is now called the untyped lambda calculus...

      • Church-Rosser theorem
      • Calculus of constructions
        Calculus of constructions
        The calculus of constructions is a formal language in which both computer programs and mathematical proofs can be expressed. This language forms the basis of theory behind the Coq proof assistant, which implements the derivative calculus of inductive constructions.-General traits:The CoC is a...

    • Combinatory logic
      Combinatory logic
      Combinatory logic is a notation introduced by Moses Schönfinkel and Haskell Curry to eliminate the need for variables in mathematical logic. It has more recently been used in computer science as a theoretical model of computation and also as a basis for the design of functional programming...

    • Post correspondence problem
      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....

  • Kleene's recursion theorem
    Kleene's recursion theorem
    In computability theory, Kleene's recursion theorems are a pair of fundamental results about the application of computable functions to their own descriptions...

  • Recursively enumerable set
    Recursively enumerable set
    In computability theory, traditionally called recursion theory, a set S of natural numbers is called recursively enumerable, computably enumerable, semidecidable, provable or Turing-recognizable if:...

    • Recursively enumerable language
      Recursively enumerable language
      In mathematics, logic and computer science, a recursively enumerable language is a type of formal language which is also called partially decidable or Turing-acceptable. It is known as a type-0 language in the Chomsky hierarchy of formal languages...

  • Decidable language
  • Undecidable language
  • Rice's theorem
    Rice's theorem
    In computability theory, Rice's theorem states that, for any non-trivial property of partial functions, there is no general and effective method to decide whether an algorithm computes a partial function with that property...

  • Post's theorem
    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 recursion theory...

  • Turing degree
    Turing degree
    In computer science and mathematical logic the Turing degree or degree of unsolvability of a set of natural numbers measures the level of algorithmic unsolvability of the set...

  • Effective results in number theory
    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...

  • Diophantine set
    Diophantine set
    In mathematics, a Diophantine equation is an equation of the form P=0 where P is a polynomial with integer coefficients...

  • Matiyasevich's theorem
  • Word problem for groups
    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 element...

  • Arithmetical hierarchy
    Arithmetical hierarchy
    In mathematical logic, the arithmetical hierarchy, arithmetic hierarchy or Kleene-Mostowski hierarchy classifies certain sets based on the complexity of formulas that define them...

  • Subrecursion theory
    • Presburger arithmetic
      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, omitting the multiplication operation entirely...

    • Computational complexity theory
      Computational complexity theory
      Computational complexity theory is a branch of the theory of computation in theoretical computer science and mathematics that focuses on classifying computational problems according to their inherent difficulty, and relating those classes to each other...

    • Polynomial time
    • Exponential time
    • Complexity class
      Complexity class
      In computational complexity theory, a complexity class is a set of problems of related resource-based complexity. A typical complexity class has a definition of the form:...

      • Complexity classes P and NP
      • Cook's theorem
        Cook's theorem
        In computational complexity theory, the Cook–Levin theorem, also known as Cook's theorem, states that the Boolean satisfiability problem is NP-complete...

      • List of complexity classes
      • Polynomial hierarchy
        Polynomial hierarchy
        In computational complexity theory, the polynomial hierarchy is a hierarchy of complexity classes that generalize the classes P, NP and co-NP to oracle machines...

      • Exponential hierarchy
    • NP-complete
      NP-complete
      In computational complexity theory, the complexity class NP-complete is a class of decision problems. A decision problem L is NP-complete if it is in the set of NP problems so that any given solution to the decision problem can be verified in polynomial time, and also in the set of NP-hard...

    • Time hierarchy theorem
      Time hierarchy theorem
      In computational complexity theory, the time hierarchy theorems are important statements about time-bounded computation on Turing machines. Informally, these theorems say that given more time, a Turing machine can solve more problems...

    • Space 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 more space, subject to certain conditions. For example, a deterministic Turing machine can solve more decision problems...

  • Natural proof
    Natural proof
    In computational complexity theory, a natural proof is a certain kind of proof establishing that one complexity class differs from another one. While these proofs are in some sense "natural", it can be shown that no such proof can possibly be used to solve the P vs...

  • Hypercomputation
    Hypercomputation
    Hypercomputation or super-Turing computation refers to models of computation that are more powerful than, or are incomparable with, Turing computability. This includes various hypothetical methods for the computation of non-Turing-computable functions, following super-recursive algorithms...

    • Oracle machine
      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 decide certain decision problems in a single operation. The problem can be of any...

  • Alonzo Church
    Alonzo Church
    Alonzo Church was an American mathematician and logician who made major contributions to mathematical logic and the foundations of theoretical computer science. He is best known for the lambda calculus, Church–Turing thesis, Frege–Church ontology, and the Church–Rosser theorem.-Life:Alonzo Church...

  • Emil Post
  • Alan Turing
    Alan Turing
    Alan Mathison Turing, OBE, FRS , was an English mathematician, logician, cryptanalyst, and computer scientist. He was highly influential in the development of computer science, providing a formalisation of the concepts of "algorithm" and "computation" with the Turing machine, which played a...

  • Jacques Herbrand
    Jacques Herbrand
    Jacques Herbrand was a French mathematician who was born in Paris, France and died in La Bérarde, Isère, France. Although he died at only 23 years of age, he was already considered one of "the greatest mathematicians of the younger generation" by his professors Helmut Hasse, and Richard Courant.He...

  • Haskell Curry
    Haskell Curry
    Haskell Brooks Curry 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 Moses Schönfinkel, much of the development was done by Curry. Curry is also known for Curry's...

  • Stephen Cole Kleene
    Stephen Cole Kleene
    Stephen Cole Kleene was an American mathematician who helped lay the foundations for theoretical computer science...

  • Definable real number

Proof theory

  • Metamathematics
    Metamathematics
    Metamathematics is the study of mathematics itself using mathematical methods. This study produces metatheories, which are mathematical theories about other mathematical theories...

  • Cut-elimination
  • Tarski's indefinability theorem
    Tarski's indefinability theorem
    Tarski's undefinability theorem, stated and proved by Alfred Tarski in 1936, is an important limitative result in mathematical logic, the foundations of mathematics, and in formal semantics...

  • Diagonal lemma
    Diagonal lemma
    In mathematical logic, the diagonal lemma or fixed point theorem establishes the existence of self-referential sentences in certain formal theories of the natural numbers -- specifically those theories that are strong enough to represent all computable functions...

  • Provability logic
    Provability logic
    Provability logic is a modal logic, in which the box 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....

  • Interpretability logic
    Interpretability logic
    Interpretability logics comprise a family of modal logics that extend provability logic to describe interpretability and/or various related metamathematical properties and relations such as weak interpretability, Π1-conservativity, cointerpretability, tolerance, cotolerance and arithmetic...

  • Sequent
    Sequent
    In proof theory, a sequent is a formalized statement of provability that is frequently used when specifying calculi for deduction. In the sequent calculus, the name sequent is used for the construct which can be regarded as a specific kind of judgment, characteristic to this deduction system.-...

  • Sequent calculus
    Sequent calculus
    In proof theory and mathematical logic, sequent calculus is a family of formal systems sharing a certain style of inference and certain formal properties. The first sequent calculi, systems LK and LJ, were introduced by Gerhard Gentzen in 1934 as a tool for studying natural deduction in...

  • Analytic proof
    Analytic proof
    In mathematical analysis, an analytical proof is a proof of a theorem in analysis that only makes use of methods from analysis, and which does not make use of results from geometry...

  • Structural proof theory
    Structural proof theory
    In mathematical logic, structural proof theory is the subdiscipline of proof theory that studies proof calculi that support a notion of analytic proof.-Analytic proof:...

  • Self-verifying theories
    Self-verifying theories
    Self-verifying theories are consistent first-order systems of arithmetic much weaker than Peano arithmetic that are capable of proving their own consistency. Dan Willard was the first to investigate their properties, and he has described a family of such systems...

  • Substructural logic
    Substructural logic
    In logic, a substructural logic is a logic lacking one of the usual structural rules , such as weakening, contraction or associativity...

    s
    • Structural rule
      Structural rule
      In proof theory, a structural rule is an inference rule that does not refer to any logical connective, but instead operates on the judgements or sequents directly. Structural rules often mimic intended meta-theoretic properties of the logic...

      • Weakening
      • Contraction
    • Linear logic
      Linear logic
      Linear logic is a substructural logic proposed by Jean-Yves Girard as a refinement of classical and intuitionistic logic, joining the dualities of the former with many of the constructive properties of the latter...

      • Intuitionistic linear logic
      • Proof net
        Proof net
        In proof theory, proof nets are a geometrical method of representing proofs thateliminates two forms of bureaucracy that differentiates proofs: irrelevant syntactical features of regular proof calculi such as the natural deduction calculus and the sequent calculus, and the order of rules applied...

    • Affine logic
      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....

    • Strict logic
      Strict logic
      Strict logic is essentially synonymous with relevant logic, though it can be characterized proof-theoretically as* ordinary logic without weakening, or* linear logic with contraction....

    • Relevant logic
  • Proof-theoretic semantics
    Proof-theoretic semantics
    Proof-theoretic semantics is an approach to the semantics of logic that attempts to locate the meaning of propositions and logical connectives not in terms of interpretations, as in Tarskian approaches to semantics, but in the role that the proposition or logical connective plays within the system...

  • Ludics
    Ludics
    In proof theory, ludics is an analysis of the principles governing inference rules of mathematical logic. Key features of ludics are its notion of compound connectives using a technique known as focusing or focalisation , and its use of locations or loci over a base instead of propositions.More...

  • System F
    System F
    System F, also known as the polymorphic lambda calculus or the second-order lambda calculus, is a typed lambda calculus that differs from the simply typed lambda calculus by the introduction of a mechanism of universal quantification over types...

  • Gerhard Gentzen
    Gerhard Gentzen
    Gerhard Karl Erich Gentzen was a German mathematician and logician. He had his major contributions in the foundations of mathematics, proof theory, especially on natural deduction and sequent calculus...

  • Gentzen's consistency proof
    Gentzen's consistency proof
    Gentzen's consistency proof is a result of proof theory in mathematical logic. It "reduces" the consistency of a simplified part of mathematics, not to something that could be proved , but to clarified logical principles.-Gentzen's theorem:In 1936 Gerhard Gentzen proved the consistency of...

  • Reverse mathematics
    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 contrast to the ordinary mathematical practice of...

  • Nonfirstorderizability
    Nonfirstorderizability
    In formal logic, nonfirstorderizability is the inability of an expression to be adequately captured in particular theories in first-order logic. Nonfirstorderizable sentences are sometimes presented as evidence that first-order logic is not adequate to capture the nuances of meaning in natural...

  • Interpretability
    Interpretability
    In mathematical logic, interpretability is a relation between formal theories that expresses the possibility of interpreting or translating one into the other.-Informal definition:Assume T and S are formal theories...

  • Weak interpretability
    Weak interpretability
    Weak interpretability is a special case of the concept of tolerance introduced by Giorgi Japaridze in 1992.Assume T and S are formal theories. Slightly simplified, T is said to be weakly interpretable in S if, and only if, the language of T can be translated into the language of S in such a way...

  • Cointerpretability
    Cointerpretability
    In mathematical logic, cointerpretability is a binary relation on formal theories: a formal theory T is cointerpretable in another such theory S, when the language of S can be translated into the language of T in such a way that S proves every formula whose translation is a theorem of T...

  • Tolerant sequence
  • Cotolerant sequence
  • Deduction theorem
    Deduction theorem
    In mathematical logic, the deduction theorem is a metatheorem of first-order logic. It is a formalization of the common proof technique in which an implication A → B is proved by assuming A and then proving B from this assumption. The deduction theorem explains why proofs of conditional...


Mathematical constructivism

  • Nonconstructive proof
  • Existence theorem
    Existence theorem
    In mathematics, an existence theorem is a theorem with a statement beginning 'there exist ..', or more generally 'for all x, y, ... there exist ...'. That is, in more formal terms of symbolic logic, it is a theorem with a statement involving the existential quantifier. Many such theorems will not...

  • Intuitionistic logic
    Intuitionistic logic
    Intuitionistic logic, or constructive logic, is a symbolic logic system differing from classical logic in its definition of the meaning of a statement being true. In classical logic, all well-formed statements are assumed to be either true or false, even if we do not have a proof of either...

  • Intuitionistic type theory
    Intuitionistic type theory
    Intuitionistic type theory, or constructive type theory, or Martin-Löf type theory or just Type Theory is a logical system and a set theory based on the principles of mathematical constructivism. Intuitionistic type theory was introduced by Per Martin-Löf, a Swedish mathematician and philosopher,...

  • Type theory
    Type theory
    In mathematics, logic and computer science, type theory is any of several formal systems that can serve as alternatives to naive set theory, or the study of such formalisms in general...

  • Lambda calculus
    Lambda calculus
    In mathematical logic and computer science, lambda calculus, also written as λ-calculus, is a formal system for function definition, function application and recursion. The portion of lambda calculus relevant to computation is now called the untyped lambda calculus...

    • Church–Rosser theorem
      Church–Rosser theorem
      The Church–Rosser theorem states that if there are two distinct reductions starting from the same lambda calculus term, then there exists a term that is reachable from each reduct via a sequence of reductions...

  • Simply typed lambda calculus
    Simply typed lambda calculus
    The simply typed lambda calculus , a formof 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 calculus...

  • Typed lambda calculus
    Typed lambda calculus
    A typed lambda calculus is a typed formalism that uses the lambda-symbol 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 type depends on the calculus considered...

  • Curry–Howard isomorphism
  • Calculus of constructions
    Calculus of constructions
    The calculus of constructions is a formal language in which both computer programs and mathematical proofs can be expressed. This language forms the basis of theory behind the Coq proof assistant, which implements the derivative calculus of inductive constructions.-General traits:The CoC is a...

  • Constructivist analysis
    Constructivist analysis
    In mathematics, constructive analysis is mathematical analysis done according to the principles of constructive mathematics.This contrasts with classical analysis, which simply means analysis done according to the principles of classical mathematics.Generally speaking, constructive analysis can...

  • Lambda cube
    Lambda cube
    In mathematical logic and type theory, the λ-cube is a framework for exploring the axes of refinement in Coquand's calculus of constructions, starting from the simply typed lambda calculus as the vertex of a cube placed at the origin, and the calculus of constructions as its diametrically opposite...

  • System F
    System F
    System F, also known as the polymorphic lambda calculus or the second-order lambda calculus, is a typed lambda calculus that differs from the simply typed lambda calculus by the introduction of a mechanism of universal quantification over types...

  • Introduction to topos theory
  • LF (logical framework)
    LF (logical framework)
    In logic, a logical framework provides a means to define 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 type theory. This approach has been used successfully for ...

  • Computability logic
    Computability logic
    Introduced by Giorgi Japaridze in 2003, computability logic is a research programme and mathematical framework for redeveloping logic as a systematic formal theory of computability, as opposed to classical logic which is a formal theory of truth...

  • Computable measure theory
    Computable measure theory
    In mathematics, computable measure theory is a version of measure theory which deals with computable numbers, as opposed to real numbers which are used in standard measure theory....

  • Finitism
    Finitism
    In the philosophy of mathematics, one of the varieties of finitism is an extreme form of constructivism, according to which a mathematical object does not exist unless it can be constructed from natural numbers in a finite number of steps...

  • Ultraintuitionism
  • Luitzen Egbertus Jan Brouwer
    Luitzen Egbertus Jan Brouwer
    Luitzen Egbertus Jan Brouwer FRS , usually cited as L. E. J. Brouwer but known to his friends as Bertus, was a Dutch mathematician and philosopher, a graduate of the University of Amsterdam, who worked in topology, set theory, measure theory and complex analysis.-Biography:Early in his career,...


Theorem provers

  • First-order resolution
  • Automated theorem proving
    Automated theorem proving
    Automated theorem proving or automated deduction, currently the most well-developed subfield of automated reasoning , is the proving of mathematical theorems by a computer program.- Decidability of the problem :...

  • ACL2 theorem prover
    ACL2 theorem prover
    ACL2 is a software system consisting of a programming language, an extensible theory in a first-order logic, and a mechanical theorem prover. ACL2 is designed to support automated reasoning in inductive logical theories, mostly for the purpose of software and hardware verification...

  • E equational theorem prover
    E equational theorem prover
    E is a modern, high performance theorem prover for full first-order logic with equality. It is based on the equational superposition calculus and uses a purely equational paradigm. It has been integrated into other theorem provers and it has been among the best-placed systems in several theorem...

  • Gandalf theorem prover
    Gandalf theorem prover
    Gandalf is a first-order automated theorem prover applied to several domain-specifictasks such as Semantic web. It has also participated in The CADE ATP System Competition and had impressive results in that competition. It is programmed in the Scheme programming language which is then compiled to...

  • HOL theorem prover
    HOL theorem prover
    HOL denotes a family of interactive theorem proving systems sharingsimilar logics and implementation strategies....

  • Isabelle theorem prover
    Isabelle theorem prover
    The Isabelle theorem prover is an interactive theorem prover, successor of the Higher Order Logic theorem prover. It is an LCF-style theorem prover , so it is based on a small logical core guaranteeing logical correctness...

  • LCF theorem prover
    LCF theorem prover
    Logic for Computable Functions is an interactive automated theorem prover developed at the universities of Edinburgh and Stanford by Robin Milner and others in 1972. LCF introduced the general-purpose programming language ML to allow users to write theorem-proving tactics. Theorems in the system...

  • Otter theorem prover
    Otter theorem prover
    Otter is an automated theorem prover developed by William McCune at Argonne National Laboratory in Illinois. Otter was the first widely distributed, high-performance theorem prover for first-order logic, and it pioneered a number of important implementation techniques...

  • Paradox theorem prover
    Paradox theorem prover
    Paradox is an automated theorem proving system developed by Koen Lindström Claessen and Niklas Sörensson at the Chalmers University of Technology. The software is written in the Haskell programming language and is released under the terms of the GNU General Public License....

  • Vampire theorem prover
    Vampire theorem prover
    Vampire is an automatic theorem prover for first-order classical logic developed in the Computer Science Department of the University of Manchester byProf. Andrei Voronkov together with Kryštof Hoder and previously with Dr. Alexandre Riazanov...

  • Interactive proof system
    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. The parties, the verifier and the prover, interact by exchanging messages in order to ascertain whether a given string belongs to a...

  • Mizar system
    Mizar system
    The Mizar system consists of a language for writing strictly formalized mathematical definitions and proofs, a computer program which is able to check proofs written in this language, and a library of definitions and proved theorems which can be referenced and used in new articles. Mizar has goals...

  • QED project
    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. The idea for the project arose in 1993, mainly under the impetus of Robert Boyer...

  • Coq
    Coq
    In computer science, Coq is an interactive theorem prover. It allows the expression of mathematical assertions, mechanically checks proofs of these assertions, helps to find formal proofs, and extracts a certified program from the constructive proof of its formal specification...


Historical

  • Begriffsschrift
    Begriffsschrift
    Begriffsschrift is a book on logic by Gottlob Frege, published in 1879, and the formal system set out in that book...

  • Systems of Logic Based on Ordinals
    Systems of Logic Based on Ordinals
    Systems of Logic Based on Ordinals was the PhD dissertation of the mathematician Alan Turing.The thesis was completed at Princeton under Alonzo Church and was a classic work in mathematics which introduced the concept of ordinal logic....

    Alan Turing's
    Alan Turing
    Alan Mathison Turing, OBE, FRS , was an English mathematician, logician, cryptanalyst, and computer scientist. He was highly influential in the development of computer science, providing a formalisation of the concepts of "algorithm" and "computation" with the Turing machine, which played a...

    Ph.D. thesis
The source of this article is wikipedia, the free encyclopedia.  The text of this article is licensed under the GFDL.
 
x
OK