Model theory
Encyclopedia
In mathematics
, model theory is the study of (classes of) mathematical structures
(e.g. groups
, fields
, graphs
, universes of set theory
) using tools from mathematical logic
.
Objects of study in model theory are models for formal language
s which are structures that give meaning to the sentences of these formal languages. If a model for a language moreover satisfies a particular sentence or theory (set of sentences satisfying special conditions), it is called a model of the sentence or theory.
Model theory has close ties to algebra
and universal algebra
.
This article focuses on finitary first order
model theory of infinite structures. Finite model theory
, which concentrates on finite structures, diverges significantly from the study of infinite structures in both the problems studied and the techniques used. Model theory in higher-order logic
s or infinitary logic
s is hampered by the fact that completeness
does not in general hold for these logics. However, a great deal of study has also been done in such languages.
elements by means of syntactical
elements of a corresponding language. To quote the first page of Chang
and Keisler
(1990):
Model theory developed rapidly during the 1990s, and a more modern definition is provided by Wilfrid Hodges
(1997):
In a similar way to proof theory
, model theory is situated in an area of interdisciplinarity
between mathematics
, philosophy
, and computer science
. The most important professional organization in the field of model theory is the Association for Symbolic Logic
.
An incomplete and somewhat arbitrary subdivision of model theory is into classical model theory, model theory applied to groups and fields, and geometric model theory. A missing subdivision is computable model theory
, but this can arguably be viewed as an independent subfield of logic. Examples of early theorems from classical model theory include Gödel's completeness theorem
, the upward and downward Löwenheim–Skolem theorem
s, Vaught
's two-cardinal theorem, Scott
's isomorphism theorem, the omitting types theorem, and the Ryll-Nardzewski theorem. Examples of early results from model theory applied to fields are Tarski's elimination of quantifiers
for real closed fields, Ax
's theorem on pseudo-finite fields, and Robinson
's development of nonstandard analysis. An important step in the evolution of classical model theory occurred with the birth of stability theory
(through Morley's theorem
on uncountably categorical theories and Shelah
's classification program), which developed a calculus of independence and rank based on syntactical conditions satisfied by theories. During the last several decades applied model theory has repeatedly merged with the more pure stability theory. The result of this synthesis is called geometric model theory in this article (which is taken to include o-minimality, for example, as well as classical geometric stability theory). An example of a theorem from geometric model theory is Hrushovski
's proof of the Mordell–Lang conjecture for function fields. The ambition of geometric model theory is to provide a geography of mathematics by embarking on a detailed study of definable sets in various mathematical structures, aided by the substantial tools developed in the study of pure model theory.
σ and σ-algebras. Since these concepts are formally defined in the article on structure
s, the present article can content itself with an informal introduction which consists in examples of how these terms are used.
This is a very efficient way to define most classes of algebraic structure
s, because there is also the concept of σ-homomorphism, which correctly specializes to the usual notions of homomorphism for groups, semigroups, magmas and rings. For this to work, the signature must be chosen well.
Terms such as the σring-term t(u,v,w) given by are used to define identities but also to construct free algebra
s. An equational class
is a class of structures which, like the examples above and many others, is defined as the class of all σ-structures which satisfy a certain set of identities. Birkhoff's theorem states:
An important non-trivial tool in universal algebra are ultraproduct
s
, where I is an infinite set indexing a system of σ-structures Ai, and U is an ultrafilter
on I.
While model theory is generally considered a part of mathematical logic
, universal algebra, which grew out of Alfred North Whitehead
's (1898) work on abstract algebra
, is part of algebra
. This is reflected by their respective MSC
classifications. Nevertheless model theory can be seen as an extension of universal algebra.
s for signatures σ which may contain relation symbols as in the following example:
A σ-homomorphism is a map that commutes with the operations and preserves the relations in σ. This definition gives rise to the usual notion of graph homomorphism
, which has the interesting property that a bijective homomorphism need not be invertible. Structures are also a part of universal algebra; after all, some algebraic structure
s such as ordered groups have a binary relation <. What distinguishes finite model theory from universal algebra is its use of more general logical sentences (as in the example above) in place of identities. (In a model-theoretic context an identity t=t' is written as a sentence 
.)
The logics employed in finite model theory are often substantially more expressive than first-order logic, the standard logic for model theory of infinite structures.
for a signature
, logic
provides the syntax
. With terms, identities and quasi-identities
, even universal algebra has some limited syntactic tools; first-order logic is the result of making quantification explicit and adding negation into the picture.
A first-order formula is built out of atomic formula
s such as R(f(x,y),z) or y = x + 1 by means of the Boolean connectives
and prefixing of quantifiers 
or 
. A sentence is a formula in which each occurrence of a variable is in the scope of a corresponding quantifier. Examples for formulas are φ (or φ(x) to mark the fact that at most x is an unbound variable in φ) and ψ defined as follows:
(Note that the equality symbol has a double meaning here.) It is intuitively clear how to translate such formulas into mathematical meaning. In the σsmr-structure
of the natural numbers, for example, an element n satisfies the formula φ if and only if n is a prime number. The formula ψ similarly defines irreducibility. Tarski gave a rigorous definition, sometimes called "Tarski's definition of truth"
, for the satisfaction relation
, so that one easily proves:
is a prime number.
is irreducible.
A set T of sentences is called a (first-order) theory
. A theory is satisfiable if it has a model
, i.e. a structure (of the appropriate signature) which satisfies all the sentences in the set T. Consistency
of a theory is usually defined in a syntactical way, but in first-order logic by the completeness theorem
there is no need to distinguish between satisfiability and consistency. Therefore model theorists often use "consistent" as a synonym for "satisfiable".
A theory is called categorical if it determines a structure up to isomorphism, but it turns out that this definition is not useful, due to serious restrictions in the expressivity of first-order logic. The Löwenheim–Skolem theorem
implies that for every theory T which has an infinite model and for every infinite cardinal number
κ, there is a model
such that the number of elements of 
is exactly κ. Therefore only finite structures can be described by a categorical theory.
Lack of expressivity (when compared to higher logics such as second-order logic
) has its advantages, though. For model theorists the Löwenheim–Skolem theorem is an important practical tool rather than the source of Skolem's paradox
. First-order logic is in some sense (for which see Lindström's theorem
) the most expressive logic for which both the Löwenheim–Skolem theorem and the compactness theorem hold:
This important theorem, due to Gödel
, is of central importance in infinite model theory, where the words "by compactness" are commonplace. One way to prove it is by means of ultraproduct
s. An alternative proof uses the completeness theorem, which is otherwise reduced to a marginal role in most of modern model theory.
, i.e. axiomatizable in first-order logic (i.e. there is a theory T such that a σ-structure is in the class if and only if it satisfies T). E.g. this step fails for the trees, since connectedness cannot be expressed in first-order logic. Axiomatizability ensures that model theory can speak about the right objects. Quantifier elimination can be seen as a condition which ensures that model theory does not say too much about the objects.
A theory T has quantifier elimination
if every first-order formula φ(x1,...,xn) over its signature is equivalent modulo T to a first-order formula ψ(x1,...,xn) without quantifiers, i.e.
holds in all models of T. For example the theory of algebraically closed fields in the signature σring=(×,+,−,0,1) has quantifier elimination because every formula is equivalent to a Boolean combination of equations between polynomials.
A substructure
of a σ-structure is a subset of its domain, closed under all functions in its signature σ, which is regarded as a σ-structure by restricting all functions and relations in σ to the subset. An embedding
of a σ-structure
into another σ-structure 
is a map f: A → B between the domains which can be written as an isomorphism of 
with a substructure of 
. Every embedding is an injective homomorphism, but the converse holds only if the signature contains no relation symbols.
If a theory does not have quantifier elimination, one can add additional symbols to its signature so that it does. Early model theory spent much effort on proving axiomatizability and quantifier elimination results for specific theories, especially in algebra. But often instead of quantifier elimination a weaker property suffices:
A theory T is called model-complete if every substructure of a model of T which is itself a model of T is an elementary substructure. There is a useful criterion for testing whether a substructure is an elementary substructure, called the Tarski–Vaught test. It follows from this criterion that a theory T is model-complete if and only if every first-order formula φ(x1,...,xn) over its signature is equivalent modulo T to an existential first-order formula, i.e. a formula of the following form:
,
where ψ is quantifier free. A theory that is not model-complete may or may not have a model completion, which is a related model-complete theory that is not, in general, an extension of the original theory. A more general notion is that of model companions.
κ. A theory T is called κ-categorical if any two models of T that are of cardinality κ are isomorphic. It turns out that the question of κ-categoricity depends critically on whether κ is bigger than the cardinality of the language (i.e.
+ |σ|, where |σ| is the cardinality of the signature). For finite or countable signatures this means that there is a fundamental difference between 
-cardinality and κ-cardinality for uncountable κ.
A few characterizations of
-categoricity
include:
This result, due independently to Engeler
, Ryll-Nardzewski and Svenonius
, is sometimes referred to as the Ryll-Nardzewski
theorem.
Further,
-categorical theories and their countable models have strong ties with oligomorphic group
s. They are often constructed as Fraïssé limits.
Michael Morley
's highly non-trivial result that (for countable languages) there is only one notion of uncountable categoricity was the starting point for modern model theory, and in particular classification theory and stability theory:
Uncountably categorical (i.e. κ-categorical for all uncountable cardinals κ) theories are from many points of view the most well-behaved theories. A theory that is both
-categorical and uncountably categorical is called totally categorical.
(which is expressed in a countable language) has a countable model; this is known as Skolem's paradox
, since there are sentences in set theory which postulate the existence of uncountable sets and yet these sentences are true in our countable model. Particularly the proof of the independence of the continuum hypothesis
requires considering sets in models which appear to be uncountable when viewed from within the model, but are countable to someone outside the model.
The model-theoretic viewpoint has been useful in set theory
; for example in Kurt Gödel's
work on the constructible universe, which, along with the method of forcing developed by Paul Cohen
can be shown to prove the (again philosophically interesting) independence
of the axiom of choice and the continuum hypothesis from the other axioms of set theory.
Similarly, if σ' is a signature that extends another signature σ, then a complete σ'-theory can be restricted to σ by intersecting the set of its sentences with the set of σ-formulas. Conversely, a complete σ-theory can be regarded as a σ'-theory, and one can extend it (in more than one way) to a complete σ'-theory. The terms reduct and expansion are sometimes applied to this relation as well.
One might say that to understand the full structure one must understand these quotients. When the equivalence relation is definable, we can give the previous sentence a precise meaning. We say that these structures are interpretable.
A key fact is that one can translate sentences from the language of the interpreted structures to the language of the original structure. Thus one can show that if a structure M interprets another whose theory is undecidable
, then M itself is undecidable.
(not to be confused with his incompleteness theorems
) says that a theory has a model if and only if it is consistent
, i.e. no contradiction is proved by the theory. This is the heart of model theory as it lets us answer questions about theories by looking at models and vice-versa. One should not confuse the completeness theorem with the notion of a complete theory. A complete theory is a theory that contains every sentence
or its negation. Importantly, one can find a complete consistent theory extending any consistent theory. However, as shown by Gödel's incompleteness theorems only in relatively simple cases will it be possible to have a complete consistent theory that is also recursive
, i.e. that can be described by a recursively enumerable set
of axioms. In particular, the theory of natural numbers has no recursive complete and consistent theory. Non-recursive theories are of little practical use, since it is undecidable
if a proposed axiom is indeed an axiom, making proof-checking a supertask
.
The compactness theorem
states that a set of sentences S is satisfiable if every finite subset of S is satisfiable. In the context of proof theory
the analogous statement is trivial, since every proof can have only a finite number of antecedents used in the proof. In the context of model theory, however, this proof is somewhat more difficult. There are two well known proofs, one by Gödel
(which goes via proofs) and one by Malcev (which is more direct and allows us to restrict the cardinality of the resulting model).
Model theory is usually concerned with first-order logic
, and many important results (such as the completeness and compactness theorems) fail in second-order logic
or other alternatives. In first-order logic all infinite cardinals look the same to a language which is countable. This is expressed in the Löwenheim–Skolem theorem
s, which state that any countable theory with an infinite model
has models of all infinite cardinalities (at least that of the language) which agree with 
on all sentences, i.e. they are 'elementarily equivalent'.
-structure 
, and a natural number 
. The set of definable subsets of 
over some parameters 
is a Boolean algebra. By Stone's representation theorem for Boolean algebras
there is a natural dual notion to this. One can consider this to be the topological space
consisting of maximal consistent sets of formulae over
. We call this the space of (complete) 
-types over 
, and write 
.
Now consider an element
. Then the set of all formulae 
with parameters in 
in free variables 
so that 
is consistent and maximal such. It is called the type of 
over 
.
One can show that for any
-type 
, there exists some elementary extension 
of 
and some 
so that 
is the type of 
over 
.
Many important properties in model theory can be expressed with types. Further many proofs go via constructing models with elements that contain elements with certain types and then using these elements.
Illustrative Example: Suppose
is an algebraically closed field
. The theory has quantifier elimination . This allows us to show that a type is determined exactly by the polynomial equations it contains. Thus the space of
-types over a subfield 
is bijective with the set of prime ideal
s of the polynomial ring
. This is the same set as the spectrum
of
. Note however that the topology considered on the type space is the constructible topology: a set of types is basic open
iff it is of the form
or of the form 
. This is finer than the Zariski topology
.
, is often regarded as being of a model-theoretical nature in retrospect. The first significant result in what is now model theory was a special case of the downward Löwenheim–Skolem theorem
, published by Leopold Löwenheim
in 1915. The compactness theorem
was implicit in work by Thoralf Skolem
, but it was first published in 1930, as a lemma in Kurt Gödel
's proof of his completeness theorem
. The Löwenheim–Skolems theorem and the compactness theorem received their respective general forms in 1936 and 1941 from Anatoly Maltsev
.
Mathematics
Mathematics is the study of quantity, space, structure, and change. Mathematicians seek out patterns and formulate new conjectures. Mathematicians resolve the truth or falsity of conjectures by mathematical proofs, which are arguments sufficient to convince other mathematicians of their validity...
, model theory is the study of (classes of) mathematical structures
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....
(e.g. groups
Group (mathematics)
In mathematics, a group is an algebraic structure consisting of a set together with an operation that combines any two of its elements to form a third element. To qualify as a group, the set and the operation must satisfy a few conditions called group axioms, namely closure, associativity, identity...
, fields
Field (mathematics)
In abstract algebra, a field is a commutative ring whose nonzero elements form a group under multiplication. As such it is an algebraic structure with notions of addition, subtraction, multiplication, and division, satisfying certain axioms...
, graphs
Graph (mathematics)
In mathematics, a graph is an abstract representation of a set of objects where some pairs of the objects are connected by links. The interconnected objects are represented by mathematical abstractions called vertices, and the links that connect some pairs of vertices are called edges...
, universes of 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...
) using tools from mathematical logic
Mathematical logic
Mathematical logic is a subfield of mathematics with close connections to foundations of mathematics, theoretical computer science and philosophical logic. The field includes both the mathematical study of logic and the applications of formal logic to other areas of mathematics...
.
Objects of study in model theory are models for 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...
s which are structures that give meaning to the sentences of these formal languages. If a model for a language moreover satisfies a particular sentence or theory (set of sentences satisfying special conditions), it is called a model of the sentence or theory.
Model theory has close ties to algebra
Algebra
Algebra is the branch of mathematics concerning the study of the rules of operations and relations, and the constructions and concepts arising from them, including terms, polynomials, equations and algebraic structures...
and universal algebra
Universal algebra
Universal algebra is the field of mathematics that studies algebraic structures themselves, not examples of algebraic structures....
.
This article focuses on finitary first order
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...
model theory of infinite structures. 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...
, which concentrates on finite structures, diverges significantly from the study of infinite structures in both the problems studied and the techniques used. Model theory in 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...
s or 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...
s is hampered by the fact that completeness
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....
does not in general hold for these logics. However, a great deal of study has also been done in such languages.
Introduction
Model theory recognises and is intimately concerned with a duality: It examines semanticalSemantics
Semantics is the study of meaning. It focuses on the relation between signifiers, such as words, phrases, signs and symbols, and what they stand for, their denotata....
elements by means of syntactical
Syntax
In linguistics, syntax is the study of the principles and rules for constructing phrases and sentences in natural languages....
elements of a corresponding language. To quote the first page of Chang
Chen Chung Chang
Chen Chung Chang is a mathematician who works in model theory. He obtained his PhD from Berkeley in 1955 on "Cardinal and Ordinal Factorization of Relation Types" under Alfred Tarski. He wrote the standard text on model theory. Chang's conjecture is named after him...
and Keisler
Howard Jerome Keisler
H. Jerome Keisler is an American mathematician, currently professor emeritus at University of Wisconsin–Madison. His research has included model theory and non-standard analysis.His Ph.D...
(1990):
- universal algebraUniversal algebraUniversal algebra is the field of mathematics that studies algebraic structures themselves, not examples of algebraic structures....
+ 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....
= model theory.
Model theory developed rapidly during the 1990s, and a more modern definition is provided by Wilfrid Hodges
Wilfrid Hodges
Wilfrid Augustine Hodges is a British mathematician, known for his work in model theory. He was Professor of Mathematics at Queen Mary, University of London from 1987 to 2006, and is the author of numerous books on logic....
(1997):
- model theory = algebraic geometryAlgebraic geometryAlgebraic geometry is a branch of mathematics which combines techniques of abstract algebra, especially commutative algebra, with the language and the problems of geometry. It occupies a central place in modern mathematics and has multiple conceptual connections with such diverse fields as complex...
− fieldField (mathematics)In abstract algebra, a field is a commutative ring whose nonzero elements form a group under multiplication. As such it is an algebraic structure with notions of addition, subtraction, multiplication, and division, satisfying certain axioms...
s.
In a similar way to proof theory
Proof theory
Proof theory is a branch of mathematical logic that represents proofs as formal mathematical objects, facilitating their analysis by mathematical techniques. Proofs are typically presented as inductively-defined data structures such as plain lists, boxed lists, or trees, which are constructed...
, model theory is situated in an area of interdisciplinarity
Interdisciplinarity
Interdisciplinarity involves the combining of two or more academic fields into one single discipline. An interdisciplinary field crosses traditional boundaries between academic disciplines or schools of thought, as new needs and professions have emerged....
between mathematics
Mathematics
Mathematics is the study of quantity, space, structure, and change. Mathematicians seek out patterns and formulate new conjectures. Mathematicians resolve the truth or falsity of conjectures by mathematical proofs, which are arguments sufficient to convince other mathematicians of their validity...
, philosophy
Philosophy
Philosophy is the study of general and fundamental problems, such as those connected with existence, knowledge, values, reason, mind, and language. Philosophy is distinguished from other ways of addressing such problems by its critical, generally systematic approach and its reliance on rational...
, and computer science
Computer science
Computer science or computing science is the study of the theoretical foundations of information and computation and of practical techniques for their implementation and application in computer systems...
. The most important professional organization in the field of model theory is the Association for Symbolic Logic
Association for Symbolic Logic
The Association for Symbolic Logic is an international organization of specialists in mathematical logic and philosophical logic—the largest such organization in the world. The ASL was founded in 1936, a crucial year in the development of modern logic, and its first president was Alonzo Church...
.
An incomplete and somewhat arbitrary subdivision of model theory is into classical model theory, model theory applied to groups and fields, and geometric model theory. A missing subdivision is 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...
, but this can arguably be viewed as an independent subfield of logic. Examples of early theorems from classical model theory include 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....
, the upward and downward Löwenheim–Skolem theorem
Löwenheim–Skolem theorem
In mathematical logic, the Löwenheim–Skolem theorem, named for Leopold Löwenheim and Thoralf Skolem, states that if a countable first-order theory has an infinite model, then for every infinite cardinal number κ it has a model of size κ...
s, Vaught
Robert Lawson Vaught
Robert Lawson Vaught was a mathematical logician, and one of the founders of model theory.-Life:Vaught was a bit of a musical prodigy in his youth, in his case the piano. He began his university studies at Pomona College, at age 16. When World War II broke out, he enlisted US Navy which assigned...
's two-cardinal theorem, Scott
Dana Scott
Dana Stewart Scott is the emeritus Hillman University Professor of Computer Science, Philosophy, and Mathematical Logic at Carnegie Mellon University; he is now retired and lives in Berkeley, California...
's isomorphism theorem, the omitting types theorem, and the Ryll-Nardzewski theorem. Examples of early results from model theory applied to fields are Tarski's elimination of quantifiers
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...
for real closed fields, Ax
James Ax
James Burton Ax was a mathematician who proved several results in algebra and number theory by using model theory. He shared the seventh Frank Nelson Cole Prize in Number Theory with Simon B. Kochen, which was awarded for a series of three joint papers on Diophantine problems.James Ax earned his...
's theorem on pseudo-finite fields, and Robinson
Abraham Robinson
Abraham Robinson was a mathematician who is most widely known for development of non-standard analysis, a mathematically rigorous system whereby infinitesimal and infinite numbers were incorporated into mathematics....
's development of nonstandard analysis. An important step in the evolution of classical model theory occurred with the birth of stability 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...
(through Morley's 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....
on uncountably categorical theories and Shelah
Saharon Shelah
Saharon Shelah is an Israeli mathematician. He is a professor of mathematics at the Hebrew University of Jerusalem and Rutgers University in New Jersey.-Biography:...
's classification program), which developed a calculus of independence and rank based on syntactical conditions satisfied by theories. During the last several decades applied model theory has repeatedly merged with the more pure stability theory. The result of this synthesis is called geometric model theory in this article (which is taken to include o-minimality, for example, as well as classical geometric stability theory). An example of a theorem from geometric model theory is Hrushovski
Ehud Hrushovski
Ehud Hrushovski is a mathematical logician. He is a Professor of Mathematics at the Hebrew University of Jerusalem.His father, Benjamin Harshav, is Emeritus Professor in Yale University and Tel Aviv University to Comparative Literature and a poet....
's proof of the Mordell–Lang conjecture for function fields. The ambition of geometric model theory is to provide a geography of mathematics by embarking on a detailed study of definable sets in various mathematical structures, aided by the substantial tools developed in the study of pure model theory.
Example
To illustrate the basic relationship involving syntax and semantics in the context of a non-trivial model, one can start, on the syntactic side, with suitable axioms for the natural numbers such as Peano axioms, and the associated theory. Going on to the semantic side, one has the usual counting numbers as a model. In the 1930s, Skolem developed alternative models satisfying the axioms. This illustrates what is meant by interpreting a language or theory in a particular model. A more traditional example is interpreting the axioms of a particular algebraic system such as a group, in the context of a model provided by a specific group.Universal algebra
Fundamental concepts in universal algebra are signaturesSignature (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...
σ and σ-algebras. Since these concepts are formally defined in the article on structure
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....
s, the present article can content itself with an informal introduction which consists in examples of how these terms are used.
- The standard signature of rings is σring = {×,+,−,0,1}, where × and + are binaryBinary operationIn mathematics, a binary operation is a calculation involving two operands, in other words, an operation whose arity is two. Examples include the familiar arithmetic operations of addition, subtraction, multiplication and division....
, − is unaryUnary operationIn mathematics, a unary operation is an operation with only one operand, i.e. a single input. Specifically, it is a functionf:\ A\to Awhere A is a set. In this case f is called a unary operation on A....
, and 0 and 1 are nullary. - The standard signature of semirings is σsmr = {×,+,0,1}, where the arities are as above.
- The standard signature of (multiplicative) groups is σgrp = {×,−1,1}, where × is binary, −1 is unary and 1 is nullary.
- The standard signature of monoids is σmnd = {×,1}.
- A ringRing (mathematics)In mathematics, a ring is an algebraic structure consisting of a set together with two binary operations usually called addition and multiplication, where the set is an abelian group under addition and a semigroup under multiplication such that multiplication distributes over addition...
is a σring-structure which satisfies the identities and - A groupGroup (mathematics)In mathematics, a group is an algebraic structure consisting of a set together with an operation that combines any two of its elements to form a third element. To qualify as a group, the set and the operation must satisfy a few conditions called group axioms, namely closure, associativity, identity...
is a σgrp-structure which satisfies the identitiesIdentity (mathematics)In mathematics, the term identity has several different important meanings:*An identity is a relation which is tautologically true. This means that whatever the number or value may be, the answer stays the same. For example, algebraically, this occurs if an equation is satisfied for all values of...
and - A monoidMonoidIn abstract algebra, a branch of mathematics, a monoid is an algebraic structure with a single associative binary operation and an identity element. Monoids are studied in semigroup theory as they are naturally semigroups with identity. Monoids occur in several branches of mathematics; for...
is a σmnd-structure which satisfies the identities and - A semigroupSemigroupIn mathematics, a semigroup is an algebraic structure consisting of a set together with an associative binary operation. A semigroup generalizes a monoid in that there might not exist an identity element...
is a {×}-structure which satisfies the identity - A magma is just a {×}-structure.
This is a very efficient way to define most classes of algebraic structure
Algebraic structure
In abstract algebra, an algebraic structure consists of one or more sets, called underlying sets or carriers or sorts, closed under one or more operations, satisfying some axioms. Abstract algebra is primarily the study of algebraic structures and their properties...
s, because there is also the concept of σ-homomorphism, which correctly specializes to the usual notions of homomorphism for groups, semigroups, magmas and rings. For this to work, the signature must be chosen well.
Terms such as the σring-term t(u,v,w) given by are used to define identities but also to construct free algebra
Free object
In mathematics, the idea of a free object is one of the basic concepts of abstract algebra. It is a part of universal algebra, in the sense that it relates to all types of algebraic structure . It also has a formulation in terms of category theory, although this is in yet more abstract terms....
s. An equational class
Variety (universal algebra)
In mathematics, specifically universal algebra, a variety of algebras is the class of all algebraic structures of a given signature satisfying a given set of identities. Equivalently, a variety is a class of algebraic structures of the same signature which is closed under the taking of homomorphic...
is a class of structures which, like the examples above and many others, is defined as the class of all σ-structures which satisfy a certain set of identities. Birkhoff's theorem states:
- A class of σ-structures is an equational class if and only if it is not empty and closed under subalgebras, homomorphic images, and direct products.
An important non-trivial tool in universal algebra are 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...
s
, where I is an infinite set indexing a system of σ-structures Ai, and U is an ultrafilterUltrafilter
In the mathematical field of set theory, an ultrafilter on a set X is a collection of subsets of X that is a filter, that cannot be enlarged . An ultrafilter may be considered as a finitely additive measure. Then every subset of X is either considered "almost everything" or "almost nothing"...
on I.
While model theory is generally considered a part of mathematical logic
Mathematical logic
Mathematical logic is a subfield of mathematics with close connections to foundations of mathematics, theoretical computer science and philosophical logic. The field includes both the mathematical study of logic and the applications of formal logic to other areas of mathematics...
, universal algebra, which grew out of Alfred North Whitehead
Alfred North Whitehead
Alfred North Whitehead, OM FRS was an English mathematician who became a philosopher. He wrote on algebra, logic, foundations of mathematics, philosophy of science, physics, metaphysics, and education...
's (1898) work on abstract algebra
Abstract algebra
Abstract algebra is the subject area of mathematics that studies algebraic structures, such as groups, rings, fields, modules, vector spaces, and algebras...
, is part of algebra
Algebra
Algebra is the branch of mathematics concerning the study of the rules of operations and relations, and the constructions and concepts arising from them, including terms, polynomials, equations and algebraic structures...
. This is reflected by their respective MSC
Mathematics Subject Classification
The Mathematics Subject Classification is an alphanumerical classification scheme collaboratively produced by staff of and based on the coverage of the two major mathematical reviewing databases, Mathematical Reviews and Zentralblatt MATH...
classifications. Nevertheless model theory can be seen as an extension of universal algebra.
Finite model theory
Finite model theory is the area of model theory which has the closest ties to universal algebra. Like some parts of universal algebra, and in contrast with the other areas of model theory, it is mainly concerned with finite algebras, or more generally, with finite σ-structureStructure (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....
s for signatures σ which may contain relation symbols as in the following example:
- The standard signature for graphs is σgrph={E}, where E is a binary relation symbol.
- A graph is a σgrph-structure satisfying the sentences
and 
.
A σ-homomorphism is a map that commutes with the operations and preserves the relations in σ. This definition gives rise to the usual notion of graph homomorphism
Graph homomorphism
In the mathematical field of graph theory a graph homomorphism is a mapping between two graphs that respects their structure. More concretely it maps adjacent vertices to adjacent vertices.-Definitions:...
, which has the interesting property that a bijective homomorphism need not be invertible. Structures are also a part of universal algebra; after all, some algebraic structure
Algebraic structure
In abstract algebra, an algebraic structure consists of one or more sets, called underlying sets or carriers or sorts, closed under one or more operations, satisfying some axioms. Abstract algebra is primarily the study of algebraic structures and their properties...
s such as ordered groups have a binary relation <. What distinguishes finite model theory from universal algebra is its use of more general logical sentences (as in the example above) in place of identities. (In a model-theoretic context an identity t=t
.)The logics employed in finite model theory are often substantially more expressive than first-order logic, the standard logic for model theory of infinite structures.
First-order logic
Whereas universal algebra provides the semanticsSemantics
Semantics is the study of meaning. It focuses on the relation between signifiers, such as words, phrases, signs and symbols, and what they stand for, their denotata....
for a signature
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...
, logic
Mathematical logic
Mathematical logic is a subfield of mathematics with close connections to foundations of mathematics, theoretical computer science and philosophical logic. The field includes both the mathematical study of logic and the applications of formal logic to other areas of mathematics...
provides the syntax
Syntax
In linguistics, syntax is the study of the principles and rules for constructing phrases and sentences in natural languages....
. With terms, identities and quasi-identities
Quasiidentity
In universal algebra, a quasiidentity is an implication of the formwhere s1, ..., sn, s and t1, ..., tn,t are terms built up from variables using the operation symbols of the specified signature....
, even universal algebra has some limited syntactic tools; first-order logic is the result of making quantification explicit and adding negation into the picture.
A first-order formula is built out of atomic formula
Atomic formula
In mathematical logic, an atomic formula is a formula with no deeper propositional structure, that is, a formula that contains no logical connectives or equivalently a formula that has no strict subformulas. Atoms are thus the simplest well-formed formulas of the logic...
s such as R(f(x,y),z) or y = x + 1 by means of the Boolean connectives
Table of logic symbols
In logic, a set of symbols is commonly used to express logical representation. As logicians are familiar with these symbols, they are not explained each time they are used. So, for students of logic, the following table lists many common symbols together with their name, pronunciation and related...
and prefixing of quantifiers or . A sentence is a formula in which each occurrence of a variable is in the scope of a corresponding quantifier. Examples for formulas are φ (or φ(x) to mark the fact that at most x is an unbound variable in φ) and ψ defined as follows:(Note that the equality symbol has a double meaning here.) It is intuitively clear how to translate such formulas into mathematical meaning. In the σsmr-structure
of the natural numbers, for example, an element n satisfies the formula φ if and only if n is a prime number. The formula ψ similarly defines irreducibility. Tarski gave a rigorous definition, sometimes called "Tarski's definition of truth"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...
, for the satisfaction relation
, so that one easily proves: is a prime number. is irreducible.A set T of sentences is called a (first-order) theory
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...
. A theory is satisfiable if it has a model
, i.e. a structure (of the appropriate signature) which satisfies all the sentences in the set T. ConsistencyConsistency
Consistency can refer to:* Consistency , the psychological need to be consistent with prior acts and statements* "Consistency", an 1887 speech by Mark Twain...
of a theory is usually defined in a syntactical way, but in first-order logic by the 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....
there is no need to distinguish between satisfiability and consistency. Therefore model theorists often use "consistent" as a synonym for "satisfiable".
A theory is called categorical if it determines a structure up to isomorphism, but it turns out that this definition is not useful, due to serious restrictions in the expressivity of first-order logic. The Löwenheim–Skolem theorem
Löwenheim–Skolem theorem
In mathematical logic, the Löwenheim–Skolem theorem, named for Leopold Löwenheim and Thoralf Skolem, states that if a countable first-order theory has an infinite model, then for every infinite cardinal number κ it has a model of size κ...
implies that for every theory T which has an infinite model and for every infinite 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...
κ, there is a model
such that the number of elements of is exactly κ. Therefore only finite structures can be described by a categorical theory.Lack of expressivity (when compared to higher logics such as 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....
) has its advantages, though. For model theorists the Löwenheim–Skolem theorem is an important practical tool rather than the source of 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...
. First-order logic is in some sense (for which see Lindström's theorem
Lindström's theorem
In mathematical logic, Lindström's theorem states that first-order logic is the strongest logic In mathematical logic, Lindström's theorem (named after Swedish logician Per Lindström) states that first-order logic is the strongest logic In mathematical logic, Lindström's theorem (named after...
) the most expressive logic for which both the Löwenheim–Skolem theorem and the compactness theorem hold:
- Compactness theoremCompactness theoremIn 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...
- Every unsatisfiable first-order theory has a finite unsatisfiable subset.
This important theorem, due to Gödel
Kurt Gödel
Kurt Friedrich Gödel was an Austrian logician, mathematician and philosopher. Later in his life he emigrated to the United States to escape the effects of World War II. One of the most significant logicians of all time, Gödel made an immense impact upon scientific and philosophical thinking in the...
, is of central importance in infinite model theory, where the words "by compactness" are commonplace. One way to prove it is by means of 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...
s. An alternative proof uses the completeness theorem, which is otherwise reduced to a marginal role in most of modern model theory.
Axiomatizability, elimination of quantifiers, and model-completeness
The first step, often trivial, for applying the methods of model theory to a class of mathematical objects such as groups, or trees in the sense of graph theory, is to choose a signature σ and represent the objects as σ-structures. The next step is to show that the class is an elementary classElementary 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 :...
, i.e. axiomatizable in first-order logic (i.e. there is a theory T such that a σ-structure is in the class if and only if it satisfies T). E.g. this step fails for the trees, since connectedness cannot be expressed in first-order logic. Axiomatizability ensures that model theory can speak about the right objects. Quantifier elimination can be seen as a condition which ensures that model theory does not say too much about the objects.
A theory T has 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...
if every first-order formula φ(x1,...,xn) over its signature is equivalent modulo T to a first-order formula ψ(x1,...,xn) without quantifiers, i.e.
holds in all models of T. For example the theory of algebraically closed fields in the signature σring=(×,+,−,0,1) has quantifier elimination because every formula is equivalent to a Boolean combination of equations between polynomials.A 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...
of a σ-structure is a subset of its domain, closed under all functions in its signature σ, which is regarded as a σ-structure by restricting all functions and relations in σ to the subset. An embedding
Embedding
In mathematics, an embedding is one instance of some mathematical structure contained within another instance, such as a group that is a subgroup....
of a σ-structure
into another σ-structure is a map f: A → B between the domains which can be written as an isomorphism of with a substructure of . Every embedding is an injective homomorphism, but the converse holds only if the signature contains no relation symbols.If a theory does not have quantifier elimination, one can add additional symbols to its signature so that it does. Early model theory spent much effort on proving axiomatizability and quantifier elimination results for specific theories, especially in algebra. But often instead of quantifier elimination a weaker property suffices:
A theory T is called model-complete if every substructure of a model of T which is itself a model of T is an elementary substructure. There is a useful criterion for testing whether a substructure is an elementary substructure, called the Tarski–Vaught test. It follows from this criterion that a theory T is model-complete if and only if every first-order formula φ(x1,...,xn) over its signature is equivalent modulo T to an existential first-order formula, i.e. a formula of the following form:
,where ψ is quantifier free. A theory that is not model-complete may or may not have a model completion, which is a related model-complete theory that is not, in general, an extension of the original theory. A more general notion is that of model companions.
Categoricity
As observed in the section on first-order logic, first-order theories cannot be categorical, i.e. they cannot describe a unique model up to isomorphism, unless that model is finite. But two famous model-theoretic theorems deal with the weaker notion of κ-categoricity for a cardinalCardinal 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...
κ. A theory T is called κ-categorical if any two models of T that are of cardinality κ are isomorphic. It turns out that the question of κ-categoricity depends critically on whether κ is bigger than the cardinality of the language (i.e.
+ |σ|, where |σ| is the cardinality of the signature). For finite or countable signatures this means that there is a fundamental difference between -cardinality and κ-cardinality for uncountable κ.A few characterizations of
-categoricityOmega-categorical theory
In mathematical logic, an omega-categorical theory is a theory that has only one countable model up to isomorphism. Omega-categoricity is the special case κ = \aleph_0 = ω of κ-categoricity, and omega-categorical theories are also referred to as ω-categorical...
include:
- For a complete first-order theory T in a finite or countable signature the following conditions are equivalent:
- T is
-categorical. - For every natural number n, the Stone space Sn(T) is finite.
- For every natural number n, the number of formulas φ(x1, ..., xn) in n free variables, up to equivalence modulo T, is finite.
- T is
This result, due independently to Engeler
Erwin Engeler
Erwin Engeler is a Swiss mathematician who did pioneering work on the interrelations between logic, computer science and scientific computation in the 20th century...
, Ryll-Nardzewski and Svenonius
Lars Svenonius
Lars Svenonius was a Swedish logician and philosopher.He was a visiting professor at University of California at Berkeley in 1962-63, then held a position at the University of Chicago from 1963-69, and was professor of philosophy at the University of Maryland from 1969 to 2009...
, is sometimes referred to as the Ryll-Nardzewski
Omega-categorical theory
In mathematical logic, an omega-categorical theory is a theory that has only one countable model up to isomorphism. Omega-categoricity is the special case κ = \aleph_0 = ω of κ-categoricity, and omega-categorical theories are also referred to as ω-categorical...
theorem.
Further,
-categorical theories and their countable models have strong ties with oligomorphic groupOligomorphic group
In group theory, a branch of mathematics, an oligomorphic group is a particular kind of permutation group. If a group G acts on a set S, then G is said to be oligomorphic if every Cartesian product, Sn of S has finitely many orbits under the action of G...
s. They are often constructed as Fraïssé limits.
Michael Morley
Michael D. Morley
Michael Darwin Morley is an American mathematician, currently professor emeritus at Cornell University.His research is in advanced mathematical logic and model theory, and he is best known for Morley's categoricity theorem, which he proved in his Ph.D. thesis "Categoricity in Power" in 1962.His...
's highly non-trivial result that (for countable languages) there is only one notion of uncountable categoricity was the starting point for modern model theory, and in particular classification theory and stability theory:
- Morley's categoricity theoremMorley's categoricity theoremIn model theory, a branch of mathematical logic, a theory is κ-categorical if it has exactly one model of cardinality κ up to isomorphism....
- If a first-order theory T in a finite or countable signature is κ-categorical for some uncountable cardinal κ, then T is κ-categorical for all uncountable cardinals κ.
Uncountably categorical (i.e. κ-categorical for all uncountable cardinals κ) theories are from many points of view the most well-behaved theories. A theory that is both
-categorical and uncountably categorical is called totally categorical.Model theory and set theory
Set theorySet 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...
(which is expressed in a countable language) has a countable model; this is known as 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...
, since there are sentences in set theory which postulate the existence of uncountable sets and yet these sentences are true in our countable model. Particularly the proof of the independence of the 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...
requires considering sets in models which appear to be uncountable when viewed from within the model, but are countable to someone outside the model.
The model-theoretic viewpoint has been useful in 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...
; for example in Kurt Gödel's
Kurt Gödel
Kurt Friedrich Gödel was an Austrian logician, mathematician and philosopher. Later in his life he emigrated to the United States to escape the effects of World War II. One of the most significant logicians of all time, Gödel made an immense impact upon scientific and philosophical thinking in the...
work on the constructible universe, which, along with the method of forcing developed by Paul Cohen
Paul Cohen (mathematician)
Paul Joseph Cohen was an American mathematician best known for his proof of the independence of the continuum hypothesis and the axiom of choice from Zermelo–Fraenkel set theory, the most widely accepted axiomatization of set theory.-Early years:Cohen was born in Long Branch, New Jersey, into a...
can be shown to prove the (again philosophically interesting) independence
Independence (mathematical logic)
In mathematical logic, independence refers to the unprovability of a sentence from other sentences.A sentence σ is independent of a given first-order theory T if T neither proves nor refutes σ; that is, it is impossible to prove σ from T, and it is also impossible to prove from T that...
of the axiom of choice and the continuum hypothesis from the other axioms of set theory.
Reducts and expansions
A field or a vector space can be regarded as a (commutative) group by simply ignoring some of its structure. The corresponding notion in model theory is that of a reduct of a structure to a subset of the original signature. The opposite relation is called an expansion - e.g. the (additive) group of the rational numbers, regarded as a structure in the signature {+,0} can be expanded to a field with the signature {×,+,1,0} or to an ordered group with the signature {+,0,<}.Similarly, if σ' is a signature that extends another signature σ, then a complete σ'-theory can be restricted to σ by intersecting the set of its sentences with the set of σ-formulas. Conversely, a complete σ-theory can be regarded as a σ'-theory, and one can extend it (in more than one way) to a complete σ'-theory. The terms reduct and expansion are sometimes applied to this relation as well.
Interpretability
Given a mathematical structure, there are very often associated structures which can be constructed as a quotient of part of the original structure via an equivalence relation. An important example is a quotient group of a group.One might say that to understand the full structure one must understand these quotients. When the equivalence relation is definable, we can give the previous sentence a precise meaning. We say that these structures are interpretable.
A key fact is that one can translate sentences from the language of the interpreted structures to the language of the original structure. Thus one can show that if a structure M interprets another whose theory is undecidable
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...
, then M itself is undecidable.
Using the compactness and completeness theorems
Gödel's completeness theoremGö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....
(not to be confused with his 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...
) says that a theory has a model if and only if it is consistent
Consistency
Consistency can refer to:* Consistency , the psychological need to be consistent with prior acts and statements* "Consistency", an 1887 speech by Mark Twain...
, i.e. no contradiction is proved by the theory. This is the heart of model theory as it lets us answer questions about theories by looking at models and vice-versa. One should not confuse the completeness theorem with the notion of a complete theory. A complete theory is a theory that contains every sentence
Sentence (mathematical logic)
In mathematical logic, a sentence of a predicate logic is a boolean-valued well formed formula with no free variables. A sentence can be viewed as expressing a proposition, something that may be true or false...
or its negation. Importantly, one can find a complete consistent theory extending any consistent theory. However, as shown by Gödel's incompleteness theorems only in relatively simple cases will it be possible to have a complete consistent theory that is also recursive
Recursive language
In mathematics, logic and computer science, a formal language is called recursive if it is a recursive subset of the set of all possible finite sequences over the alphabet of the language...
, i.e. that can be described by a 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:...
of axioms. In particular, the theory of natural numbers has no recursive complete and consistent theory. Non-recursive theories are of little practical use, since it is undecidable
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...
if a proposed axiom is indeed an axiom, making proof-checking a supertask
Supertask
In philosophy, a supertask is a quantifiably infinite number of operations that occur sequentially within a finite interval of time. Supertasks are called "hypertasks" when the number of operations becomes innumerably infinite. The term supertask was coined by the philosopher James F...
.
The 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...
states that a set of sentences S is satisfiable if every finite subset of S is satisfiable. In the context of proof theory
Proof theory
Proof theory is a branch of mathematical logic that represents proofs as formal mathematical objects, facilitating their analysis by mathematical techniques. Proofs are typically presented as inductively-defined data structures such as plain lists, boxed lists, or trees, which are constructed...
the analogous statement is trivial, since every proof can have only a finite number of antecedents used in the proof. In the context of model theory, however, this proof is somewhat more difficult. There are two well known proofs, one by Gödel
Kurt Gödel
Kurt Friedrich Gödel was an Austrian logician, mathematician and philosopher. Later in his life he emigrated to the United States to escape the effects of World War II. One of the most significant logicians of all time, Gödel made an immense impact upon scientific and philosophical thinking in the...
(which goes via proofs) and one by Malcev (which is more direct and allows us to restrict the cardinality of the resulting model).
Model theory is usually concerned with 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...
, and many important results (such as the completeness and compactness theorems) fail in 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....
or other alternatives. In first-order logic all infinite cardinals look the same to a language which is countable. This is expressed in the Löwenheim–Skolem theorem
Löwenheim–Skolem theorem
In mathematical logic, the Löwenheim–Skolem theorem, named for Leopold Löwenheim and Thoralf Skolem, states that if a countable first-order theory has an infinite model, then for every infinite cardinal number κ it has a model of size κ...
s, which state that any countable theory with an infinite model
has models of all infinite cardinalities (at least that of the language) which agree with on all sentences, i.e. they are 'elementarily equivalent'.Types
Fix an-structure , and a natural number . The set of definable subsets of over some parameters is a Boolean algebra. By Stone's representation theorem for Boolean algebrasStone's representation theorem for Boolean algebras
In mathematics, Stone's representation theorem for Boolean algebras states that every Boolean algebra is isomorphic to a field of sets. The theorem is fundamental to the deeper understanding of Boolean algebra that emerged in the first half of the 20th century. The theorem was first proved by Stone...
there is a natural dual notion to this. One can consider this to be the topological space
Topology
Topology is a major area of mathematics concerned with properties that are preserved under continuous deformations of objects, such as deformations that involve stretching, but no tearing or gluing...
consisting of maximal consistent sets of formulae over
. We call this the space of (complete) -types over , and write .Now consider an element
. Then the set of all formulae with parameters in in free variables so that is consistent and maximal such. It is called the type of over .One can show that for any
-type , there exists some elementary extension of and some so that is the type of over .Many important properties in model theory can be expressed with types. Further many proofs go via constructing models with elements that contain elements with certain types and then using these elements.
Illustrative Example: Suppose
is an algebraically closed fieldAlgebraically closed field
In mathematics, a field F is said to be algebraically closed if every polynomial with one variable of degree at least 1, with coefficients in F, has a root in F.-Examples:...
. The theory has quantifier elimination . This allows us to show that a type is determined exactly by the polynomial equations it contains. Thus the space of
-types over a subfield is bijective with the set of prime idealPrime ideal
In algebra , a prime ideal is a subset of a ring which shares many important properties of a prime number in the ring of integers...
s of the polynomial ring
Polynomial ring
In mathematics, especially in the field of abstract algebra, a polynomial ring is a ring formed from the set of polynomials in one or more variables with coefficients in another ring. Polynomial rings have influenced much of mathematics, from the Hilbert basis theorem, to the construction of...
. This is the same set as the spectrumSpectrum of a ring
In abstract algebra and algebraic geometry, the spectrum of a commutative ring R, denoted by Spec, is the set of all proper prime ideals of R...
of
. Note however that the topology considered on the type space is the constructible topology: a set of types is basic openOpen set
The concept of an open set is fundamental to many areas of mathematics, especially point-set topology and metric topology. Intuitively speaking, a set U is open if any point x in U can be "moved" a small amount in any direction and still be in the set U...
iff it is of the form
or of the form . This is finer than the Zariski topologyZariski topology
In algebraic geometry, the Zariski topology is a particular topology chosen for algebraic varieties that reflects the algebraic nature of their definition. It is due to Oscar Zariski and took a place of particular importance in the field around 1950...
.
Early history
Model theory as a subject has existed since approximately the middle of the 20th century. However some earlier research, especially in mathematical logicMathematical logic
Mathematical logic is a subfield of mathematics with close connections to foundations of mathematics, theoretical computer science and philosophical logic. The field includes both the mathematical study of logic and the applications of formal logic to other areas of mathematics...
, is often regarded as being of a model-theoretical nature in retrospect. The first significant result in what is now model theory was a special case of the downward Löwenheim–Skolem theorem
Löwenheim–Skolem theorem
In mathematical logic, the Löwenheim–Skolem theorem, named for Leopold Löwenheim and Thoralf Skolem, states that if a countable first-order theory has an infinite model, then for every infinite cardinal number κ it has a model of size κ...
, published by Leopold Löwenheim
Leopold Löwenheim
Leopold Löwenheim was a German mathematician, known for his work in mathematical logic. The Nazi regime forced him to retire because under the Nuremberg Laws he was considered only three quarters Aryan. In 1943 much of his work was destroyed during a bombing raid on Berlin...
in 1915. The 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...
was implicit in work by Thoralf Skolem
Thoralf Skolem
Thoralf Albert Skolem was a Norwegian mathematician known mainly for his work on mathematical logic and set theory.-Life:...
, but it was first published in 1930, as a lemma in Kurt Gödel
Kurt Gödel
Kurt Friedrich Gödel was an Austrian logician, mathematician and philosopher. Later in his life he emigrated to the United States to escape the effects of World War II. One of the most significant logicians of all time, Gödel made an immense impact upon scientific and philosophical thinking in the...
's proof of his 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....
. The Löwenheim–Skolems theorem and the compactness theorem received their respective general forms in 1936 and 1941 from Anatoly Maltsev
Anatoly Maltsev
Anatoly Ivanovich Maltsev was born in Misheronsky, near Moscow, and died in Novosibirsk, USSR. He was a mathematician noted for his work on the decidability of various algebraic groups...
.
See also
- Axiomatizable class
- Compactness theoremCompactness theoremIn 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...
- Descriptive complexityDescriptive complexityDescriptive 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 classes in the polynomial hierarchy, is precisely the...
- Elementary equivalenceElementary equivalenceIn 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....
- First-order theories
- ForcingForcing (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...
- Hyperreal numberHyperreal numberThe 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...
- Institutional model theoryInstitutional model theoryInstitutional 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...
- Kripke semanticsKripke semanticsKripke 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...
- Löwenheim–Skolem theoremLöwenheim–Skolem theoremIn mathematical logic, the Löwenheim–Skolem theorem, named for Leopold Löwenheim and Thoralf Skolem, states that if a countable first-order theory has an infinite model, then for every infinite cardinal number κ it has a model of size κ...
- Proof theoryProof theoryProof theory is a branch of mathematical logic that represents proofs as formal mathematical objects, facilitating their analysis by mathematical techniques. Proofs are typically presented as inductively-defined data structures such as plain lists, boxed lists, or trees, which are constructed...
- Saturated modelSaturated modelIn 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...
Free online texts
- Hodges, WilfridWilfrid HodgesWilfrid Augustine Hodges is a British mathematician, known for his work in model theory. He was Professor of Mathematics at Queen Mary, University of London from 1987 to 2006, and is the author of numerous books on logic....
, First-order Model theory. The Stanford Encyclopedia Of Philosophy, E. Zalta (ed.). - Simmons, Harold (2004), An introduction to Good old fashioned model theory. Notes of an introductory course for postgraduates (with exercises).
- J. Barwise and S. Feferman (editors), Model-Theoretic Logics, Perspectives in Mathematical Logic, Volume 8, New York: Springer-Verlag, 1985.