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, for Horn clause theories, we say that such a theory is stratified if and only if there is a stratification assignment S that fulfills the following conditions:

(A) 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 .

(B) 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).

Stratification is not only guaranteeing unique interpretation of Horn clause theories. 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 singularity theory, there is a different meaning, of a decomposition of a topological space X into disjoint subsets (so that stratification is to spaces what partition is to sets). 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 defined formal conditions for stratification.