Схема свёртывания

Схема свёртывания (Шаблон:Lang-en) — схема аксиом наивной теории множеств; неформально говорит о том, что для каждого свойства существует множество, состоящее в точности из тех элементов, что удовлетворяют этому свойству. Схема свёртывания формализует известное дидактическое определение множества, гласящее, что «множество — это совокупность элементов, обладающих общим свойством». На языке логики предикатов схема свёртывания записывается следующим образом:

$\mathrm{\exists }A\mathrm{\forall }x(x\in A\leftrightarrow \phi )$,

где $\phi$ — любая формула языка логики предикатов с равенством и двуместным предикатным символом $\in$, в которую не входит свободно переменная $A$. Таким образом, схема представляет собой набор аксиом по одной для каждой конкретной формулы $\phi$Шаблон:Sfn.

Схема свёртывания является противоречивой. Для вывода противоречия в наивной теории множеств даже не нужно использовать аксиому объёмности: схема свёртывания сама по себе противоречива.

Противоречивость

Из схемы свёртывания можно вывести противоречие. Одно из наиболее известных выводимых из неё противоречий — парадоксом Рассела.

НапримерШаблон:Sfn, для формулы:

$\phi :\leftrightarrow \mathrm{\neg }(x\in x)$

схема свёртывания утверждает, что существует такое множество $A$, что:

$\mathrm{\forall }xx\in A\leftrightarrow \mathrm{\neg }(x\in x)$;

если взять $x$ равный $A$, то:

$A\in A\leftrightarrow \mathrm{\neg }(A\in A)$ — противоречие.

Также есть и другие известные противоречия, например парадокс Кантора или парадокс Бурали-Форти.

Есть различные модификации схемы свёртывания для того, чтобы избавить её от противоречий.

Схема выделения

Шаблон:Основная статья Схема ограниченного свёртывания (выделения) постулирует существование множества удовлетворяющих некоторому свойству элементов уже существующего множества. Схема выделения позволяет выделять подмножества при помощи любой формулы. Формально схема записывается так:

$\mathrm{\forall }B\mathrm{\exists }A\mathrm{\forall }x(x\in A\leftrightarrow x\in B\wedge \phi )$

Данная схема является основным способом построения множеств в теориях множеств Цермело и Цермело — Френкеля. Полную схему свёртывания иногда называют схемой неограниченного свёртывания или схемой неограниченного выделения.Шаблон:Sfn

Схема свёртывания классов

В теории множеств фон Неймана — Бернайса — Гёделя кроме множеств присутствуют также классы. Классы могут состоять из всех множеств, удовлетворяющих некоторому свойству, что и утверждает данный аналог схемы свёртывания:

$\mathrm{\exists }A\mathrm{\forall }x(x\in A\leftrightarrow \phi )$.

Отличие от обычной схемы свёртывания здесь в том, что маленькими буквами обозначаются множества, а большими — классы. Стоит понимать, что класс, полученный в результате применения схемы свёртывания, может не оказаться множеством. Также данная схема не позволяет строить совокупности классов, обладающих некоторым свойством, поскольку не все классы могут принадлежать другомуШаблон:Sfn.

Схема свёртывания в теории типов

В простой теории типов схема свёртывания выглядит следующим образом:

$\mathrm{\exists }{A}_{n+1}\mathrm{\forall }{x}_n(x_n\in A_{n+1}\leftrightarrow \phi )$,

где индекс переменных обозначает их тип. В теории типов множеству типа $n+1$ позволяется иметь лишь элементы типа $n$, поэтому формулы вида $x\in x$ просто не допускаютсяШаблон:Sfn.

Схема свёртывания для стратифицируемых формул

В новых основаниях Куайна используется иной подход для борьбы с противоречивостью схемы свёртывания. В отличие от схемы выделения, где ограничения накладываются на элементы, в новых основаниях ограничения накладываются на формулы. Требуется, чтобы формула была стратифицируемой, то есть чтобы было возможно расставить в ней для каждой переменной типы так, чтобы это была корректная формула простой теории типов. Схема свёртывания имеет такой вид:

$\mathrm{\exists }A\mathrm{\forall }x(x\in A\leftrightarrow \phi )$,

где $\phi$ — стратифицируемая формула.Шаблон:Sfn

Литература

• Шаблон:Книга