Теория моделей

Одна и та же формула «∀x∀y (x+y = y+x)» может быть истинной в целых числах и ложной в матрицах. Теория моделей изучает отношение между синтаксисом (формулами) и семантикой (структурами, где эти формулы истинны или ложны).

• Реляционные базы данных - это структуры первого порядка; SQL-запросы - формулы
• Алгебраические спецификации в формальной разработке ПО
• Верификация аппаратуры: схема - структура, спецификация - формула

Структуры и интерпретации

Структура (или реализация) для сигнатуры σ - это пара M = (M, I), где M - непустое множество (носитель), а I - интерпретация: каждому функциональному символу f/k ставится в соответствие функция I(f): M^k → M, а каждому предикатному символу R/k - отношение I(R) ⊆ M^k.

Гомоморфизм и элементарное вложение

Гомоморфизм между структурами - это отображение, сохраняющее интерпретацию символов. Изоморфизм - биективный гомоморфизм с биективным обратным. Элементарное вложение - гомоморфизм, сохраняющий истинность всех формул первого порядка.

Элементарная эквивалентность

Две структуры элементарно эквивалентны (M ≡ N), если в них истинны одни и те же замкнутые формулы первого порядка. Это более слабое понятие, чем изоморфизм: неизоморфные структуры могут быть элементарно эквивалентны.

Игры Эренфойхта-Фраïссе дают комбинаторный критерий для проверки элементарной эквивалентности. Игрок I пытается «различить» структуры, выбирая элементы; игрок II пытается «синхронизировать» выборы. Если II выигрывает все n-ходовые игры - структуры удовлетворяют одним и тем же формулам кванторной глубины ≤ n.

Ультрапроизведения

Ультрапроизведение - мощный инструмент для построения новых структур из семейства структур. Фундаментальное свойство: теорема Лоша утверждает, что формула истинна в ультрапроизведении тогда и только тогда, когда она истинна «почти везде» (на ультрафильтре).

Нестандартный анализ Робинсона реализовал мечту Лейбница: сделать бесконечно малые строго обоснованными. Гиперреальные числа *ℝ содержат ε с 0 < ε < 1/n для всех натуральных n. Производная определяется как стандартная часть: f'(x) = st((f(x+ε) - f(x))/ε).

Теория моделей: ключевые идеи

• Структура = носитель + интерпретация символов; формула истинна или ложна в структуре
• Элементарное вложение M ≺ N: сохраняет истинность всех первопорядковых формул
• Элементарная эквивалентность M ≡ N: одни и те же замкнутые формулы истинны (слабее изоморфизма)
• Ультрапроизведение: теорема Лоша - формула истинна в ΠMᵢ/U ⟺ истинна «почти везде»
• Нестандартный анализ: ультрапроизведение реализует бесконечно малые строго

К теории множеств

Теория моделей работает внутри теории множеств ZFC - она изучает структуры как множества. Следующий урок посвящён самой ZFC: какова её собственная аксиоматика и что из неё следует.

• ml-08 — Related lesson

Вопросы для размышления

• Если ℚ ≡ ℝ как упорядоченные поля (в первом порядке), то как теорема о полноте ℝ (всякая ограниченная последовательность имеет предел) соотносится с этим фактом?
• Нестандартный анализ строго обосновывает бесконечно малые. Почему тогда стандартный анализ (ε-δ определения) используется повсеместно?
• Как игры Эренфойхта-Фраïссе позволяют доказывать, что формулу нельзя выразить в первом порядке?

Связанные уроки

• plt-02-type-systems