Выводимость и доказуемость формул

Определение 9.16. Выводом формулы А из конечного или бесконечного множества формул Т в исчислении α называется конечная последовательность формул

А₁, А₂, …, A_n,

в которой A_n = A и каждая из формул A_i, i = 1, …, n является или аксиомой, или формулой из Т (исходной формулой), или получается по некоторому правилу вывода из предыдущих формул этой последовательности.

Если существует вывод формулы А из множества формул Т исчисления α, то говорят, что в α А выводима из Т и пишут

Т ├─ А, или В₁, В₂, …, В_К ├─ А,

α α

если Т = {В₁, В₂, …, В_К}. При этом формулы из Т называют посылками вывода.

Особо важным является случай, когда Т — пустое множество.

Определение 9.17. Формула из А языка α , выводимая в исчислении α из пустого множества формул, называется доказуемой формулой, или теоремой исчисления α, а сам вывод формулы А из пустого множества формул называется ее доказательством. Если формула А доказуема в исчислении α, то пишут

├─ А.

α

Так как у нас исчисление α фиксировано, то букву α будем опускать и писать просто

Т ├─ А; В₁, В₂, …, В_К ├─ А; ├─ А.

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

Дальше нас будут интересовать вопросы о характеризации доказуемых формул и формул, выводимых из заданного множества, вопросы о непротиворечивости и полноте исчисления α. Предварительно приведем доказательства некоторых формул и вспомогательных правил вывода. При этом последовательности формул, являющиеся доказательствами или выводами, будем записывать в столбик, указывая справа их происхождение (номер аксиомы, номер правила вывода, порядковые номера исходных формул и т.п.).

Теорема 9.18. ├─ А ® А для любой формулы А.

Доказательство.

Теорема 9.19. Если А — любая формула и В — доказуемая формула, то ├─ А ® В.

Доказательство получается и добавлением к доказательству формулы В аксиомы I₁ и формулы А ® В, получаемой из В и аксиомы I₁ по правилу I.

Теорема 9.20. ├─ АВ ® ВА для любых формул А, В.

Доказательство.

Заменяя в доказательстве теоремы 9.20 II₁ II₃ соответственно аксиомами III₁ – III₃, получим доказательство следующей формулы.

Теорема 9.21. ├─ А Ú В ® В Ú А для любых формул А, В.

Теорема 9.22. ├─ для любой формулы А(х), содержащей свободные вхождения переменной х.

Доказательство.

1.	А(х) ® $х А(х).	(V2)
2.	(А(х) ® $хА(х)) ® .	(IV3)
3.	.	(I, 1, 2)
4.	.	(I, 1, 3)

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

AC ® D ├─ A ® (C ® D).

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

Ряд наиболее распространенных вспомогательных правил вывода можно получить из так называемой теоремы дедукции. Однако и ее формулировка и доказательство в общем случае сложны. Мы пока рассмотрим один ее ослабленный вариант.

Теорема 9.23 (об ограниченной дедукции). Пусть Т — произвольное множество формул, и А, В — произвольные формулы. Если T, A├─ B и существует вывод формулы В из T È {A}, в котором не используются правила "-введения и $-удаления, то T ├─ A ® B.

Доказательство. Пусть В₁, В₂, …, В_m = B есть вывод формулы В из T È {A}, в котором не используются правила "-введения и $-удаления. Докажем утверждение теоремы индукцией по длине вывода m.

Пусть m = 1. Тогда В является или аксиомой, или посылкой. Если В — аксиома, то она, очевидно, доказуема, и по теореме 9.19 имеем ├─ A ® B для любой формулы А. Пусть В — посылка. Если В = А, то T ├─ A ® B следует из теоремы 9.18. Если же В Î Т, то можно указать следующий вывод формулы А ® В из Т:

Допустим, что теорема верна при m £ n, и докажем ее для m = n + 1. В этом случае по условию формула В будет или аксиомой, или посылкой, или непосредственным следствием двух предыдущих формул B_i, B_j по правилу заключения. Если В — аксиома или посылка, то T ├─ A ® B устанавливается точно так же, как и при m = 1. Пусть В получается из B_i, B_j по правилу заключения, т.е. B_J = B_i -> B. Так как i < n, j < n, то по предположению индукции имеем: T ├─ A ® B_i, T ├─ A ® (B_i ® B). Применяя теперь к формулам A ® (B_i ® B), A ® B_i и к аксиоме I₂

(A ® (B_i ® B)) ® ((A ® B_i) ® (A ® B))

дважды правило заключения, получим формулу А ® В. Теорема доказана.

Докажем теперь ряд вспомогательных правил вывода, обозначая в них буквами А, В, С произвольные формулы α.

Правило умножения формул:

A, B ├─ AB.

