Разрешающая процедура для теории вещественно замкнутых полей. Семинар 1

Элементарные теории (чей язык содержит только кванторы по элементам носителя) — ключевой объект изучения в математической логике. Многие известные результаты связаны с изучением алгоритмических свойств элементарных теорий различных классов структур — графов, решёток, групп, колец и т.п. — и их фрагментов. Пожалуй, наиболее известным «положительным» результатом в этой области является теорема Тарского–Зайденберга о разрешимости теории упорядоченного поля вещественных чисел, совпадающей с теорией вещественно замкнутых полей: существует алгоритм, который по произвольному предложению в языке упорядоченных полей определяет, истинно ли оно над вещественными числами. В качестве простого следствия отсюда получается разрешимость теории поля комплексных чисел, совпадающей с теорией алгебраически замкнутых полей, а также разрешимость элементарной геометрии (на вещественной плоскости), где язык содержит трёхместный предикат «$x$ лежит на прямой $uv$ между $u$ и $v$» и четырёхместный предикат «расстояние между $x$ и $y$ равно расстоянию между $u$ и $v$». Кроме того, отсюда же получается решение известной «Семнадцатой проблемы Гильберта», связанной с представимостью неотрицательных рациональных функций в виде сумм квадратов рациональных функций. С другой стороны, с помощью первой теоремы Гёделя о неполноте можно показать неразрешимость теорий колец и полей.

Цель данного мини-курса — познакомить слушателей с доказательством теоремы Тарского–Зайденберга и её основными приложениями, а также рассказать о контрастирующих с ней «негативных» результатах, связанных с кольцами и полями.

Предварительный план
1. Метод элиминации кванторов — основной метод доказательства разрешимости элементарных теорий.
2-3. Разрешимость теории поля вещественных чисел, теорий поля комплексных чисел и элементарной геометрии.
4. Семнадцатая проблема Гильберта и её обобщение на произвольные вещественно замкнутые поля. Результаты о неразрешимости, связанные с кольцами и полями.