Наиболее распространенными правилами являются:
1) Введение квантора общности: “если F1(t)® F2(x) выводимая формула и F1(t) не содержит свободной переменной x , то F1(t)® «x(F2(x)) также выводима”, т.е.
(F1(t)® F2(x))
(F1(t)® «x(F2(x))).
2) Удаление квантора общности: «если «x(F(x)) выводимая формула, то вместо x можно выполнить подстановку терма t, свободного от x , и получить также выводимую формулу F (t), т.е.
«x(F(x))
. F (t).
3) Введение квантора существования: «если терм t входит в предикат F(t) , то существует, по крайней мере одна предметная переменная x , удовлетворяющая требованиям $x(F(x)) ”, т.е.
F(t)
$x(F(x)).
4) Смена квантора:
«x(F(x)) $x(F(x))
ù$x(ùF(x)); ù»x(ùF(x)).
5) Перенос квантора, если терм t не содержит переменной x:
a) Âx(F1(x))Ú F2(t)
Âx(F1(x)Ú F2(t));
b) Âx(F1(x))&F2(t)
Âx(F1(x)& F2(t);
c) F1(t)® Âx(F2(x))
Âx(F1(t)®F2(x));
d) «x(P(x))®F(t)
$x(P(x)®F(t));
e) $x(P(x))®F(t)
«x(P(x)®F(t)).
6) Введение новой переменной:
a) «x(F1(x))Ú»x(F2(x))
«y»x(F1(y)Ú F2(x));
b) $x(F1(x))&$x( F2(x))
$y$x(F1(y)Ú F2(x)).