Основные понятия и методы теории формальных систем. Волохович А.В. - 4 стр.

     Множество аксиом – это выделенное подмножество ППФ. Если
множество аксиом бесконечно, то предполагается наличие
процедуры проверки по ППФ, является ли она аксиомой.
     Правила вывода позволяют из имеющегося множества ППФ
(утверждений) получать новые ППФ – непосредственные следствия
этих утверждений.
     Последовательность ППФ А 1 , А 2 , ..., А n называется выводом в
ФС, если для любого i=1,…,n ППA А i является либо аксиомой AС,
либо непосредственным следствием некоторых ППФ множества (A 1 ,
A 2 , …,A i - 1 ), получаемым применением к этим ППФ некоторого
правила вывода; ППФ A называется теоремой ФС, если в данной
ФС имеется вывод, в котором последней ППФ является A.
     Формальная система называется разрешимой, если существует
алгоритм определения по произвольной ППФ, является ли она
теоремой.          Если      такого    алгоритме    не    существует,       то
рассматриваемая ФС именуется неразрешимой.
     Правильно построенная формула B выводима из совокупности
 ППФ (А 1 , А 2 , ..., А n ), если существует последовательность ППФ В 1 ,
 В 2 , ..., В k такая, что В k =В и для любого i=1,..,k формула В i является
 либо аксиомой ФС, либо формулой множества (А 1 , А 2 , ..., А n ), либо
 непосредственным следствием некоторых ППФ множества (В 1 , В 2 ,
 ..., В k ), получаемых применением к этим ППФ одного из правил
 посылками или гипотезами. Формулы, выводимые из пустого
 множества посылок, являются теоремами.
     Запись А 1 , А 2 , ..., А n |- В означает выводимость формулы В из
множества посылок (А 1 , А 2 , ..., А n ); запись |- В означает, что В
является теоремой ФС. Если М={А 1 , А 2 , ..., А n }, то запись А 1 , А 2 , ...,
А n |- В можно представить записью М |- В.
     Очевидны следующие утверждения:
 – если M 1 ⊆ M и M 1 | −B , то M | −B ;
 – M | −B тогда и только тогда, когда в М имеется конечное
     подмножество M 1 такое, что M 1 | −B ;
  – если M 1 | − A и M 2 | −B для любой формулы В из множества M 1 ,
        M 2 | −A .
          Приведем простейший пример формальной системы. Считаем
алфавит состоящим из символов |, = , +. Правила конструкции ППФ
следующие:

    1)   | есть ППФ;
    2)   если а – ППФ, то а| также ППФ;
    3)   если а и b – ППФ, то а + b и а = b также ППФ;
    4)   других ППФ нет.




4