Т. А. Сливина математическая логика и теория алгоритмов

§ 3. Производные правила вывода

Производные правила вывода, как и рассмотренные правила подстановки и заключения, позволяют получать новые доказуемые формулы. Они получаются с помощью правил подстановки и заключения, а поэтому являются производными от них.

1. Правило одновременной подстановки.
Пусть А – доказуемая формула; х₁, х₂, ..., х_n – переменные, а В₁, В₂, …, В_п – любые формулы исчисления высказываний. Тогда результат одновременной подстановки в А вместо х₁, х₂, ..., х_n соответственно формул В₁, В₂, ..., В_n является доказуемой формулой.
2. Правило сложного заключения.
Второе производное правило применяется к формулам вида и формулируется так: если формулы A₁, A₂, ..., А_n и доказуемы, то и формула L доказуема.
Это утверждение легко доказывается последовательным применением правила заключения.
3. Правило силлогизма.
Если доказуемы формулы и , то доказуема формула .
4. Правило контрпозиции.
Если доказуема формула , то доказуема формула .
5. Правило снятия двойного отрицания.
а) Если доказуема формула , то доказуема формула .
б) Если доказуема формула , то доказуема формула .


§ 4. Выводимость формул из совокупности формул

Будем рассматривать конечную совокупность формул Н = {A₁, A₂,...,A_n}.

Определение формулы, выводимой из совокупности Н.

1. 
   Всякая формула А_iН является формулой, выводимой из Н.
   
2. 
   Всякая доказуемая формула выводима из Н.
   
3. 
   Если формулы С и С  В выводимы из совокупности Н, то формула В также выводима из Н.
   

Если некоторая формула В выводима из совокупности Н, то записывают Н├В .
Нетрудно видеть, что класс формул, выводимых из совокупности Н, совпадает с классом доказуемых формул в случае, когда совокупность Н содержит только доказуемые формулы, и в случае, когда Н пуста.
Если же совокупность формул Н содержит хотя бы одну не доказуемую формулу, то класс формул, выводимых из Н, шире класса доказуемых формул.
Пример:
Доказать, что из совокупности формул Н={А,В} выводима формула .
Доказательство: так как АН и ВН, то по определению выводимой формулы
Н├А, (1)
Н├В. (2)
Возьмем аксиомы II₃ и I₁ и выполним подстановки
и
В результате получим доказуемые формулы, которые выводимы из H по определению выводимой формулы, то есть
Н├ (3)
Н├ (4)
Так как формула АА доказуема, то
Н├ АА (5)
Из формул (5) и (3) по правилу заключения получаем:
H├ (6)
Из формул (2) и (4) по правилу заключения получаем:
Н├ АB (7)
Из формул (7) и (6) по правилу заключения получаем:
Н ├ (8)
И, наконец, из формул (1) и (8) получаем
Н├ (9)
Ясно, что при доказательстве выводимости формулы из совокупности формул можно пользоваться не только основным правилом заключения, но и правилом сложного заключения. Тогда, пользуясь этим правилом, предложение (9) можно получить из предложений (5), (7), (1) и (3).