Математическая логика

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

Теорема Лёвенгейма-Сколема: теория с бесконечной моделью имеет счётную модель, включая теорию вещественных чисел. Это кажется парадоксом (R несчётно), но показывает фундаментальное ограничение логики первого порядка - нельзя 'захватить' несчётность в первопорядковых аксиомах.

Нестандартный анализ Робинсона: бесконечно малые Лейбница строго обоснованы теоремой компактности - они существуют в нестандартных моделях R
Базы данных: теория конечных структур и SQL-запросов использует методы теории моделей для анализа выразительности запросов
SAT-солверы: алгоритмы проверки выполнимости (DPLL, CDCL) реализуют теорему компактности для пропозициональных формул в конъюнктивной нормальной форме
SMT-солверы (Z3, CVC5): решают теории (линейная арифметика, теория массивов) используя процедуры проверки выполнимости фрагментов первого порядка

Структуры, модели и теорема компактности

Теория моделей изучает отношение между формальными теориями и их интерпретациями. Абрахам Робинсон в 1961 году использовал теорему компактности для обоснования нестандартного анализа - полей с настоящими бесконечно малыми. Теорема Лёвенгейма-Сколема обнаруживает парадоксальное следствие: теория вещественных чисел имеет счётную модель.

Что утверждает теорема компактности в теории моделей?

Теорема компактности: T имеет модель тогда и только тогда, когда каждое конечное подмножество T имеет модель. Следствие: нестандартный анализ Робинсона, нестандартные модели PA.

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

Две структуры элементарно эквивалентны, если в них выполнены одни и те же предложения первого порядка. Теория называется полной, если каждое предложение либо доказуемо, либо опровержимо. Теория Th(N, +, x) (истинная арифметика) полна, но не рекурсивно аксиоматизируема - она слишком богата для компьютерной проверки.

Теория плотных линейных порядков без концов (DLO) - полная и рекурсивно аксиоматизированная теория. Теория вещественно замкнутых полей (RCF) тоже полна - следствие теоремы Тарского об устранении кванторов. Это объясняет, почему компьютеры могут решать некоторые геометрические задачи.

Что означает, что теория первого порядка является полной?

Полная теория T: для каждого замкнутого предложения phi либо T |- phi, либо T |- neg phi. По теореме Гёделя, PA неполна: существует G, независимое от PA.

Итоги

Структура = (носитель, интерпретации предикатов, функций, констант) - конкретная математическая интерпретация теории
Теорема компактности: T выполнима тогда и только тогда, когда каждое конечное подмножество T выполнимо
Нисходящая теорема Лёвенгейма-Сколема: консистентная счётная теория первого порядка имеет счётную модель
Нестандартный анализ: PA + {c > n | n in N} выполнима по компактности, порождая нестандартные модели с бесконечно большими элементами
Элементарная эквивалентность: M equiv N, если они выполняют одни предложения первого порядка (изоморфизм влечёт, обратное неверно)
Теория RCF полна (устранение кванторов по Тарскому): вещественная алгебра алгоритмически разрешима

Структуры, модели и теорема компактности

Что утверждает теорема компактности в теории моделей?

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

Что означает, что теория первого порядка является полной?

Итоги

Структура = (носитель, интерпретации предикатов, функций, констант) - конкретная математическая интерпретация теории

Теорема компактности: T выполнима тогда и только тогда, когда каждое конечное подмножество T выполнимо

Нисходящая теорема Лёвенгейма-Сколема: консистентная счётная теория первого порядка имеет счётную модель

Нестандартный анализ: PA + {c > n | n in N} выполнима по компактности, порождая нестандартные модели с бесконечно большими элементами

Элементарная эквивалентность: M equiv N, если они выполняют одни предложения первого порядка (изоморфизм влечёт, обратное неверно)

Теория RCF полна (устранение кванторов по Тарскому): вещественная алгебра алгоритмически разрешима