Понятие вывода и его свойства

Заложив основу будущей аксиоматической теории в виде системы аксиом и правила вывода, приступим к её развитию, то есть к доказательству теорем. Прежде всего, уточним понятия доказательства и теоремы.

Определение 14.1. Доказательством или выводом формулы F из множества формул Г называется такая конечная последовательность В₁, В₂, …, B_s формул, каждая формула которой является либо аксиомой, либо формулой из Г, либо получена из двух предыдущих формул этой последовательности по правилу МР, а последняя формула B_s совпадает с F. Если имеется вывод формулы F из множества Г, то говорят, что F выводима из Г, или что Г выводит F, и пишут Г? F. Элементы из Г называются гипотезами или посылками вывода. Если же имеется вывод формулы F из пустого множества гипотез, то говорят, что F выводима из аксиом, или что F доказуема, а последовательность В₁, В₂, …, B_s называется доказательством этой формулы. Саму F называют теоремой и пишут F. Таким образом, запись «F» служит сокращением утверждения «F есть теорема».

Если множество Г конечно: Г = {F₁, F₂, …, F_m}, то вместо {F₁, F₂, …, F_m? G будем писать F₁, F₂, …, F_mG.

Совокупность аксиом, правил вывода и всех теорем, выводимых из аксиом, и представляет собой аксиоматическую теорию высказываний, или формализованное исчисление высказываний. Наша ближайшая цель состоит в том, чтобы научиться доказывать теоремы в данной теории, то есть научиться строить выводы формул из аксиом.

Приведем пример доказательства какой-нибудь формулы.

Пример 14.2. Доказать: F F.

Для доказательства того, что формула F F является теоремой формализованного исчисления высказываний, нужно построить вывод (доказательство) этой формулы из аксиом. Таким выводом является, например, следующая последовательность формул:

(F ((F F) F)) ((F (F F)) (F F)),.

F ((F F) F),.

(F (F F)) (F F),.

F (F F),.

F F.

Поясним. Формула (1) представляет собой аксиому (А2), в которой в качестве формул F и Н взята формула F, а в качестве формулы G взята формула FF. Формула (2) представляет собой аксиому (А1), в которой в качестве формулы G берется формула F F. Формула (3) получена из формул (1) и (2) по правилу МР. Формула (4) есть аксиома (А1). Наконец, формула (5) получена из формул (3) и (4) по правилу МР.

Таким образом, F F.

В следующей теореме отмечается несколько простых, но важных свойств понятия выводимости из гипотез.

Теорема 14.3 (свойства выводимости).

• а) Если ГF и Г, то F.
• б) ГF тогда и только тогда, когда в Г существует такое конечное подмножество, что F.
• в) Если G для любой формулы G из множества и? F, то Г? F.

Доказательство. а) Данное свойство выражает следующий очевидный факт: если формула F выводима из множества посылок Г, то она будет выводима и из всякого множества, получающегося добавлением к Г новых посылок.

• б) Достаточность вытекает из свойства (а). Обратно, если Г? F, то, по определению 14.1, существует вывод F из Г, то есть некоторая конечная последовательность формул, использующая, следовательно, лишь конечное число посылок из Г. Поэтому можно считать, что именно эта конечная часть формул из Г и выводит формулу F.
• в) По условию,? F. Тогда, ввиду предыдущего свойства (б), в существует такое конечное подмножество ₀, что ₀? F. Пусть ₀ = {В₁, В₂, …, B_k. По условию, кроме того, Г? B₁, Г? В₂,…, Г? B_k, то есть имеются выводы каждой из формул В₁, В₂, …, B_k из множества гипотез Г, представляющие собой конечные последовательности формул. Выпишем эти последовательности одну за другой и добавим к ним последовательность, являющуюся выводом формулы Г из множества гипотез ₀ = {В₁, В₂, …, B_k. Полученная таким образом последовательность будет представлять собой вывод формулы F из множества гипотез Г, то есть Г F.