Теория моделей — раздел математической логики, изучающий связь между формальными языками (синтаксис) и их интерпретациями (семантика). Основана Альфредом Тарским в 1930-х годах. Теория моделей отвечает на вопросы: какие структуры удовлетворяют данным аксиомам? Можно ли отличить структуры с помощью формул логики первого порядка? Какие свойства сохраняются при переходе между моделями?
Представьте геометрию Евклида: аксиомы — это правила игры (через две точки проходит прямая, параллельные не пересекаются). Модель — конкретная реализация: плоскость, сфера, гиперболическая поверхность. Теория моделей изучает, какие утверждения истинны во всех моделях (теоремы геометрии), а какие зависят от выбора модели (5-й постулат Евклида).
Основные понятия
Сигнатура σ — набор символов: констант (0, 1), функций (+, ×), отношений (<, =). Определяет "алфавит" теории. Например, сигнатура групп: {∘, e, ⁻¹} (операция, единица, обратный элемент).
Структура (модель) M = (M, σᴹ) — непустое множество M (носитель) с интерпретацией символов сигнатуры. Для групп: M — множество элементов, ∘ᴹ — конкретная операция (умножение матриц, сложение чисел), eᴹ — единица.
Удовлетворяет (⊨): Структура M удовлетворяет формуле φ, если φ истинна в M при интерпретации символов. M ⊨ φ читается "M — модель φ".
Теория T — множество формул (обычно аксиом). Модель теории — структура, удовлетворяющая всем аксиомам T. Например, теория групп: аксиомы ассоциативности, единицы, обратного элемента.
Элементарная эквивалентность
Структуры M и N элементарно эквивалентны (M ≡ N), если удовлетворяют одним и тем же предложениям логики первого порядка. Это не означает изоморфизм: (ℚ, <) ≡ (ℝ, <) (рациональные и вещественные числа неразличимы формулами первого порядка), но не изоморфны (ℚ счётно, ℝ несчётно).
Теорема Лёвенхейма-Сколема (1915-1920): Если теория T имеет бесконечную модель, у неё есть счётная модель. Следствие: вещественные числа (несчётные) имеют счётную модель, неотличимую от ℝ формулами первого порядка. Это показывает ограниченность логики первого порядка.
Компактность
Теорема компактности (Гёдель, 1930; Мальцев, 1936): Теория T имеет модель тогда и только тогда, когда любое конечное подмножество T имеет модель. Эквивалентно: если из T выводится противоречие, оно выводится из конечного числа аксиом.
Применение: Нестандартный анализ (Робинсон, 1966). Добавляем к аксиомам вещественных чисел бесконечно малое ε: ε > 0, ε < 1/n для всех натуральных n. Любое конечное подмножество аксиом выполнимо (берём достаточно малое ε), значит, по компактности существует модель с бесконечно малыми — гипердействительные числа *ℝ.
Ультрапроизведения
Ультрапроизведение — конструкция новой модели из семейства моделей через ультрафильтр. Позволяет строить нестандартные модели и доказывать элементарную эквивалентность.
Теорема Лося (1955): Формула истинна в ультрапроизведении тогда и только тогда, когда она истинна в "большинстве" исходных моделей (согласно ультрафильтру). Используется для переноса свойств между моделями.
Категоричность
Теория T категорична в мощности κ, если все модели мощности κ изоморфны. Означает: теория однозначно описывает структуру заданного размера.
Примеры:
- Теория плотных линейных порядков без концов категорична в счётной мощности (единственная модель — рациональные числа ℚ).
- Теория алгебраически замкнутых полей характеристики 0 категорична в несчётных мощностях (все модели мощности континуум изоморфны ℂ).
Теорема Морли (1965): Если теория категорична в одной несчётной мощности, она категорична во всех несчётных мощностях. Неожиданный результат, связывающий категоричность с алгебраическими свойствами.
Полнота и разрешимость
Теория T полна, если для любого предложения φ либо T ⊢ φ, либо T ⊢ ¬φ (не существует "неопределённых" утверждений). Эквивалентно: все модели элементарно эквивалентны.
Примеры полных теорий:
- Теория вещественно замкнутых полей (Тарский, 1948) — описывает вещественные числа. Разрешима: существует алгоритм проверки истинности любого утверждения о ℝ (например, ∃x(x⁵ - 3x + 1 = 0)).
- Теория плотных линейных порядков без концов — полна и разрешима.
Неполные теории: Арифметика Пеано (PA) неполна (теорема Гёделя, 1931): существуют истинные, но недоказуемые утверждения о натуральных числах.
Квантификация кванторов
Теория моделей классифицирует формулы по чередованию кванторов:
- Экзистенциальные (∃-формулы): ∃x₁...∃xₙ φ, где φ бескванторная. Сохраняются при вложениях.
- Универсальные (∀-формулы): ∀x₁...∀xₙ φ. Сохраняются при расширениях.
- Формулы типа ∀∃, ∃∀, ∀∃∀... — иерархия сложности.
Теорема об элиминации кванторов: В некоторых теориях любая формула эквивалентна бескванторной. Например, в теории плотных линейных порядков ∃y(x < y < z) эквивалентно x < z. Элиминация кванторов — мощный инструмент упрощения.
Применение в алгебре
Теория моделей изучает алгебраические структуры через логические свойства. Например, поле алгебраически замкнуто (любой многочлен имеет корень) выражается формулой: ∀a₀...∀aₙ ∃x(aₙx^n + ... + a₁x + a₀ = 0).
Аксиома выбора и теория моделей: Компактность эквивалентна аксиоме выбора (для языков с бесконечными сигнатурами). Многие результаты (теорема Лёвенхейма-Сколема, существование ультрафильтров) используют аксиому выбора.
Применение в computer science
Верификация программ: Программа — модель спецификации (формальных требований). Проверка корректности — доказательство M ⊨ φ для всех состояний M.
Базы данных: Реляционная база — конечная модель, SQL-запрос — формула логики первого порядка. Оптимизация запросов использует эквивалентность формул.
SAT-решатели: Проверка выполнимости формулы — поиск модели. SMT (Satisfiability Modulo Theories) расширяет SAT теориями (арифметика, массивы) — прикладная теория моделей.
Современные направления
Дескриптивная теория множеств: Связь теории моделей с топологией и дескриптивными свойствами множеств. Изучает борелевские и проективные множества через логику.
O-минимальность: Класс структур, где определимые множества на прямой конечны или коконечны. Включает вещественно замкнутые поля, используется в теории дифференциальных уравнений.
Стабильность: Классификация теорий по сложности типов (Шелах, 1970-е). Стабильные теории имеют хорошие свойства (например, категоричны в несчётных мощностях при условиях). Программа Шелаха — грандиозная классификация всех теорий первого порядка.