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

    п. 4. Правило обобщения (или правило связывания квантором
общности) .
    Если ППФ В → А(х) при условии, что В не содержит свободных
вхождений х, выводима, то выводима будет и ППФ В → ∀ х А(х).
     п. 5. Правило конкретизации (или правило связывания квантором
существования).
    Если ППФ А(х) → В выводимая ППФ (теорема) и В не содержит
свободных вхождений х, то ∃ x А(х) → В также теорема.
    п. 6. Если А – теорема, имеющая квантор общности и/или квантор
существования, то одна связанная переменная в А может быть
заменена другой связанной переменной, отличной от всех свободных
переменных, одновременно во всех областях действия квантора и в
самом кванторе. Полученная ППФ также является теоремой.
    п. 7. Других правил вывода нет.
    Определение выводимости в исчислении предикатов является
расширением соответствующего определения для исчисления
высказываний. Поэтому среди выводимых ППФ исчисления
предикатов будут находиться все выводимые ППФ исчисления
высказывании.
    Будем считать, что ППФ В выводима из ППФ А (аналогично из
множества ППФ A 1 , A 2 , ….,A n ), если:
    1) A выводима из A;
    2) каждая выводимая в ФС ППФ также выводима и из A;
    3) из выводимости ППФ В 1 , и В 1 → В 2 , из А следует выводимость
В 2 из А;
    4) если ППФ В 1 → В 2 (х) выводима из А, причем В 1 и А не содержат
свободных вхождений х, то и ППФ В 1 → ∀ х В 2 (х) также выводима из
А;
    5) если ППФ В 2 (х) → В 1 выводима из А, причем В 1 и А не
содержат свободных вхождений х, то и ППФ ∃ x В 2 (х) → В 1 выводима
из А;
    6) если ППФ В выводима из ППФ А, то и В`, полученная из В
подстановкой термов вместо свободных вхождений в В переменных,
также выводима из А;
    7) если В выводима из А, то и В`, полученная из В любым
переименованием связанных переменных, отличных от имен
свободных переменных, выводима из А.
    Вывод ППФ из пустого множества посылок есть доказательство
этой ППФ, а сама ППФ называется теоремой.
    Для исчисления предикатов также имеет место теорема дедукции:
если A 1 , A 2 , ….,A n |- B, то |-A 1 → ( A 2 → (….,(A n → B)…)).
Остановимся         теперь      на      свойствах      исчисления  предикатов:
непротиворечивости и полноте. Как и раньше, будем считать




20