Введение
Метод упрощения в математической логике. Устранение кванторов — это концепция упрощения, используемая в математической логике, теории моделей и теоретической информатике. Неформально, квантифицированное утверждение "существует такое, что" можно рассматривать как вопрос "При каких условиях существует такое, что ?", а утверждение без кванторов можно рассматривать как ответ на этот вопрос. Один из способов классификации формул — по степени квантификации. Формулы с меньшей глубиной чередования кванторов считаются более простыми, а формулы без кванторов — самыми простыми. Теория обладает свойством устранения кванторов, если для каждой формулы φ существует другая формула ψ без кванторов, эквивалентная ей (в рамках данной теории).
Quantifier elimination is a concept of simplification used in mathematical logic, model theory, and theoretical computer science. Informally, a quantified statement " such that " can be viewed as a question "When is there an such that ? ", and the statement without quantifiers can be viewed as the answer to that question. One way of classifying formulas is by the amount of quantification. Formulas with less depth of quantifier alternation are thought of as being simpler, with the quantifier free formulas as the simplest. A theory has quantifier elimination if for every formula , there exists another formula without quantifiers that is equivalent to it (modulo this theory).
Алгоритмы и решаемость
Если теория обладает устранением кванторов, то можно задать конкретный вопрос: существует ли метод определения для каждого ? Если такой метод существует, мы называем его алгоритмом устранения кванторов. Если такой алгоритм существует, то задача определения исполнимости теории сводится к определению истинности кванторно-свободных формул. Кванторно-свободные формулы не содержат переменных, поэтому их истинность в данной теории часто можно вычислить, что позволяет использовать алгоритмы устранения кванторов для определения истинности формул.
Связанные понятия
Различные идеи модели-теоретического характера связаны с устранением кванторов, и существует множество эквивалентных условий. Любая теория первого порядка с устранением кванторов является модель-полной. И наоборот, модель-полная теория, теория универсальных следствий которой обладает свойством амильгамации, имеет устранение кванторов. Модели теории универсальных следствий теории являются как раз подструктурами моделей исходной теории. Теория линейных порядков не имеет устранения кванторов. Однако теория ее универсальных следствий обладает свойством амильгамации.
Связь с решаемостью
В ранней теории моделей устранение кванторов использовалось для демонстрации того, что различные теории обладают свойствами, такими как разрешимость и полнота. Распространенной техникой было сначала показать, что теория допускает устранение кванторов, а затем доказать разрешимость или полноту, рассматривая только формулы без кванторов. Этот метод можно использовать для доказательства разрешимости арифметики Пресбургера. Теории могут быть разрешимыми, но не допускать устранения кванторов. Строго говоря, теория аддитивных натуральных чисел не допускала устранения кванторов, но было показано, что расширение аддитивных натуральных чисел является разрешимым. Если теория разрешима, а язык ее валидных формул счетен, то можно расширить теорию счетным числом отношений, чтобы добиться устранения кванторов (например, для каждой формулы теории можно ввести символ отношения, связывающий свободные переменные этой формулы). Пример: теорема Нульштейна для алгебраически замкнутых полей и для дифференциально замкнутых полей.