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

Определение. Выводом из конечной совокупности формул Н называется всякая конечная последовательность формул В₁, В₂, ..., B_k , всякий член которой удовлетворяет одному из следующих трех условий:

1. 
   он является одной из формул совокупности Н,
   
2. 
   он является доказуемой формулой,
   
3. 
   он получается по правилу заключения из двух любых предшествующих членов последовательности В₁, В₂, ..., В_k.
   

Как было показано в предыдущем примере, выводом из совокупности формул Н = {А, В является конечная последовательность формул:
А, В, , , АА, , АB, , .
Если же здесь воспользоваться правилом сложного заключения, то вывод можно записать так:
А, В, , , АА, АB, .
Из определений выводимой формулы и вывода из совокупности формул следуют очевидные свойства вывода:
1) Всякий начальный отрезок вывода из совокупности Н есть вывод из Н.
В самом деле, все формулы начального отрезка вывода удовлетворяют определению вывода.
2) Если между двумя соседними членами вывода из Н (или в начале, или в конце его) вставить некоторый вывод из Н, то полученная новая последовательность формул будет выводом из Н.
3) Всякий член вывода из совокупности Н является формулой, выводимой из Н.
Всякий вывод из Н является выводом его последней формулы.
4) Если Н  W , то всякий вывод из Н является выводом из W.
5) Для того, чтобы формула В была выводима из совокупности Н, необходимо и достаточно, чтобы существовал вывод этой формулы из Н.


Правила выводимости
Пусть Н и W – две совокупности формул исчисления высказываний. Будем обозначать через Н, W их объединение, то есть H,W = HW.
В частности, если совокупность W состоит из одной формулы С, то будем записывать объединение Н{С} в виде Н,С.
Рассмотрим основные правила выводимости:
1. Если Н├А, то H,W├A.
Это правило следует непосредственно из определения вывода из совокупности формул.
2. Если Н,С├А и Н├С, то Н├А.
3. Если Н,С├А и W├С, то Н,W├А.
4. Если Н├ , то Н,С├А.
5. Теорема дедукции: Если Н,С├А, то Н├ .
Важным следствием из теоремы дедукции является обобщенная теорема дедукции: Если ├ А, то ├ .
6. Правило введения конъюнкции: Если Н├А и Н├В, то Н├ .
7. Правило введения дизъюнкции: Если Н,А├С и Н,В├С, то Н, ├С.