Stratification (mathematics)

In mathematical logic, stratification is any consistent assignment of numbers to predicate symbols guaranteeing that a unique formal interpretation of a logical theory exists.

Stratification is not only useful for guaranteeing unique interpretation of Horn clause theories.

In 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

(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

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

A set abstract satisfying this weaker condition is said to be weakly stratified.

The stratification of 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

, with fixed displacements from the values of each of their (bound) arguments in a (weakly) stratified formula.

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 article, and this is probably the best way to understand the stratification of New Foundations in practice.

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

A motivation for the use of stratification is to address Russell's paradox, the antinomy considered to have undermined Frege's central work Grundgesetze der Arithmetik (1902).

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 Whitney stratification and topologically stratified space.