Элиминация кванторов

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

Процессы нахождения алгоритмов элиминации кванторов для различных теорий имеют общие черты, что позволяет говорить о них как о едином методе. Название метод элиминации кванторов ввёл в обиход Тарский в 1935 году, хотя впервые соображения такого рода были применены ещё Ленгфордом в 1927 году. Метод элиминации кванторов применим только к теориям очень специального вида, кроме того, каждый раз, когда этот метод применяется к новой теории, приходится проводить все доказательства с самого начала, так как арсенал общих результатов весьма скуден. Однако, если его удаётся применить, этот метод оказывается чрезвычайно полезным, так как даёт исчерпывающую информацию о данной теории. Обычно он также приводит к регулярному способу, позволяющему решить, принадлежит ли некоторое высказывание данной теории или нет — иными словами, даёт доказательство разрешимости теории.

Теории первого порядка[править | править код]

Теория первого порядка ${\displaystyle {\mathcal {T}}}$ допускает элиминацию кванторов, если для любой (не обязательно замкнутой) формулы ${\displaystyle \varphi }$ этой теории существует формула ${\displaystyle \psi }$, не содержащая кванторов, такая что ${\displaystyle {\mathcal {T}}\models \varphi \leftrightarrow \psi }$, то есть обе формулы эквивалентны на всех моделях теории ${\displaystyle {\mathcal {T}}}$.

Важнейшими теориями первого порядка, допускающими элиминацию кванторов, являются арифметика Пресбургера, алгебраически замкнутые поля, замкнутые вещественные поля^[en] (теорема Зайденберга — Тарского), безатомные булевы алгебры, алгебра термов, плотный линейный порядок^[en], теория абелевых групп, теория очередей. При этом, например, в целочисленной арифметике формула ${\displaystyle \exists x(x\geqslant 0\land a+x=b)}$ эквивалентна формуле ${\displaystyle b\geqslant a}$, однако для формулы ${\displaystyle \exists x(a=x\cdot b)}$ не существует эквивалентной формулы, не содержащей кванторов, то есть, целочисленная арифметика не допускает элиминации кванторов.

Подход к доказательству[править | править код]

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

${\displaystyle \exists x\bigwedge _{i=1}^{n}L_{i}}$.

Квантор всеобщности можно заменить на квантор существования, так как ${\displaystyle \forall xF}$ эквивалентно ${\displaystyle \lnot \exists x\lnot F}$. Дальше, формулу можно записать в дизъюнктивной нормальной форме и воспользоваться тем фактом, что:

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

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

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

Литература[править | править код]

• Кейслер Г., Чен Ч. Теория моделей. — М.: Мир, 1977.
• Н. К. Верещагин, А. Шень. 2. Языки и исчисления // Лекции по математической логике и теории алгоритмов. — М.: МЦНМО, 2012.