Feferman–Vaught theorem in
model theory
In mathematical logic, model theory is the study of the relationship between formal theories (a collection of sentences in a formal language expressing statements about a mathematical structure), and their models (those structures in which the s ...
is a theorem by
Solomon Feferman
Solomon Feferman (December 13, 1928 – July 26, 2016) was an American philosopher and mathematician who worked in mathematical logic.
Life
Solomon Feferman was born in The Bronx in New York City to working-class parents who had immigrated to th ...
and
Robert Lawson Vaught
Robert Lawson Vaught (April 4, 1926 – April 2, 2002) was a mathematical logician and one of the founders of model theory.first-order theory
First-order logic—also known as predicate logic, quantificational logic, and first-order predicate calculus—is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quantif ...
of a product of first-order structures to the first-order theory of elements of the structure.
The theorem is considered as one of the standard results in model theory. The theorem extends the previous result of
Andrzej Mostowski on direct products of theories.
It generalizes (to formulas with arbitrary quantifiers) the property in
universal algebra
Universal algebra (sometimes called general algebra) is the field of mathematics that studies algebraic structures themselves, not examples ("models") of algebraic structures.
For instance, rather than take particular groups as the object of stu ...
that equalities (identities) carry over to
direct products of
algebraic structure
In mathematics, an algebraic structure consists of a nonempty set ''A'' (called the underlying set, carrier set or domain), a collection of operations on ''A'' (typically binary operations such as addition and multiplication), and a finite set of ...
s (which is a consequence of one direction of
Birkhoff's theorem).
Direct product of structures
Consider a first-order logic
signature
A signature (; from la, signare, "to sign") is a handwritten (and often stylized) depiction of someone's name, nickname, or even a simple "X" or other mark that a person writes on documents as a proof of identity and intent. The writer of a ...
''L''.
The definition of product structures takes a family of ''L''-structures
for
for some index set ''I'' and defines the product structure
, which is also an ''L''-structure, with all functions and relations defined pointwise.
The definition generalizes
direct product in universal algebra to relational first-order structures, which contain not only function symbols but also relation symbols.
If
is a relation symbol with
arguments in ''L'' and
are elements of the
cartesian product
In mathematics, specifically set theory, the Cartesian product of two sets ''A'' and ''B'', denoted ''A''×''B'', is the set of all ordered pairs where ''a'' is in ''A'' and ''b'' is in ''B''. In terms of set-builder notation, that is
: A\ti ...
, we define the interpretation of
in
by
:
When
is a functional relation, this definition reduces to the definition of
direct product in universal algebra.
Statement of the theorem for direct products
For a first-order logic formula
in signature ''L'' with free variables, and for an interpretation
of the variables
, we define the set of indices
for which
holds in
:
Given a first-order formula with free variables
, there is an algorithm to compute its equivalent game normal form, which is a finite disjunction
of mutually contradictory formulas.
The Feferman-Vaught theorem gives an
algorithm
In mathematics and computer science, an algorithm () is a finite sequence of rigorous instructions, typically used to solve a class of specific Computational problem, problems or to perform a computation. Algorithms are used as specificat ...
that takes a first-order formula
and constructs a formula
that reduces the condition that
holds in the product to the condition that
holds in the interpretation of
sets of indices:
:
Formula
is thus a formula with
free set variables, for example, in the first-order theory of
Boolean algebra
In mathematics and mathematical logic, Boolean algebra is a branch of algebra. It differs from elementary algebra in two ways. First, the values of the variables are the truth values ''true'' and ''false'', usually denoted 1 and 0, whereas in e ...
of sets.
Proof idea
Formula
can be constructed following the structure of the starting formula
. When
is quantifier free then, by definition of direct product above it follows
:
Consequently, we can take
to be the equality
in the language of boolean algebra of sets (equivalently, the
field of sets
In mathematics, a field of sets is a mathematical structure consisting of a pair ( X, \mathcal ) consisting of a set X and a family \mathcal of subsets of X called an algebra over X that contains the empty set as an element, and is closed un ...
).
Extending the condition to quantified formulas can be viewed as a form of
quantifier elimination Quantifier elimination is a concept of simplification used in mathematical logic, model theory, and theoretical computer science. Informally, a quantified statement "\exists x such that \ldots" can be viewed as a question "When is there an x such t ...
, where quantification over product elements
in
is reduced to quantification over subsets of
.
Generalized products
It is often of interest to consider
substructure of the direct product structure. If the restriction that defines product elements that belong to the substructure can be expressed as a condition on the sets of index elements, then the results can be generalized.
An example is the substructure of product elements that are constant at all but finitely many indices. Assume that the language ''L'' contains a constant symbol
and consider the substructure containing only those product elements
for which the set
:
is finite. The theorem then reduces the truth value in such substructure to a formula
in the boolean algebra of sets, where certain sets are restricted to be finite.
One way to define generalized products is to consider those
substructures where the sets
belong to some boolean algebra
of sets
of indices (a subset of the powerset set algebra
), and where the product substructure admits gluing.
Here admitting gluing refers to the following closure condition: if
are two product elements and
is the element of the boolean algebra, then so is the element
defined by "gluing"
and
according to
:
:
Consequences
Feferman-Vaught theorem implies the decidability of
Skolem arithmetic by viewing, via
fundamental theorem of arithmetic
In mathematics, the fundamental theorem of arithmetic, also called the unique factorization theorem and prime factorization theorem, states that every integer greater than 1 can be represented uniquely as a product of prime numbers, up to the ord ...
, the structure natural numbers with multiplication as a generalized product (power) of
Presburger arithmetic
Presburger arithmetic is the first-order theory of the natural numbers with addition, named in honor of Mojżesz Presburger, who introduced it in 1929. The signature of Presburger arithmetic contains only the addition operation and equality, omit ...
structures.
Model theory
In mathematical logic, model theory is the study of the relationship between formal theories (a collection of sentences in a formal language expressing statements about a mathematical structure), and their models (those structures in which the s ...
References
{{reflist