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

   В ИВ имеются два правила вывода - подстановка и modus ропепs
(дедуктивного вывода).
   Правило подстановки применяется к имеющейся ППФ А,
содержащей некоторый атом X. Одновременной заменой всех
вхождений этого атома в А(X) на произвольную ППФ В мы получим
формулу A(В), которую именуем результатом подстановки в ППФ
А(X) формулы В.
   Если А(X) – теорема ИВ, то A(В) – тоже теорема ИВ.
   Приведем пример. Подставив в аксиому 8 ИВ формулу (С&D)
вместо атома С, получаем следующую теорему ИВ:

         ( A → (С & D ) ) → (( B → (С & D ) ) → (( A ∨ B ) → (С & D ) )) .

     Правило дедуктивного вывода (modus ponens) применяется к
имеющейся паре ППФ А и А → В; результатом применения данного
правила является ППФ В.
     Если A и А → В являются теоремами ИВ, то В - также теорема ИВ.
     Будем трактовать символы ¬ , &, ∨ , → как функции алгебры
логики. Тогда каждая ППФ, сконструированная из атомов X 1 , X 2 , …,
X n , на любых наборах их логических значений (0 или 1, ложь или
истина) обращается в ложь или истину.
     Правильно построенная формула, которая является истинной на
всех наборах логических значений ее переменных, именуется
общезначимой.
     Правильно построенную формулу А именуем невыполнимой
(противоречивой), если ППФ ¬ А является общезначимой.
     Можно проверить, что все аксиомы ИВ являются общезначимыми
ИПФ. Оба правила вывода сохраняют общезначимость. Получаем
справедливость следующего утверждения:
      "Каждая теорема ИВ является общезначимой ППФ".
     Полноту приведенной системы аксиом утверждает следующий
факт:
     "Каждая общезначимая ППФ является теоремой ИВ".
     Система аксиом П.С.Новикова обладает также свойствами
непротиворечивости и независимости.
     Далее под термином "формула" понимаем ППФ.
     Две формулы ИВ называются эквивалентными, если на любом
наборе логических значений составляющих их атомов они
одновременно обращаются в истину или одновременно обращаются в
ложь. Эквивалентность обозначаем символом =.
     Легко убедиться, что

                 (А → В )=( ¬ А ∨ В);


6