Editing Stratification (mathematics) (section)

==In a specific set theory==

In [[New Foundations]] (NF) and related set theories, a formula <math>\phi</math> in the language of first-order logic with equality and membership is said to be
'''stratified''' if and only if there is a function
<math>\sigma</math> which sends each variable appearing in <math>\phi</math> (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 <math>x \in y</math> appearing in <math>\phi</math> satisfies <math>\sigma(x)+1 = \sigma(y)</math> and any [[atomic formula]] <math>x = y</math> appearing in <math>\phi</math> satisfies <math>\sigma(x) = \sigma(y)</math>.

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 <math>\{x \mid \phi\}</math>
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.  Each primitive predicate needs to have specified
required displacements between values of <math>\sigma</math> at its (bound) arguments
in a (weakly) stratified formula.  In a language with term constructions, terms themselves
need to be assigned values under <math>\sigma</math>, 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 <math>(\iota x.\phi)</math> (the x such that <math>\phi</math>) must
be assigned the same value under <math>\sigma</math> 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]] 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).
{{cite book
 | last = Quine
 | first = Willard Van Orman
 | title = From a Logical Point of View
 | publisher = [[Harper & Row]]
 | edition = 2nd
 | location = New York
 | orig-year = 1961
 | date = 1963
 | page = 90
 | lccn = 61-15277
 }}