Логика - доступно для всех

Наиболее распространенными правилами являются:

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)).