Stratification (mathematics)

Stratification has several usages in 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. Specifically, we say that a set of clauses 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 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 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 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 generalizes readily to languages with more predicates and with term constructions.