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

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

Более точно, говорят, что теория первого порядка T допускает элиминацию кванторов, если для любой (не обязательно замкнутой) формулы A существует формула B, не содержащая кванторов, такая что формулы A и B эквивалентны в теории T, то есть в этой теории выводима их эквивалентность: .

Так, в арифметике (то есть теории натуральных чисел с операциями сложения и умножения, с константой 0 и предикатом равенства) формула эквивалентна бескванторной формуле x = 0. В той же теории формула , означающая, что число y делится на x, не эквивалентна никакой бескванторной формуле. Таким образом, арифметика не допускает элиминации кванторов.

Элиминацию кванторов ввел Альфред Тарский в 1935 году как метод доказательства разрешимости теорий. Метод состоит в предъявлении алгоритма, который по всякой формуле в данном языке строит эквивалентную ей бескванторную формулу. Имея этот метод (и алгоритм проверки выводимости бескванторных формул в данной теории, который для многих важных теорий существует и довольно прост), мы получаем алгоритм проверки выводимости любых формул в данной теории. Важнейшими теориями, допускающими элиминацию кванторов (и тем самым разрешимыми) являются:

• теория плотного линейного порядка — теория в языке с единственным двуместным предикатным символом < и аксиомами, утверждающими, что это линейный порядок (иррефлексивное транзитивное отношение, причем любые два различных элемента сравнимы), являющийся плотным (то есть между любыми двумя элементами x < y есть элемент z, такой что x < y < z). Примером плотного линейного порядка может служить множество рациональных чисел, рациональных чисел на интервале (0,1), действительных чисел.
• арифметика Пресбургера — теория натуральных чисел, являющаяся фрагментом арифметики Пеано в языке без умножения (лишь со сложением, константами 0 и 1 и равенством).
• теория вещественно-замкнутых полей — теория вещественных чисел в языке с операциями сложения и умножения и аксиомой, утверждающей, что всякий многочлен нечетной степени имеет корень. Результат об элиминации кванторов в этой теории является известной теоремой Тарского.