Наша задача: привести произвольную формулу к бескванторной форме. Это можно решить приведением к пренексной нормальной форме с последующей элиминацией кванторов и расширением исходного языка.
Пренексная нормальная форма
Формула Q1y1Q2y2 … Qnyn q, где – Qi кванторы, а q не имеет кванторов, называется пренексной (или предваренной) нормальной формой. Существует эффективная процедура приведения формулы к пренексной нормальной форме. Она основана на следующих далее правилах преобразования, вытекающих из логических аксиом исчисления предикатов.
Обозначим "¢ = $, $¢ = ". Имеет место эквивалентность формул ØQxq º Q¢xØq. При условии, что переменная х не входит свободно в формулу y, верны равенства:
1) Qxq & y º Qx(q & y);
2) Qxq Ú y º Qx(q Ú y);
3) (y ® Qxq) º Qx(y ® q);
4) (Qxq ® y) º Q¢x(q ® y);
Имеет место эквивалентность формул:
5) Qxq º Qyq(x/y)
Пример 1
Найдём пренексную нормальную форму формулы $xq « y, где q и y не содержат кванторов, и х не входит свободно в y. Представим её как
($xq ® y) & (y ® $xq).
С помощью равенств 3 – 4 она приводится к виду:
"x(q ® y) & $x(y ® q).
С помощью равенства 1 – к виду: "x((q ® y) & $x(y ® q)).
С помощью равенства 5 – к виду: "x((q ® y) & $y(y ® q(y/x))),
где y не входит в преобразуемую формулу. Снова из равенства 1 получаем:
"x$y((q ® y) & (y ® q(y/x))).
Элиминация кванторов
По пренексной нормальной форме q строится формула q*, не содержащая кванторов. Кванторы всеобщности удаляются, а кванторы существования заменяются на функциональные символы, добавляемые к языку:
$yq(y, x1, …, xn) переходит в q(f(x1, …, xn), x1, …, xn), и операция f добавляется к языку.
Пример 2
Пусть q º$x1 "x2 "x3 $x4 $x5 "x6 y(x1, x2, x3, x4, x5, x6). Выполним действия для приведения к бескванторной форме:
1) удалим $x1 и заменим x1 константой b1:
"x2 "x3 $x4 $x5 "x6 y(b1, x2, x3, x4, x5, x6);
2) удалим два квантора всеобщности:
$x4 $x5 "x6 y(b1, x2, x3, x4, x5, x6);
3) удалим квантор существования и к L добавим символ операции x4 = f(x2, x3):
$x5 "x6 y(b1, x2, x3, f(x2, x3), x5, x6);
4) удалим квантор существования и к L добавим символ операции x5 = g(x2, x3):
"x6 y(b1, x2, x3, f(x2, x3), g(x2, x3), x6);
5) удалим квантор всеобщности:
q¢¢ = y(b1, x2, x3, f(x2, x3), g(x2, x3), x6).
Полученная формула определена в языке L¢¢ = L È {b1, f, g}.
Пусть å – множество предложений в языке L. Обозначим через q¢¢ формулу, полученную из предложения q приведением к пренексной нормальной форме с последующей элиминацией кванторов и преобразованием языка L. Положим 
. Пусть в результате преобразований формул q Î å в q¢¢ мы пришли к расширенному языку L¢¢.
Теорема (вторая e-теорема)
а) Если y – формула языка L, то вывод 墢 
y существует тогда и только тогда в L¢¢, когда существует вывод å y в L
б) Теория å непротиворечива, если и только если непротиворечива теория 墢.