Stratification has several usages in mathematics.
In mathematical logic
In
mathematical logic
Mathematical logic is the study of logic, formal logic within mathematics. Major subareas include model theory, proof theory, set theory, and recursion theory. Research in mathematical logic commonly addresses the mathematical properties of for ...
, stratification is any consistent assignment of numbers to
predicate
Predicate or predication may refer to:
* Predicate (grammar), in linguistics
* Predication (philosophy)
* several closely related uses in mathematics and formal logic:
**Predicate (mathematical logic)
**Propositional function
**Finitary relation, o ...
symbols guaranteeing that a unique formal
interpretation of a logical theory exists. Specifically, we say that a set of
clauses
In language, a clause is a constituent that comprises a semantic predicand (expressed or not) and a semantic predicate. A typical clause consists of a subject and a syntactic predicate, the latter typically a verb phrase composed of a verb with ...
of the form
is stratified if and only if
there is a stratification assignment S that fulfills the following conditions:
# If a predicate P is positively derived from a predicate Q (i.e., P is the head of a rule, and Q occurs positively in the body of the same rule), then the stratification number of P must be greater than or equal to the stratification number of Q, in short
.
# If a predicate P is derived from a negated predicate Q (i.e., P is the head of a rule, and Q occurs negatively in the body of the same rule), then the stratification number of P must be greater than the stratification number of Q, in short
.
The notion of stratified negation leads to a very effective operational semantics for stratified programs in terms of the stratified least fixpoint, that is obtained by iteratively applying the fixpoint operator to each ''stratum'' of the program, from the lowest one up.
Stratification is not only useful for guaranteeing unique interpretation of
Horn clause In mathematical logic and logic programming, a Horn clause is a logical formula of a particular rule-like form which gives it useful properties for use in logic programming, formal specification, and model theory. Horn clauses are named for the log ...
theories.
In a specific set theory
In
New Foundations
In mathematical logic, New Foundations (NF) 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 ...
(NF) and related set theories, a formula
in the language of first-order logic with equality and membership is said to be
stratified if and only if there is a function
which sends each variable appearing in
(considered as an item of syntax) to
a natural number (this works equally well if all integers are used) in such a way that
any atomic formula
appearing in
satisfies
and any
atomic formula
In mathematical logic, an atomic formula (also known as an atom or a prime 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 subformu ...
appearing in
satisfies
.
It turns out that it is sufficient to require that these conditions be satisfied only when
both variables in an atomic formula are bound in the set abstract
under consideration. A set abstract satisfying this weaker condition is said to be
weakly stratified.
The stratification of
New Foundations
In mathematical logic, New Foundations (NF) 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 ...
generalizes readily to languages with more
predicates and with term constructions. Each primitive predicate needs to have specified
required displacements between values of
at its (bound) arguments
in a (weakly) stratified formula. In a language with term constructions, terms themselves
need to be assigned values under
, with fixed displacements from the
values of each of their (bound) arguments in a (weakly) stratified formula. Defined term
constructions are neatly handled by (possibly merely implicitly) using the theory
of descriptions: a term
(the x such that
) must
be assigned the same value under
as the variable x.
A formula is stratified if and only if it is possible to assign types to all variables appearing
in the formula in such a way that it will make sense in a version TST of the theory of
types described in the
New Foundations
In mathematical logic, New Foundations (NF) 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 ...
article, and this is probably the best way
to understand the stratification of
New Foundations
In mathematical logic, New Foundations (NF) 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 ...
in practice.
The notion of stratification can be extended to the
lambda calculus
Lambda calculus (also written as ''λ''-calculus) is a formal system in mathematical logic for expressing computation based on function abstraction and application using variable binding and substitution. It is a universal model of computation ...
; this is found
in papers of Randall Holmes.
A motivation for the use of stratification is to address
Russell's paradox
In mathematical logic, Russell's paradox (also known as Russell's antinomy) is a set-theoretic paradox discovered by the British philosopher and mathematician Bertrand Russell in 1901. Russell's paradox shows that every set theory that contains a ...
, the antinomy considered to have undermined
Frege
Friedrich Ludwig Gottlob Frege (; ; 8 November 1848 – 26 July 1925) was a German philosopher, logician, and mathematician. He was a mathematics professor at the University of Jena, and is understood by many to be the father of analytic philo ...
's central work ''
Grundgesetze der Arithmetik
''The Foundations of Arithmetic'' (german: Die Grundlagen der Arithmetik) is a book by Gottlob Frege, published in 1884, which investigates the Philosophy, philosophical foundations of arithmetic. Frege refutes other theories of number and develop ...
'' (1902).
In topology
In
singularity theory
In mathematics, singularity theory studies spaces that are almost manifolds, but not quite. A string can serve as an example of a one-dimensional manifold, if one neglects its thickness. A singularity can be made by balling it up, dropping it ...
, there is a different meaning, of a decomposition of a
topological space
In mathematics, a topological space is, roughly speaking, a geometrical space in which closeness is defined but cannot necessarily be measured by a numeric distance. More specifically, a topological space is a set whose elements are called points ...
''X'' into disjoint subsets each of which is a
topological manifold In topology, a branch of mathematics, a topological manifold is a topological space that locally resembles real ''n''-dimensional Euclidean space. Topological manifolds are an important class of topological spaces, with applications throughout mathe ...
(so that in particular a ''stratification'' defines a
partition
Partition may refer to:
Computing Hardware
* Disk partitioning, the division of a hard disk drive
* Memory partition, a subdivision of a computer's memory, usually for use by a single job
Software
* Partition (database), the division of a ...
of the topological space). This is not a useful notion when unrestricted; but when the various strata are defined by some recognisable set of conditions (for example being
locally closed In topology, a branch of mathematics, a subset E of a topological space X is said to be locally closed if any of the following equivalent conditions are satisfied:
* E is the intersection of an open set and a closed set in X.
* For each point x\in E ...
), and fit together manageably, this idea is often applied in geometry.
Hassler Whitney
Hassler Whitney (March 23, 1907 – May 10, 1989) was an American mathematician. He was one of the founders of singularity theory, and did foundational work in manifolds, embeddings, immersions, characteristic classes, and geometric integration t ...
and
René Thom
René Frédéric Thom (; 2 September 1923 – 25 October 2002) was a French mathematician, who received the Fields Medal in 1958.
He made his reputation as a topologist, moving on to aspects of what would be called singularity theory; he became w ...
first defined formal conditions for stratification. See
Whitney stratification In differential topology, a branch of mathematics, the Whitney conditions are conditions on a pair of submanifolds of a manifold introduced by Hassler Whitney in 1965.
A stratification of a topological space is a finite filtration by closed sub ...
and
topologically stratified space
In mathematics, topology (from the Greek words , and ) is concerned with the properties of a geometric object that are preserved under continuous deformations, such as stretching, twisting, crumpling, and bending; that is, without closing ho ...
.
In statistics
See
stratified sampling
In statistics, stratified sampling is a method of sampling from a population which can be partitioned into subpopulations.
In statistical surveys, when subpopulations within an overall population vary, it could be advantageous to sample each s ...
.
{{DEFAULTSORT:Stratification (Mathematics)
Mathematical logic
Mathematical terminology
Set theory
Stratifications