In mathematical logic

In mathematical logic

Mathematical logic

Mathematical logic is a subfield of mathematics with close connections to foundations of mathematics, theoretical computer science and philosophical logic. The field includes both the mathematical study of logic and the applications of formal logic to other areas of mathematics...

, stratification is any consistent assignment of numbers to predicate symbols guaranteeing that a unique formal interpretation

Interpretation (logic)

An interpretation is an assignment of meaning to the symbols of a formal language. Many formal languages used in mathematics, logic, and theoretical computer science are defined in solely syntactic terms, and as such do not have any meaning until they are given some interpretation...

 of a logical theory exists. Specifically, we say that a set of clauses

Clause (logic)

In logic, a clause is a finite disjunction ofliterals. Clausesare usually written as follows, where the symbols l_i areliterals:l_1 \vee \cdots \vee l_nIn some cases, clauses are written as sets of literals, so that clause above...

 of the form is stratified if and only if
there is a stratification assignment S that fulfills the following conditions:

1. 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 .
2. 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. It has also been used by W.V. Quine (1937) to address Russell's paradox

Russell's paradox

In the foundations of mathematics, Russell's paradox , discovered by Bertrand Russell in 1901, showed that the naive set theory created by Georg Cantor leads to a contradiction...

, which undermined Frege's central work Grundgesetze der Arithmetik (1902).

In set theory

In New Foundations

New Foundations

In mathematical logic, New Foundations 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 for Mathematical Logic"; hence the name...

 (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

Atomic formula

In mathematical logic, an atomic 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 subformulas. Atoms are thus the simplest well-formed formulas of the logic...

  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

New Foundations

In mathematical logic, New Foundations 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 for Mathematical Logic"; hence the name...

 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

New Foundations

In mathematical logic, New Foundations 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 for Mathematical Logic"; hence the name...

 article, and this is probably the best way
to understand the stratification of New Foundations

New Foundations

In mathematical logic, New Foundations 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 for Mathematical Logic"; hence the name...

 in practice.

The notion of stratification can be extended to the lambda calculus

Lambda calculus

In mathematical logic and computer science, lambda calculus, also written as λ-calculus, is a formal system for function definition, function application and recursion. The portion of lambda calculus relevant to computation is now called the untyped lambda calculus...

; this is found
in papers of Randall Holmes.

In singularity theory

In singularity theory

Singularity theory

-The notion of singularity:In mathematics, singularity theory is the study of the failure of manifold structure. A loop of string can serve as an example of a one-dimensional manifold, if one neglects its width. What is meant by a singularity can be seen by dropping it on the floor...

, there is a different meaning, of a decomposition of a topological space

Topological space

Topological spaces are mathematical structures that allow the formal definition of concepts such as convergence, connectedness, and continuity. They appear in virtually every branch of modern mathematics and are a central unifying notion...

 X into disjoint subsets each of which is a topological manifold

Topological manifold

In mathematics, a topological manifold is a topological space which looks locally like Euclidean space in a sense defined below...

 (so that in particular a stratification defines a partition

Partition of a set

In mathematics, a partition of a set X is a division of X into non-overlapping and non-empty "parts" or "blocks" or "cells" that cover all of X...

 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

Hassler Whitney

Hassler Whitney was an American mathematician. He was one of the founders of singularity theory, and did foundational work in manifolds, embeddings, immersions, and characteristic classes.-Work:...

 and René Thom

René Thom

René Frédéric Thom was a French mathematician. He made his reputation as a topologist, moving on to aspects of what would be called singularity theory; he became world-famous among the wider academic community and the educated general public for one aspect of this latter interest, his work as...

 first defined formal conditions for stratification. See topologically stratified space

Topologically stratified space

In topology, a branch of mathematics, a topologically stratified space is a space X that has been decomposed into pieces called strata; these strata are topological manifolds and are required to fit together in a certain way...

.