Трюк Даны Скотта

---

Трюк Даны Скотта — трюк, позволяющий факторизовать собственный класс в теории множеств Цермело — Френкеля^[1]. При помощи него в ZF можно определить изоморфный тип, в частности мощность множества^[2]. Возможность применения трюка Даны Скотта существенно зависит от аксиомы регулярности.

Пусть ${\displaystyle A}$ — некоторый непустой класс, на котором задано отношение-класс эквивалентности ${\displaystyle \sim }$. Требуется построить в некотором смысле факторкласс, то есть такой класс ${\displaystyle A/\sim }$, каждому элементу которого будет взаимно однозначно соответствовать класс эквивалентности ${\displaystyle A}$ по ${\displaystyle \sim }$.

Взять и просто определить ${\displaystyle A/\sim }$ как совокупность всех классов эквивалентности ${\displaystyle A}$ по ${\displaystyle \sim }$ не получится — какие-то из классов эквивалентности могут оказаться собственными, а собственные классы не могут быть элементами других классов. Поэтому для определения такой конструкции приходится искать обходные пути. Один из таких путей был предложен Даной Скоттом.

Как известно, в ZF все множества полностью описываются иерархией фон Неймана, то есть каждое множество имеет ранг (эта часть полагается на аксиому регулярности). Если в некотором классе взять подкласс всех элементов какого-то определённого ранга — этот подкласс будет множеством. Это следует из двух простых фактов: того, что класс всех множеств определённого ранга образует множество, и того, что пересечение класса и множества — это множество. Такой подкласс (если он непуст) однозначно задаёт класс эквивалентности. В свою очередь если потребовать минимальность ранга, при котором подкласс будет непуст, то такой подкласс будет однозначно задаваться классом эквивалентности. В этом и состоит суть трюка Даны Скотта: замена полного класса эквивалентности его подмножеством, состоящим из элементов, имеющих минимальный ранг.

Более формально, введём обозначение для произвольного непустого класса ${\displaystyle B}$ обозначение: ${\displaystyle \operatorname {minrk} B=\min \limits _{b\in B}\operatorname {rk} b}$. Тогда

Такое определение удовлетворяет требованию, что каждому элементу факторкласса взаимно однозначно соответствует обычный класс эквивалентности.^[3]

---