Исключение квантора - Quantifier elimination

Исключение кванторов - это концепция упрощения, используемая в математической логике , теории моделей и теоретической информатике . Неформально, количественное утверждение « такое, что » можно рассматривать как вопрос «Когда есть такое, что ?», А утверждение без кванторов можно рассматривать как ответ на этот вопрос. ${\ Displaystyle \ существует х}$${\ displaystyle \ ldots}$${\ displaystyle x}$${\ displaystyle \ ldots}$

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

Примеры

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

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

Здесь предложение в левой части включает квантификатор , а в эквивалентном предложении справа - нет. ${\ Displaystyle \ существует х \ в \ mathbb {R}}$

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

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

Исключение квантора может также использоваться, чтобы показать, что «комбинирование» разрешимых теорий приводит к новым разрешимым теориям.

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

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

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

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

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

Модели теории универсальных следствий теории - это в точности подструктуры моделей . В теории линейных порядков нет исключения кванторов. Однако теория его универсальных следствий обладает свойством слияния. ${\ displaystyle T}$${\ displaystyle T}$

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

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

${\ displaystyle \ существует x. \ bigwedge _ {i = 1} ^ {n} L_ {i}}$

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

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

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

${\ displaystyle \ существует 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 xF}$

где бескванторный, мы преобразуем его в дизъюнктивную нормальную форму и используем тот факт, который эквивалентен${\ displaystyle F}$${\ Displaystyle \ lnot F}$${\ displaystyle \ forall xF}$${\ Displaystyle \ lnot \ существует х. \ lnot F.}$

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

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

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

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

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

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

Заметки

Рекомендации

• Виктор Кунчак и Мартин Ринард. « Структурное подтипирование нерекурсивных типов разрешимо ». На восемнадцатом ежегодном симпозиуме IEEE по логике в компьютерных науках, 2003 г.