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

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

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

Примеры

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

{ 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}}$ , в то время как эквивалентное предложение справа - нет.

Примеры теорий, которые оказались разрешимыми с использованием исключения кванторов: Арифметика пресбургера,^[2] алгебраически замкнутые поля, настоящие закрытые поля,^[2]^[3] безатомный Булевы алгебры, термальные алгебры, плотные линейные порядки,^[2] абелевы группы,^[4] случайные графы, а также многие их комбинации, такие как булева алгебра с арифметикой Пресбургера и термальные алгебры с очереди.

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

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

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

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

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

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

Любая теория первого порядка с исключением квантора модель завершена. И наоборот, модельно-полная теория, теория универсальных следствий которой имеет имущество слияния, имеет исключение квантора.^[5]

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

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

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

{ 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 x.F}

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

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

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

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

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

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

Примечания

^ ^а ^б Браун, Кристофер В. (31 июля 2002 г.). «Что такое исключение квантификатора». Получено 30 августа, 2018.
^ ^а ^б ^c ^d Грэдель, Эрих; Колайтис, 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: 203–271. МИСТЕР 0072131.
^ ^а ^б Ходжес, Уилфрид (1993). Теория моделей. Издательство Кембриджского университета