Вывод:

Правило силлогизма:

A ® B, B ® C├─ A ® C.

В ы в о д. Согласно теореме дедукции достаточно показать, что A ® B, B ® C, A├─ C, причем существует вывод С, не использующий правил "-введения и $-удаления. Таким выводом может служить последовательность формул: А, А ® В, В, В ® С, С. Для ее получения дважды применяется правило заключения к посылкам.

Аналогично доказываются следующие правила.

Правило де Моргана: а) ├─ , б) ├─ .

Вывод правила а):

1.	AB -> A	(II1)
2.	AB -> B	(II2)
3.		(правило контрапозиции, 1)
4.		(правило контрапозиции, 2)
5.		(правило сложения посылок, 3, 4)
6.		(посылка)
7.		(1, 5, 6)

Вывод правила б):

1.		(III1)
2.		(III2)
3.		(правило контрапозиции, 1)
4.		(правило контрапозиции, 2)
5.		(IV2)
6.		(IV2)
7.		(правило силлогизма, 3, 5)
8.		(правило силлогизма, 4, 6)
9.		(правило умножения заключений, 7, 8)
10.		(правило контрапозиции, 9)
11.		(IV2)
12.		(правило силлогизма, 10, 11)

Правило $-отрицания:

а) ├─ (следует непосредственно из теоремы 9.6.7);

б) ├─ .

Вывод правила б):

1.		(V1)
2.		(правило контрапозиции, 1)
3.		(IV1)
4.		(правило силлогизма, 2, 3)
5.		(III, 4)
6.		(правило контрапозиции, 5)
7.		(IV1)
8.		(правило силлогизма, 6, 7)

Правило "-отрицания: а) ├─ ;

б) ├─ .

Докажите в качестве упражнения.

Правило противоречия: ├─ В (из противоречия выводима любая формула).

Выведем произвольную формулу В из , используя при этом любую доказуемую формулу R, например, А ® А.

1.	A ® (R ® A)	(I1)
2.		(IV3)
3.		(правило силлогизма, 1, 2)
4.		(правило умножения посылок, 3)
5.
6.		(правило контрапозиции, 5)
7.		(правило силлогизма, 4, 6)
8.		(IV2)
9.		(правило силлогизма, 7, 8)
10.		(посылка)
11.	B	(1, 9, 10)

Правило (закон) исключенного третьего: ├─ .

Доказательство (снова используем доказуемую формулу R):

1.		(III1)
2.		(III2)
3.		(правило контрапозиции, 1)
4.		(правило контрапозиции, 2)
5.		(IV1)
6.		(правило силлогизма, 4, 5)
7.		(правило умножения заключений, 7, 8)
8.		(правило противоречия и теорема дедукции)
9.		(правило силлогизма, 7, 8)
10.		(правило контрапозиции, 9)
11.		(IV1)
12.		(правило силлогизма, 10, 11)
13.		(IV2)
14.		(правило силлогизма, 12, 13)
15.	R
16.		(1, 14, 15)

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

Теорема дедукции 9.24 (для замкнутой формулы).

Если Т произвольное множество формул, В — произвольная, А — замкнутая формулы и T, A├─ B, то T├─ A ® B.

Доказательство. Производится так же, как теоремы об ограниченной дедукции. В дополнение нам необходимо лишь рассмотреть два случая (при m = n + 1):

а) В получается по правилу "-введения из формулы B_i;

б) В получается по правилу $-удаления из формулы B_i.

В случае «а» имеем: B_i = C ® D(x), B = C ® "x D(x), причем С не содержит свободных вхождений х. По предположению индукции имеем:

T├─ A ® (C ® D(x)).

Дополним вывод формулы A ® (C ® D(x)) следующими формулами до вывода формулы А ® В:

AC ® D(x) (правило умножения посылок)

AC ® "x D(x) (правило "-введения)

A ® (C ® "x D(x)) = A ® B (правило разделения посылок)

В случае «б»: B_i = C(x) ® D, B = $x C(x) ® D, где D не содержит свободных вхождений х. По предположению индукции

T├─ A ® (C(x) ® D).

Отсюда, используя правила перестановки посылок и $-удаления, получим:

T├─ C(x) ® (A ® D);

T├─ $x C(x) ® (A ® D);

T├─ A ® ($x C(x) ® D) = A ® B.

Теорема доказана.

Укажем одно следствие теоремы дедукции.

Следствие. Если Т — любое множество формул, А — замкнутая, В — любая формулы и T, A├─ , то T├─ .

Доказательство. По теореме дедукции T├─ A ® . Применяя правило контрапозиции, получим T├─ . Из правила де Моргана «а» и закона исключенного третьего следует, что ├─ , для любой формулы В. Следовательно, T├─ .