Удаление квантификатора

Устранение кванторов — это концепция упрощения, используемая в математической логике , теории моделей и теоретической информатике . Неофициально, количественное утверждение» $\exists x$ такой, что $\ldots$можно рассматривать как вопрос «Когда будет $x$ такой, что $\ldots$?», и утверждение без кванторов можно рассматривать как ответ на этот вопрос.

Одним из способов классификации формул является количество количественных оценок . Формулы с меньшей глубиной чередования кванторов считаются более простыми, а формулы без кванторов - наиболее простыми.Теория имеет элиминацию кванторов , если для каждой формулы $\alpha$, существует другая формула $\alpha _{QF}$ без кванторов, что эквивалентно ему ( по модулю этой теории).

Примеры

Пример из школьной математики гласит, что квадратный многочлен с одной переменной имеет действительный корень тогда и только тогда, когда его дискриминант неотрицательен:

$\exists x\in \mathbb {R} .(a\neq 0\wedge ax^{2}+bx+c=0)\ \ \Longleftrightarrow \ \ a\neq 0\wedge b^{2}-4ac\geq 0$

Здесь предложение в левой части включает в себя квантификатор $\exists x\in \mathbb {R}$, тогда как эквивалентное предложение справа этого не делает.

Примерами теорий, которые оказались разрешимыми с помощью исключения кванторов, являются арифметика Пресбургера , алгебраически замкнутые поля , вещественные замкнутые поля , безатомные булевы алгебры , термальные алгебры , плотные линейные порядки , абелевы группы , случайные графы , а также многие их комбинации, такие как булева алгебра с арифметикой Пресбургера и алгебры термов с очередями .

Кванторным элиминатором для теории действительных чисел как упорядоченной аддитивной группы является исключение Фурье – Моцкина ; для теории поля действительных чисел это теорема Тарского–Зейденберга .

Исключение кванторов также можно использовать, чтобы показать, что «объединение» разрешимых теорий приводит к новым разрешимым теориям (см. теорему Фефермана – Вота ).

Алгоритмы и разрешимость

Если теория допускает устранение кванторов, то можно ответить на конкретный вопрос: существует ли метод определения $\alpha _{QF}$ для каждого $\alpha$? Если такой метод существует, мы называем его алгоритмом исключения кванторов . Если такой алгоритм существует, то разрешимость теории сводится к определению истинности предложений, свободных от кванторов . Предложения без кванторов не имеют переменных, поэтому их достоверность в данной теории часто можно вычислить, что позволяет использовать алгоритмы исключения кванторов для определения достоверности предложений.

Связанные понятия

Различные теоретико-модельные идеи связаны с устранением кванторов, и существуют различные эквивалентные условия.

Любая теория первого порядка с исключением кванторов является модельно полной . И наоборот, модельно-полная теория, теория универсальных следствий которой обладает свойством амальгамации , имеет устранение кванторов.

Модели теории универсальных следствий теории $T$ являются подструктурами моделей $T$. Теория линейных порядков не допускает исключения кванторов. Однако теория ее универсальных следствий обладает свойством амальгамации.

Основные идеи

Чтобы конструктивно показать, что теория допускает устранение кванторов, достаточно показать, что мы можем исключить квантор существования, примененный к соединению литералов , то есть показать, что каждая формула вида:

$\exists x.\bigwedge _{i=1}^{n}L_{i}$

где каждый $L_{i}$ является литералом, эквивалентен формуле без кванторов. Действительно, предположим, что мы знаем, как исключить кванторы из конъюнкций литералов, тогда если $F$ является бескванторной формулой, мы можем записать ее в дизъюнктивной нормальной форме

$\bigvee _{j=1}^{m}\bigwedge _{i=1}^{n}L_{ij},$

и использовать тот факт, что

$\exists x.\bigvee _{j=1}^{m}\bigwedge _{i=1}^{n}L_{ij}$

эквивалентно

$\bigvee _{j=1}^{m}\exists x.\bigwedge _{i=1}^{n}L_{ij}.$

Наконец, чтобы устранить универсальный квантор

$\forall x.F$

где $F$ не имеет кванторов, мы преобразуем $\lnot F$ в дизъюнктивную нормальную форму и воспользуемся тем, что $\forall x.F$эквивалентно $\lnot \exists x.\lnot F.$

с

В ранней теории моделей исключение кванторов использовалось, чтобы продемонстрировать, что различные теории обладают такими свойствами, как разрешимость и полнота . Обычный метод заключался в том, чтобы сначала показать, что теория допускает исключение кванторов, а затем доказать разрешимость или полноту, рассматривая только формулы без кванторов. Этот метод можно использовать, чтобы показать, что арифметика Пресбургера разрешима.

