Jump to content

Удаление квантификатора

(Перенаправлено с Устранение кванторов )

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

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

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

Здесь предложение в левой части включает в себя квантификатор , тогда как эквивалентное предложение справа этого не делает.

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

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

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

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

[ редактировать ]

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

[ редактировать ]

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

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

Модели теории универсальных следствий теории являются подструктурами моделей . [10] Теория линейных порядков не допускает исключения кванторов. Однако теория ее универсальных следствий обладает свойством амальгамации.

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

[ редактировать ]

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

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

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

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

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

где не имеет кванторов, мы преобразуем в дизъюнктивную нормальную форму и воспользуемся тем, что эквивалентно

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

[ редактировать ]

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

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

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

См. также

[ редактировать ]

Примечания

[ редактировать ]
  1. ^ Jump up to: Перейти обратно: а б Браун 2002 .
  2. ^ Пресбургер 1929 .
  3. ^ Разум: базовая арифметика Пресбургера - — не допускает исключения квантора. Нипков (2010) : «Арифметика Пресбургера нуждается в предикате делимости (или конгруэнтности) '|' чтобы разрешить устранение квантора».
  4. ^ Гредель и др. (2007 , стр. 20) определяют арифметику Пресбургера как . Это расширение допускает исключение кванторов.
  5. ^ Монк 2012 , с. 240.
  6. ^ Эндертон 2001 , с. 188.
  7. ^ Jump up to: Перейти обратно: а б с Grädel et al. 2007Гредель и др. 2007
  8. ^ Фрид и Джарден 2008 , с. 171.
  9. ^ Szmielew 1955 , стр. 229 описывает «метод устранения количественной оценки»..
  10. ^ Jump up to: Перейти обратно: а б Ходжес 1993 .
  • Браун, Кристофер В. (31 июля 2002 г.). «Что такое устранение квантификатора» . Проверено 30 августа 2023 г.
  • Монк, Дж. Дональд (2012). Математическая логика (Тексты для выпускников по математике (37)) (перепечатка оригинального 1-го издания 1976 г. в мягкой обложке). Спрингер. ISBN  9781468494549 .
  • Пресбургер, Мойжес (1929). «О полноте некоторой системы арифметики целых чисел, в которой единственным действием является сложение». Comptes Rendus du I congrès de Mathematiciens de Pays Slaves, Варшава : 92–101. . см. в Stansifer (1984) английский перевод
  • Жаннерод, Николя; Трейнен, Ральф. Решение теории первого порядка алгебры деревьев признаков с обновлениями . Международная совместная конференция по автоматизированному рассуждению (IJCAR). дои : 10.1007/978-3-319-94205-6_29 .
Arc.Ask3.Ru: конец переведенного документа.
Arc.Ask3.Ru
Номер скриншота №: 392f26c3344ac6e825e097218f9f26c6__1713882540
URL1:https://arc.ask3.ru/arc/aa/39/c6/392f26c3344ac6e825e097218f9f26c6.html
Заголовок, (Title) документа по адресу, URL1:
Quantifier elimination - Wikipedia
Данный printscreen веб страницы (снимок веб страницы, скриншот веб страницы), визуально-программная копия документа расположенного по адресу URL1 и сохраненная в файл, имеет: квалифицированную, усовершенствованную (подтверждены: метки времени, валидность сертификата), открепленную ЭЦП (приложена к данному файлу), что может быть использовано для подтверждения содержания и факта существования документа в этот момент времени. Права на данный скриншот принадлежат администрации Ask3.ru, использование в качестве доказательства только с письменного разрешения правообладателя скриншота. Администрация Ask3.ru не несет ответственности за информацию размещенную на данном скриншоте. Права на прочие зарегистрированные элементы любого права, изображенные на снимках принадлежат их владельцам. Качество перевода предоставляется как есть. Любые претензии, иски не могут быть предъявлены. Если вы не согласны с любым пунктом перечисленным выше, вы не можете использовать данный сайт и информация размещенную на нем (сайте/странице), немедленно покиньте данный сайт. В случае нарушения любого пункта перечисленного выше, штраф 55! (Пятьдесят пять факториал, Денежную единицу (имеющую самостоятельную стоимость) можете выбрать самостоятельно, выплаичвается товарами в течение 7 дней с момента нарушения.)