НАТУРАЛЬНЫЙ ВЫВОД
----------------------------------------------------------------------------
     Правила НАТУРАЛЬНОГО ВЫВОДА.

     Конъюнкция:
    F1   F2       F1 & F2       F1 & F2
&i  -------   &e1 -------   &e2 -------
    F1 & F2          F1            F2

     Дизъюнкция:
                                [┐F1] [┐F2]               [F1] [F2]
      F1            F2               ┴            F1VF2    F3   F3
Vi1 -------   Vi2 -------     Vi3 -------     Ve  ----------------
    F1 V F2       F1 V F2         F1 V F2                  F3

      Импликация:
     [F1]                                  [┐F3] [F2]
      F2          F1>F2  F1         F1>F2    F1   F3
>i  -------   >e1 ---------     >e2 ----------------
    F1 > F2          F2                     F3

      Отрицание и ложь:
                [F]       [┐F]
   ┐F   F        ┴          ┴
┴i ------    ┐i ---     ┐e ---
     ┴          ┐F          F

      Кванторы:                                      [(Svw)F]
    (Svw)F        A.v F        (Svt)F         E.v F    F1
Ai+ ------   Ae- ------    Ei- ------     Ee+ -----------
    A.v F        (Svt)F         E.v F               F1
     Обозначения: w - константа,  не встречающаяся в заключениях Ee+ и Ai+ и
гипотезах, от которых эти заключения зависят; t - терм, свободный для v в F;
(Sxy)F - подстановка: в F заменить x на y.

----------------------------------------------------------------------------
     Правила ПОИСКА НАТУРАЛЬНОГО ВЫВОДА.

     Конъюнкция:                          Дизъюнкция:
&ai  |- F1&F2 => |-F1 / |-F2         Vai  |- F1VF2 => ┐F1;┐F2 |- ┴
&si  F1; F2 => F1&F2                 Vae  F1VF2 |- F3 => F1|-F3 / F2|-F3
&se1 F1&F2  =>  F1                   Vsi1 F1 => F1VF2
&se2 F1&F2  =>  F2                   Vsi2 F2 => F1VF2

     Импликация:                                  Отрицание и ложь:
>ai  |- F1>F2 => F1|-F2                      ┴si     ┐F; F => ┴
>ae2 F1>F2|-F3 => ┐F3|-F1 / F2|-F3           ┴del ┴|- F =>
>ae  F1>F2 |-F2 => |-F1                      ┐ai    |- ┐F => F |- ┴
>si  F2 => F1>F2                             ┐ae1  |- F => ┐F |- ┴
>se  F1>F2; F1 => F2                         ┐ae2 ┐F|- ┴ => |-F

     Кванторы:
Aai+ |- A.vF => |- (Svw)F                        w - новая константа
Ase  A.vF => (Svt)F                              t - терм, свободный
Eai  |- E.vF => ┐E.vF |- (Svt)F                  для v в формуле F
Esi  F => E.v (Stv)F
Ese+ E.vF => (Svw)F
----------------------------------------------------------------------------