Теории могут быть разрешимы, но не допускать исключения кванторов. Строго говоря, теория аддитивных натуральных чисел не допускала исключения кванторов, но она представляла собой расширение аддитивных натуральных чисел, разрешимость которых была показана. Всякий раз, когда теория разрешима и язык ее действительных формул счетен , можно расширить теорию счетным числом отношений , чтобы исключить квантор (например, можно ввести для каждой формулы теории символ отношения, который связывает свободные переменные формулы).

Пример: Nullstellensatz для алгебраически замкнутых полей и для дифференциально замкнутых полей .

См. также

• Цилиндрическое алгебраическое разложение
• Теория устранения
• Устранение союза

Ссылки

• Браун, Кристофер В. (31 июля 2002 г.). «Что такое устранение квантификатора» . Проверено 30 августа 2023 г.

• Купер, округ Колумбия (1972). Мельцер, Бернард ; Мичи, Дональд (ред.). «Доказательство теоремы в арифметике без умножения» (PDF) . Машинный интеллект . 7 . Эдинбург: Издательство Эдинбургского университета: 91–99 . Проверено 30 августа 2023 г.

• Эндертон, Герберт (2001). Математическое введение в логику (2-е изд.). Бостон, Массачусетс: Академическая пресса . ISBN  978-0-12-238452-3 .

• Фрид, Майкл Д.; Джарден, Моше (2008). Полевая арифметика . Результаты математики и ее пограничные области. 3-й эпизод. Том 11 (3-е исправленное изд.). Издательство Спрингер . ISBN  978-3-540-77269-9 . Збл   1145.12001 .

• Гредель, Эрих; Колайтис, Фокион Г .; Либкин Леонид ; Мартен, Маркс; Спенсер, Джоэл ; Варди, Моше Ю .; Венема, Иде; Вайнштейн, Скотт (2007). Теория конечных моделей и ее приложения . Тексты по теоретической информатике. Серия EATCS. Берлин: Springer-Verlag . ISBN  978-3-540-00428-8 . Збл   1133.03001 .

• Ходжес, Уилфрид (1993). Теория моделей . Энциклопедия математики и ее приложений. Том. 42. Издательство Кембриджского университета . дои : 10.1017/CBO9780511551574 . ISBN  9780521304429 .

• Кунчак, Виктор; Ринар, Мартин (2003). «Структурное подтипирование нерекурсивных типов разрешимо» (PDF) . 18-й ежегодный симпозиум IEEE по логике в информатике, 2003 г. Материалы . стр. 96–107. дои : 10.1109/LICS.2003.1210049 . ISBN  0-7695-1884-2 . S2CID   14182674 .

• Монк, Дж. Дональд (2012). Математическая логика (Тексты для выпускников по математике (37)) (перепечатка оригинального 1-го издания 1976 г. в мягкой обложке). Спрингер. ISBN  9781468494549 .

• Нипков, Тобиас (2010). «Устранение линейного квантификатора» (PDF) . Журнал автоматизированного рассуждения . 45 (2): 189–212. дои : 10.1007/s10817-010-9183-0 . S2CID   14279141 . Проверено 12 ноября 2022 г.

• Пресбургер, Мойжес (1929). «О полноте некоторой системы арифметики целых чисел, в которой единственным действием выступает сложение». Comptes Rendus du I congrès de Mathematiciens de Pays Slaves, Варшава : 92–101. . см. в Stansifer (1984) английский перевод

• Стэнсифер, Райан (сентябрь 1984 г.). Статья Пресбургера о целочисленной арифметике: замечания и перевод (PDF) (технический отчет). Том. ТР84-639. Итака, Нью-Йорк: Кафедра компьютерных наук Корнельского университета.

• Шмелев, Ванда (1955). «Элементарные свойства абелевых групп» . Фундамента Математика . 41 (2): 203–271. дои : 10.4064/fm-41-2-203-271 . МР   0072131 .

• Жаннерод, Николя; Трейнен, Ральф. Решение теории первого порядка алгебры деревьев признаков с обновлениями . Международная совместная конференция по автоматизированному рассуждению (IJCAR). дои : 10.1007/978-3-319-94205-6_29 .

• Штурм, Томас (2017). «Обзор некоторых методов устранения, принятия решений и выполнимости реальных кванторов и их применения» . Математика в информатике . 11 (3–4): 483–502. дои : 10.1007/s11786-017-0319-z . hdl : 11858/00-001M-0000-002C-A3B5-B .