Оглавление
Устранение квантификатора
-
Исключение квантификатора
- Концепция упрощения в математической логике, теории моделей и теоретической информатике
- Формула без квантификаторов эквивалентна утверждению без квантификаторов
-
Классификация формул
- Формулы с меньшей глубиной чередования кванторов считаются более простыми
- Формулы без кванторов считаются самыми простыми
-
Примеры теорий
- Арифметика Пресбургера, алгебраически замкнутые поля, вещественные замкнутые поля, безатомные булевы алгебры, терм-алгебры, плотные линейные порядки, абелевы группы, случайные графы
-
Алгоритмы и разрешимость
- Если теория допускает исключение квантификатора, существует алгоритм устранения квантификатора
- Разрешимость теории сводится к определению истинности предложений без кванторов
-
Связанные понятия
- Каждая теория первого порядка с исключением квантификатора является завершенной моделью
- Теория, полная моделей, теория универсальных следствий которой обладает свойством объединения, исключает квантификатор
-
Основные идеи
- Чтобы показать, что теория допускает исключение квантора, достаточно исключить экзистенциальный квантор из соединений литералов
- Универсальный квантификатор исключается аналогично
-
Связь с разрешимостью
- Исключение кванторов использовалось для демонстрации разрешимости и полноты теорий
- Теория аддитивных натуральных чисел не допускает исключения квантора, но является разрешимой
-
Примеры теорий
- Nullstellensatz для алгебраически замкнутых и дифференциально замкнутых полей