Исключение кванторов - это концепция упрощения, используемая в математической логике , теории моделей и теоретической информатике . Неофициально, количественное заявление " такой, что "можно рассматривать как вопрос" Когда есть такой, что ? ", и утверждение без кванторов можно рассматривать как ответ на этот вопрос. [1]
Один из способов классификации формул - количественная оценка . Формулы с меньшей глубиной чередования кванторов считаются более простыми, а формулы без кванторов - самыми простыми. У теории есть исключение квантора, если для каждой формулы, существует другая формула без эквивалентных кванторов ( по модулю этой теории).
Примеры
Пример из математики средней школы гласит, что квадратичный многочлен с одной переменной имеет действительный корень тогда и только тогда, когда его дискриминант неотрицателен: [1]
Здесь предложение в левой части включает квантификатор , а эквивалентное предложение справа - нет.
Примеры теорий, которые были показаны разрешимыми с использованием исключения кванторов, включают арифметику Пресбургера , [2] алгебраически замкнутые поля , вещественные замкнутые поля , [2] [3] безатомные булевы алгебры , термальные алгебры , плотные линейные порядки , [2] абелевы группы , [ 2] 4] случайные графы , а также многие их комбинации, такие как булева алгебра с арифметикой Пресбургера и термальные алгебры с очередями .
Средство исключения кванторов для теории действительных чисел как упорядоченной аддитивной группы - это исключение Фурье – Моцкина ; для теории поля действительных чисел это теорема Тарского – Зайденберга . [2]
Исключение квантора может также использоваться, чтобы показать, что «комбинирование» разрешимых теорий приводит к новым разрешимым теориям.
Алгоритмы и разрешимость
Если в теории существует исключение кванторов, можно задать конкретный вопрос: существует ли метод определения для каждого ? Если такой метод существует, мы называем его алгоритмом исключения квантора . Если такой алгоритм существует, то разрешимость теории сводится к определению истинности бескванторных предложений . Предложения без кванторов не имеют переменных, поэтому их достоверность в данной теории часто можно вычислить, что позволяет использовать алгоритмы исключения кванторов для определения действительности предложений.
Связанные понятия
Различные теоретико-модельные идеи связаны с исключением квантора, и существуют различные эквивалентные условия.
Каждая теория первого порядка с исключением квантора является завершенной моделью . И наоборот, теория полной модели, чья теория универсальных следствий обладает свойством объединения , имеет исключение кванторов. [5]
Модели теории универсальных следствий теории являются именно подструктурами моделей. [5] Теория линейных порядков не имеет исключения кванторов. Однако теория его универсальных следствий обладает свойством слияния.
Основные идеи
Чтобы конструктивно показать, что в теории существует исключение квантора, достаточно показать, что мы можем исключить квантор существования, применяемый к конъюнкции литералов , то есть показать, что каждая формула вида:
где каждый является литералом, эквивалентен бескванторной формуле. В самом деле, предположим, что мы знаем, как исключить кванторы из конъюнкций литералов, тогда, еслибескванторная формула, мы можем записать ее в дизъюнктивной нормальной форме
и использовать тот факт, что
эквивалентно
Наконец, чтобы исключить универсальный квантор
где бескванторный, мы преобразуем в дизъюнктивную нормальную форму и используйте тот факт, что эквивалентно
Связь с разрешимостью
В ранней теории моделей метод исключения кванторов использовался для демонстрации того, что различные теории обладают такими свойствами, как разрешимость и полнота . Обычной техникой было сначала показать, что теория допускает исключение кванторов, а затем доказать разрешимость или полноту, рассматривая только бескванторные формулы. Этот метод можно использовать, чтобы показать, что арифметика Пресбургера разрешима.
Теории могут быть разрешимыми, но не допускать исключения кванторов. Строго говоря, теория аддитивных натуральных чисел не допускала исключения кванторов, но была показана разрешимость разложения аддитивных натуральных чисел. Всякий раз, когда теория разрешима и язык ее действительных формул счетный , можно расширить теорию с помощью счетного числа отношений, чтобы исключить квантор (например, можно ввести для каждой формулы теории символ отношения, который связывает свободные переменные формулы). [ необходима цитата ]
Пример: Nullstellensatz для алгебраически замкнутых полей и для дифференциально замкнутых полей . [ требуется разъяснение ]
Смотрите также
- Цилиндрическое алгебраическое разложение
- Теория исключения
- Устранение конъюнкции
Заметки
- ^ a b Браун, Кристофер В. (31 июля 2002 г.). «Что такое исключение квантификатора» . Проверено 30 августа 2018 года .
- ^ а б в г Грэдель, Эрих; Колайтис, Phokion G .; Либкин, Леонид ; Маартен, Маркс; Спенсер, Джоэл ; Варди, Моше Ю .; Венема, Иде; Вайнштейн, Скотт (2007). Теория конечных моделей и ее приложения . Тексты по теоретической информатике. Серия EATCS. Берлин: Springer-Verlag . ISBN 978-3-540-00428-8. Zbl 1133.03001 .
- ^ Фрид, Майкл Д .; Джарден, Моше (2008). Полевая арифметика . Ergebnisse der Mathematik und ihrer Grenzgebiete. 3. Фольге. 11 (3-е изд. Изм.). Springer-Verlag . п. 171. ISBN. 978-3-540-77269-9. Zbl 1145.12001 .
- ^ Шмелев В. (1955). «Элементарные свойства абелевых групп» . Fundamenta Mathematicae . 41 (2): 203–271. DOI : 10,4064 / фм-41-2-203-271 . Руководство по ремонту 0072131 .
- ^ a b Ходжес, Уилфрид (1993). Теория моделей. Издательство Кембриджского университета
Рекомендации
- Виктор Кунчак и Мартин Ринард. « Структурное подтипирование нерекурсивных типов разрешимо ». На восемнадцатом ежегодном симпозиуме IEEE по логике в компьютерных науках, 2003 г.