Понятие вывода

Определение. Выводом из конечной совокупности формул H называется всякая конечноая последовательность формул , всякий член которой удовлетворяет одному из следующих трех условий: 1) является одной из формул совокупности H; 2) является доказуемой формулой; 3) получается по правилу заключения из двух любых предшествующих членов последовательности .

Свойства вывода:

1) Всякий начальный отрезок вывода из совокупности H есть вывод из H.

2) Если между двумя соседними членами вывода из H вставить некоторый вывод из H, то полученная новая последовательность формул будет выводом из H.

3) Всякий член вывода из совокупности H, является формулой, выводимой из H.

Следствие. Всякий вывод из H является выводом его последней формулы.

4) Если , то всякий вывод из H является из W.

5) Для того, чтобы формула B была выводима из совокупности H, необходимо и достаточно, чтобы существовал вывод этой формулы из H.

Правила выводимости.

Пусть H и W – две совокупности формул исчисления высказываний и . Если W состоит из одной формулы C, то .

1) Если формула A выводима из совокупности H, то формула A выводима из совокупности H,W.

2) Если формула A выводима из совокупности H,C, а формула C выводима из совокупности H, то формула A выводима из совокупности H.

3) Если формула A выводима из совокупности H,C, а формула C выводима из совокупности W, то формула A выводима из совокупности H,W.

4) Если формула C→A выводима из совокупности H, то формула A выводима из совокупности H,C.

5) Теорема дедукции. Если формула A выводима из совокупности H,C, то формула C→A выводима из совокупности H.

6) Правило введения конъюнкции. Если формулы A и B выводимы из совокупности H, то формула выводима из совокупности H.

7) Правило введения дизъюнкции. Если формула C выводима из совокупностей H,A и H,B, то формула C выводима из совокупности .

Связь между алгеброй логики и исчислением высказываний.

Формулы исчисления высказываний можно интерпретировать как формулы алгебры логики.

Теорема. Каждая формула, доказуемая в исчислении высказываний является тавтологией в алгебре логики.

Обратная теорема. Каждая тождественно истинная формула (тавтология) алгебры логики доказуема в исчислении высказываний.