Stratification (mathematics)

Stratification has several usages in mathematics.

In mathematical logic

In mathematical logic, stratification is any consistent assignment of numbers to predicate symbols guaranteeing that a unique formal interpretationof a logical theory exists. Specifically, for Horn clausetheories, we say that such a theory is stratified if and only ifthere is a stratification assignment S that fulfills the following conditions:

# If a predicate P is positively derived from a predicate Q, then the stratification number of P must be greater than or equal to the stratification number of Q, in short $S(P)\; geq\; S(Q)$.
# If a predicate P is derived from a negated predicate Q, then the stratification number of P must be greater than the stratification number of Q, in short $S(P)\; >\; S(Q)$.

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 clausetheories. It has also been used by W.V. Quine (1937) to address Russell's paradox, which undermined Frege's central work "Grundgesetze der Arithmetik" (1902).

In set theory

In New Foundations (NF) and related set theories, a formula $phi$ in the language of first-order logic with equality and membership is said to bestratified if and only if there is a function$sigma$ which sends each variable appearing in $phi$ (considered as an item of syntax) toa natural number (this works equally well if all integers are used) in such a way thatany atomic formula $x\; in\; y$ appearing in $phi$ satisfies $sigma(x)+1\; =\; sigma(y)$ and any atomic formula $x\; =\; y$ appearing in $phi$ satisfies $sigma(x)\; =\; sigma(y)$.

It turns out that it is sufficient to require that these conditions be satisfied only whenboth variables in an atomic formula are bound in the set abstract $\{x\; mid\; phi\}$under consideration. A set abstract satisfying this weaker condition is said to beweakly stratified.

The stratification of New Foundations generalizes readily to languages with morepredicates and with term constructions. Each primitive predicate needs to have specifiedrequired displacements between values of $sigma$ at its (bound) argumentsin a (weakly) stratified formula. In a language with term constructions, terms themselvesneed to be assigned values under $sigma$, with fixed displacements from thevalues of each of their (bound) arguments in a (weakly) stratified formula. Defined termconstructions are neatly handled by (possibly merely implicitly) using the theoryof descriptions: a term $(iota\; x.phi)$ (the x such that $phi$) mustbe assigned the same value under $sigma$ as the variable x.

A formula is stratified if and only if it is possible to assign types to all variables appearingin the formula in such a way that it will make sense in a version TST of the theory oftypes described in the New Foundations article, and this is probably the best wayto understand the stratification of New Foundations in practice.

The notion of stratification can be extended to the lambda calculus; this is foundin papers of Randall Holmes.

In singularity theory

In singularity theory, there is a different meaning, of a decomposition of a topological space "X" into disjoint subsets each of which is a topological manifold (so that in particular a "stratification" defines a partition 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), and fit together manageably, this idea is often applied in geometry. Hassler Whitney and René Thom first defined formal conditions for stratification. See topologically stratified space.

In statistics

See stratified sampling.