Типы и насыщенные модели

Мотивация: «портрет» элемента в модели

Тип элемента — это совокупность всех свойств, которыми обладает данный элемент в данной теории. Две модели могут иметь разные типы элементов. «Насыщенная» модель «содержит» все возможные типы — она максимально богата. Теория типов — ключ к пониманию, когда модели изоморфны, и к построению «канонических» моделей теории.

Типы

Частичный n-тип (над пустым множеством параметров): Множество формул p(x₁,...,xₙ) такое, что p ∪ T выполнимо (т.е. в некоторой модели T существуют элементы, удовлетворяющие всем φ ∈ p).

Полный n-тип: Для каждой формулы φ(x₁,...,xₙ): либо φ ∈ p, либо ¬φ ∈ p. Максимально информативный тип.

Реализация типа: Элементы (a₁,...,aₙ) ∈ Mⁿ реализуют тип p, если M ⊨ φ(a₁,...,aₙ) для всех φ ∈ p.

Пространство типов Sₙ(T): Множество всех полных n-типов T. Топология Стоуна: [φ] = {p ∈ Sₙ(T) : φ ∈ p} — базисные открытые множества. Это компактное топологическое пространство.

Насыщенные модели

κ-насыщенная модель M: Для каждого A ⊆ M, |A| < κ, и каждого типа p(x) над A (выполнимого в расширении M): M реализует p.

Полностью насыщенная: M — κ-насыщена при κ = |M|.

Теорема: Две насыщенные модели одной мощности одной и той же полной теории изоморфны. Насыщенные модели — «канонические» представители теории.

ω-категоричность

T — ω-категорична: T имеет единственную (с точностью до изоморфизма) счётную модель.

Теорема Рылл-Нарджевского (1959): T — ω-категорична ⟺ Sₙ(T) конечно для каждого n.

Примеры: Th(ℚ,<) — ω-категорична (DLO); Th(∞-атомарной булевой алгебры) — ω-категорична; Th(ℤ,+) — не ω-категорична.

Численный пример

Задача: Описать полные 1-типы в теории DLO (Th(ℚ,<)).

Шаг 1. DLO — полная теория. Полные 1-типы p(x) — полные множества формул φ(x) ∈ Th(ℚ,<) ∪ {φ(x)}.

Шаг 2. Над пустым множеством параметров: единственная полная 1-теория DLO описывает «элемент в плотном линейном порядке без концов». Nет дополнительных параметров → все элементы ℚ имеют одинаковый тип (DLO ω-категорична → один 1-тип) ✓.

Шаг 3. Полные 2-типы p(x,y) над пустым множеством: три возможности (x < y), (x = y), (x > y). Каждая из них определяет полный 2-тип (в DLO формула x < y, x = y или y < x полностью «завершима» до полного типа, так как никаких других параметров нет). Итого: 3 полных 2-типа ✓.

Шаг 4. Проверка Рылл-Нарджевского: |S₁(DLO)| = 1 (конечно), |S₂(DLO)| = 3 (конечно), |S₃(DLO)| = ... порядки трёх элементов: 3! = 6 линейных порядков, плюс совпадения → в DLO всегда один из 3!/все перестановки = 6 линейных порядков... нет, совпадения тоже возможны (a=b < c, a < b = c и т.д.). Конечное число ✓ → DLO ω-категорична ✓.

Реальное приложение

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

Дополнительные аспекты

Тип частичный (partial type) элемента a в модели M над множеством параметров A — это согласованное множество формул p(x) такое, что для подходящего a' в элементарном расширении p(a') истинно. Полный тип содержит для каждой формулы либо её, либо отрицание. Пространство типов S(A) — компактное пространство Стоуна; топологическая структура связана со свойствами теории (стабильность, сатурированность). Сатурированная модель реализует все типы малой мощности; такие модели почти не зависят от выбора и служат «универсальными контейнерами». На стыке теории моделей и алгебры из сатурированности вытекают теоремы о квантификации устранимости (квантор-eliminable теории — алгебраически замкнутые поля характеристики 0, вещественно замкнутые поля; теорема Тарского) — основа автоматизированной геометрии и систем компьютерной алгебры.

Связь с другими разделами математики

Понятие типа и насыщенной модели органично связывается с алгеброй через работы Черхи-МакЛейна, Робинсона и Лося по элементарным классам алгебраических структур. В теории полей описание типов над подполем соответствует классификации корней многочленов и расширений: в алгебраически замкнутых полях типы одномерных элементов над подполем кодируют минимальные многочлены и расположение корней; насыщенные модели таких теорий совпадают с «достаточно большими» универсальными полями, используемыми в диофантовой геометрии (Ланг, Делинь).

В дифференциальных уравнениях насыщенные модели лежат в основе понятий дифференциально замкнутого поля Колчина и теории Морли о категоричности: типы описывают решения дифференциальных уравнений с параметрами, а насыщенные модели играют роль «общего решения», содержащего все формально возможные ветви. В неархимедовой аналитике (Робинсон, Лакс) насыщенные расширения действительных чисел обеспечивают существование гиперреальных чисел и позволяют формализовать методы, напоминающие численные схемы с бесконечно малыми шагами.

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

Историческая справка и развитие идеи

Зачатки понятий типа и насыщения появляются в работах Тарского 1940-х годов по элементарной теории полей, но современный язык сформировался в 1950–1960-х. Стоун в 1936 году вводит компактные пространства, ныне называемые пространствами Стоуна, что позже оказалось естественной топологической оболочкой для множеств типов. Абрахам Робинсон в книге «Model Theory and the Theory of Fields» (1959) систематизирует сверхструктуры и насыщенные расширения, развивая идеи Лосевой теоремы об ультрапроизведениях. Формальное определение типов и насыщенных моделей в привычной форме связано с школой Тарского–Кейслина и особенно с Морли и Шелахом. Морли в статье 1965 года в Journal of Symbolic Logic доказывает теорему о категоричности в несчетных мощностях, где насыщенные модели играют центральную роль. Шелах в монументальной серии «Classification Theory» (начиная с 1970-х) развивает аппарат стабильности, рангов и насыщения, превращая работу с типами в основной инструмент классификации теорий.