Стратификация имеет несколько применений в математике.
В математической логике
В математической логике , стратификация любое последовательное присвоение номеров для предикатных символов , гарантирующих , что единственное формальное толкование логической теории существует. В частности, мы говорим, что набор предложений вида стратифицирован тогда и только тогда, когда существует присваивание стратификации S, которое удовлетворяет следующим условиям:
- Если предикат P положительно получен из предиката Q (т. Е. P является главой правила, а Q положительно встречается в теле того же правила), то число стратификации P должно быть больше или равно стратификации количество Q, короче .
- Если предикат P является производным от отрицательного предиката Q (т. Е. P является главой правила, а Q встречается в теле того же правила отрицательно), то число стратификации P должно быть больше, чем число расслоения Q , коротко .
Понятие стратифицированного отрицания приводит к очень эффективной операционной семантике для стратифицированных программ в терминах стратифицированной наименьшей фиксированной точки, которая получается путем итеративного применения оператора фиксированной точки к каждому слою программы, начиная с самого нижнего. Стратификация полезна не только для обеспечения уникальной интерпретации теорий предложения Хорна .
В конкретной теории множеств
В New Foundations (NF) и связанных теориях множеств формулана языке логики первого порядка с равенством и принадлежностью называется стратифицированной тогда и только тогда, когда существует функция который отправляет каждую переменную, появляющуюся в (рассматривается как элемент синтаксиса) в натуральное число (это работает одинаково хорошо, если используются все целые числа) таким образом, что любая атомарная формула появляясь в удовлетворяет и любая атомарная формула появляясь в удовлетворяет .
Оказывается, достаточно потребовать, чтобы эти условия выполнялись только тогда, когда обе переменные в атомарной формуле связаны в множестве abstract на рассмотрении. Абстрактное множество, удовлетворяющее этому более слабому условию, называется слабо стратифицированным .
Стратификация Новых оснований легко обобщается на языки с большим количеством предикатов и с термическими конструкциями. В каждом примитивном предикате должны быть указаны необходимые смещения между значениямипо его (связанным) аргументам в (слабо) стратифицированной формуле. В языке с термическими конструкциями самим терминам необходимо присвоить значения в соответствии с, с фиксированными отклонениями от значений каждого из их (связанных) аргументов в (слабо) стратифицированной формуле. Конструкции определенных терминов аккуратно обрабатываются (возможно, просто неявно) с помощью теории описаний: термин (x такой, что ) должно быть присвоено то же значение под как переменная x.
Формула стратифицирована тогда и только тогда, когда можно присвоить типы всем переменным, фигурирующим в формуле, таким образом, чтобы это имело смысл в версии TST теории типов, описанной в статье New Foundations , и это, вероятно, лучший способ понять расслоение Новых Оснований на практике.
Понятие стратификации можно распространить на лямбда-исчисление ; это можно найти в статьях Рэндалла Холмса.
Мотивация использования стратификации состоит в том, чтобы обратиться к парадоксу Рассела , антиномии, которая, как считается, подорвала центральную работу Фреге Grundgesetze der Arithmetik (1902). Куайн, Уиллард Ван Орман (1963) [1961]. С логической точки зрения (2-е изд.). Нью-Йорк: Харпер и Роу . п. 90. LCCN 61-15277 .
В топологии
В теории особенностей есть другой смысл разложения топологического пространства X на непересекающиеся подмножества, каждое из которых является топологическим многообразием (так, что, в частности, стратификация определяет разбиение топологического пространства). Это бесполезное понятие, если оно не ограничено; но когда различные страты определяются некоторым узнаваемым набором условий (например, являются локально замкнутыми ) и управляются друг с другом, эта идея часто применяется в геометрии. Хасслер Уитни и Рене Том впервые определили формальные условия стратификации. См. Стратификацию Уитни и топологически стратифицированное пространство .