Устранение квантификатора

Метод упрощения в математической логике

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

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

Примеры

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

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

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

Примерами теорий, разрешимость которых была доказана с помощью исключения кванторов, являются арифметика Пресбургера , ^{[2] [3] [4] [5] [6]} алгебраически замкнутые поля , действительные замкнутые поля , ^{[7] [8]} безатомные булевы алгебры , термальные алгебры , плотные линейные порядки , ^[7] абелевы группы , ^[9] случайные графы , а также многие их комбинации, такие как булева алгебра с арифметикой Пресбургера и термальные алгебры с очередями .

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

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

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

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

Связанные концепции

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

Каждая теория первого порядка с устранением кванторов является модельно полной . Наоборот, модельно-полная теория, чья теория универсальных последствий имеет свойство объединения , имеет устранение кванторов. ^[10]

Модели теории всеобщих следствий теории являются в точности подструктурами моделей . ^[10] Теория линейных порядков не имеет кванторного устранения. Однако теория ее всеобщих следствий обладает свойством объединения. ${\displaystyle T}$ ${\displaystyle T}$

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

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

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

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

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

и используйте тот факт, что

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

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

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

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

${\displaystyle \forall x.F}$

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

Связь с разрешимостью

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

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

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

Смотрите также

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

Примечания

1. Brown 2002.
2. Пресбургер 1929.
3. Mind: базовая арифметика Пресбургера — — не допускает исключения квантификаторов. Нипков (2010): «Арифметике Пресбургера необходим предикат делимости (или конгруэнтности) '|', чтобы разрешить исключение квантификаторов». ${\displaystyle \langle \mathbb {N} ,+,0,1\rangle }$
4. Грэдель и др. (2007, стр. 20) определяют арифметику Пресбургера как . Это расширение допускает исключение кванторов. ${\displaystyle \langle \mathbb {N} ,+,<,0,1,(\equiv _{k})_{k>0}\rangle {\text{ where }}x\equiv _{k}y{\text{ iff }}x=y(\mod {k})}$
5. Монк 2012, стр. 240.
6. Эндертон 2001, стр. 188.
7. Грэдель и др. 2007.
8. Фрид и Джарден 2008, стр. 171.
9. Шмелев 1955, стр. 229 описывает «метод устранения квантификации».
10. Ходжес 1993.

Ссылки

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

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

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

• Фрид, Майкл Д.; Джарден, Моше (2008). Полевая арифметика . Ergebnisse der Mathematik und ihrer Grenzgebiete. 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. Cambridge University Press . doi :10.1017/CBO9780511551574. ISBN 9780521304429.

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

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

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

• Пресбургер, Мойжес (1929). «Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, в welchem ​​die Additions als einzige Operation hervortritt». Comptes Rendus du I congrès de Mathématiciens de Pays Slaves, Варшава : 92–101., см. Stansifer (1984) для перевода на английский язык

• Stansifer, Ryan (сентябрь 1984 г.). Статья Presburger's Article on Integer Arithmetic: Remarks and Translation (PDF) (технический отчет). Том TR84-639. Итака, Нью-Йорк: Кафедра компьютерных наук, Корнелльский университет.

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

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

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