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

    Система аксиом включает единственную аксиому: | = |.
Единственное правило вывода следующее: из ППФ a = b выводится
а + | = b |.
    Очевидно, что теоремой в введенной ФС будет любая формула
вида
               |+|+|+…+|=|…|,

где слева и справа от знака = стоит одинаковое число символов |;
других теорем в ФС нет.



           Исчисление высказываний как формальная система

   Исчисление высказываний (ИВ) представляем в виде формальной
системы. Алфавит ИВ образуют буквы латинского алфавита с
числовыми индексами или без них (эти буквы называются
высказывательными     переменными     или   атомами),    символы
логических связок ¬ (отрицание ), & (конъюнкция), ∨ (дизъюнкция),
→ (импликация), а также левая и правая скобки.

       Правила образования ППФ:

    1) все атомы являются ППФ;
    2) если А и В – ППФ, то ¬ (A), (А&В), (А ∨ В), (А → В)– также ППФ.
   3) других ППФ не существует.
   Скобки,    расположение   которых                  в    ППФ   определяется
однозначно, мы иногда будем опускать.

    Система аксиом ИВ (введена П. С. Новиковым):

           1)   A → (B → A ) ,
           2)   ( A → B ) → ( A → ( B → C ) → ( A → C )) ,
           3)   (A & B) → A ,
           4)   (A & B) → B ,
           5)   A → ( B → ( A & B )) ,
           6)   A → (A ∨ B) ,
           7)   B → (A ∨ B) ,
           8)   ( A → C ) → (( B → C ) → (( A ∨ B ) → C )) ,
           9)   ( A → B ) → (( A → ¬B ) → A ) ,
           10) ¬¬A → A ,
           11) A → ¬¬A .


5