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

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

Элиминация кванторов в теориях первого порядка

Говорят, что теория первого порядка $\mathcal{T}$ допускает элиминацию кванторов, если для любой (не обязательно замкнутой) формулы $\varphi$ этой теории существует формула $\psi$, не содержащая кванторов, такая что $\mathcal{T}\models\varphi\leftrightarrow\psi$, то есть обе формулы эквивалентны на всех моделях теории $\mathcal{T}$. Например, в целочисленной арифметике формула $\exists x (x\geq 0 \land a + x = b)$ эквивалентна формуле $b\geq a$, однако для формулы $\exist x (a = x\cdot b)$ не существует эквивалентной формулы, не содержащей кванторов. Таким образом целочисленная арифметика не допускает элиминации кванторов.

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

Важнейшими теориями, допускающими элиминацию кванторов, являются:

• Арифметика Пресбургера
• Действительно-замкнутые поля,
• Безатомные булевы алгебры
• Алгебра термов
• Плотный линейный порядок
• Теория очередей

Литература

• Кейслер Г.,Чен Ч. Теория моделей., М., Мир, 1977