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

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

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

Теории первого порядка

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

Важнейшими теориями первого порядка, допускающими элиминацию кванторов, являются арифметика Пресбургера, алгебраически замкнутые поля, замкнутые вещественные поля (теорема Зайденберга — Тарского), безатомные булевы алгебры, алгебра термов, плотный линейный порядок, теория абелевых групп, теория очередей. При этом, например, в целочисленной арифметике формула ∃ x ( x ⩾ 0 ∧ a + x = b ) {displaystyle exists x(xgeqslant 0land a+x=b)} эквивалентна формуле b ⩾ a {displaystyle bgeqslant a} , однако для формулы ∃ x ( a = x ⋅ b ) {displaystyle exists x(a=xcdot b)} не существует эквивалентной формулы, не содержащей кванторов, то есть, целочисленная арифметика не допускает элиминации кванторов.

Подход к доказательству

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

∃ x ⋀ i = 1 n L i {displaystyle exists xigwedge _{i=1}^{n}L_{i}} .

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

∃ x ⋁ j = 1 m ⋀ i = 1 n L i j {displaystyle exists xigvee _{j=1}^{m}igwedge _{i=1}^{n}L_{ij}}

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

⋁ j = 1 m ∃ x ⋀ i = 1 n L i j {displaystyle igvee _{j=1}^{m}exists xigwedge _{i=1}^{n}L_{ij}} .