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

    в) конечное (может быть и пустое) или счетное множество
    функциональных букв f 1 1 , f 2 2 , …, f l k ,…;
    г) непустое конечное или счетное множество предикатных букв
    A 1 1 , A 2 2 , …, A l m , P l k ,…;
    д) символы исчисления высказывании: ¬ , → , ~, &, ∨ ;
    е) скобки ( ) и запятая;
    ж) символы ∃ и ∀ ;
    з) других исходных элементов нет.
    2. Правила образования ППФ:
    а) всякий атом есть ППФ;
    б) если А и В – ППФ и х – предметная переменная, то каждое из
выражении ¬ А, А → В, А ~ В, А & В, А ∨ В, что ∃ xА, ∀ х А есть ППФ;
    в) других правил образования ППФ нет.
    Таким образом, форма записи ППФ совпадает с записью формул
исчисления предикатов.
    3. Система аксиом.
    К системе аксиом исчисления высказываний добавляются еще две
аксиомы:
    А1. ∀ х А(x) → A(t), где A(x) есть ППФ и t – терм, свободный для х
в А(х).
    А2. A(t) → ∃ xА(x), где A(x) есть ППФ и t – терм, свободный для х
в А(х).
    4. Правила вывода.
    п.1. Все аксиомы выводимы.
    п.2. Правило подстановки. Это правило аналогично правилу
подстановки, которое имеет место для исчисления высказываний.
Только в данном случае мы будем иметь дело с такой подстановкой
термов t 1 , t 2 , …, t n вместо x i , x i ,..., x i в A[ x i , x i ,..., x i ], что A[ x i , x i ,..., x i ]
                                             1   1     k           1   1      k                1   1      k


свободна для t 1 , t 2 , …, t n .
    Несоблюдение этого условия может привести к неприятным
последствиям. Например, пусть в аксиоме А1 терм t не свободен для
х в A[x] и пусть A[x] есть ППФ вида ¬ ∀ х 2 A(x 1 , x 2 ) и t есть х 2 . Тогда
терм t не свободен для x 1 , в ¬ ∀ х 2 A(x 1 , x 2 ).
    Рассмотрим следующий пример:

                ∀ х 1 ( ¬ ∀ х 2 A(x 1 , x 2 )) → ¬ ∀ х 2 A(x 2 , x 2 )

   и возьмем в качестве интерпретации любую область, содержащую
не менее двух элементов, а в качестве А – отношение тождества.
Тогда посылка ∀ х 1 ( ¬ ∀ х 2 A(x 1 , x 2 )) в данном примере истинна, а
заключение ¬ ∀ х 2 A(x 2 , x 2 ) ложно.
   п. 3. Правило modus ponens (МР).
   Если |- А и |- А → В, то |- В.



19