1. Любая аксиома в исчислении высказываний является тавтологией.
2. Любая теорема в исчислении высказываний является тавтологией.
Доказательство. То, что каждая аксиома A1-A3 является тавтологией легко проверить с помощью таблиц истинности. Для доказательства пункта 2 теоремы, предварительно докажем, что правило modus ponens, примененное к тавтологиям приводит к тавтологиям.
Действительно, пусть при произвольном распределении истинностных значений формулы A и AÉB являются тавтологиями. Тогда формула A истинна и, по свойствам импликации, B истинно. Следовательно, B - тавтология.
Для доказательства обратного утверждения нам потребуется несколько лемм.
Лемма 5.1. (теорема о дедукции - Эрбран, 1930 г.). Если G - множество формул, A и B - формулы и G,A |― B, то G |― AÉB. В частности, если A|― B, то |― AÉB.
Доказательство. Пусть B1, B2,..., Bn есть вывод из GÇ{A}, где Bn=B. Индукцией по i (1£ i £ n) докажем, что G |― AÉB.
Базис индукции. B1 должно быть элементом G, либо быть аксиомой, либо совпадать с A. По схеме аксиом A1 формула B1É(AÉ B1) является аксиомой. Поэтому в первых двух случаях G |― AÉB по modus ponens. В третьем случае, когда B1 совпадает с A, мы имеем |― AÉ B1 (см. пример 5.3) и, следовательно, G |― AÉ B1.
Индуктивный переход. Допустим теперь, что G |― AÉBk для любого k<i. Для Bi имеем четыре возможности:
1) Bi есть аксиома;
2) BiÎ G;
3) Bi совпадает с A;
4) Bi следует по modus ponens из некоторых Bs и Bm, где s<i и m<i и Bm имеет вид BsÉ Bi.
В первых трех случаях G |― AÉB доказывается также как при i=1. В последнем случае применим индуктивное предположение, согласно которому G |― AÉBs и G |― AÉ(BsÉBi). По схеме аксиом A2, |―( AÉ(BsÉBi)) É ((AÉBs )É(AÉBi)). Следовательно, по modus ponens, G|― (AÉBs )É(AÉBi) и, снова по modus ponens, G |― AÉBi.
Следствие.
1. AÉB, BÉC |―AÉC.
2. AÉ(BÉC), B |―AÉC.
Доказательство 1.
(a) AÉB гипотеза
(b) BÉC гипотеза
(c) A гипотеза
(d) B применяя modus ponens из (a) и (c)
(e) C применяя modus ponens из (b) и (d)
Таким образом, AÉB, BÉC, A |― C. Отсюда по теореме дедукции, AÉB,BÉC|― AÉC.
Доказательство 2.
(a) AÉ(BÉC) гипотеза
(b) B гипотеза
(c) A гипотеза
(d) BÉC применяя modus ponens из (a) и (c)
(e) C применяя modus ponens из (b) и (d)
Таким образом, AÉ(BÉC),B,A|―C. Отсюда по теореме дедукции, AÉ(BÉC),B|― AÉC.
Теорема о дедукции служит обоснованием для исчисления высказываний следующего приема, который часто используют в математических доказательствах. Для того, чтобы доказать утверждение "Если A, то B" предполагают, что справедливо A и доказывают справедливость B.
Лемма 5.2. [23, стр. 41-43]. Для любых формул A, B следующие формулы являются теоремами:
(a) ØØBÉB;
(b) BÉØØB;
(c) ØAÉ(AÉB);
(d) (ØBÉØA)É(AÉB);
(e) (AÉB)É(ØBÉØA);
(f) AÉ(ØBÉØ(AÉB));
(g) (AÉB)É((ØAÉB)ÉB).
Доказательство.
(a) |―ØØBÉB.
1. (ØBÉØØB)É((ØBÉØB)ÉB) схема аксиом A3
2. ØBÉØB пример 5.3
3. (ØBÉØØB)ÉB 1, 2 и следствие (2) из леммы 5.1
4. ØØBÉ(ØBÉØØB) схема аксиом А1
5. ØØBÉB 3, 4 и следствие (1) из леммы 5.1
(b) |―BÉØØB.
1. (ØØØBÉØB)É((ØØØBÉB)ÉØØB) схема аксиом A3
2. ØØØBÉØB пункт (a), доказанный выше
3. (ØØØBÉB)ÉØØB modus ponens из (1) и (2)
4. BÉ(ØØØBÉB) схема аксиом А1
5. BÉØØB 3, 4 и следствие (1) из леммы 5.1
(с) |―ØAÉ(AÉB).
1. ØA гипотеза
2. A гипотеза
3. AÉ(ØBÉA) схема аксиом А1
4. ØAÉ(ØBÉØA) схема аксиом А1
5. ØBÉA 2, 3, modus ponens
6. ØBÉØA 1, 4, modus ponens
7. (ØBÉØA)É((ØBÉA)ÉB) схема аксиом А3
8. (ØBÉA)ÉB 6, 7, modus ponens
9. B 5, 8, modus ponens
Итак, в силу 1-9, ØA,A|― B. Поэтому по теореме дедукции, ØA,|― AÉB и, снова по той же теореме, |― ØAÉ(AÉB).
(d) |― (ØBÉØA)É(AÉB).
1. ØBÉØA гипотеза
2. A гипотеза
3. (ØBÉØA)É((ØBÉA)ÉB) схема аксиом А3
4. AÉ(ØBÉA) схема аксиом A1
5. (ØBÉA)ÉB 1, 3, modus ponens
6. AÉB 4, 5, следствие (1) из леммы 5.1
7. B 2, 6, modus ponens
В силу 1-7, ØBÉØA, A |― B, после чего, дважды применяя теорему дедукции, получим требуемый результат.
(е) |― (AÉB)É(ØBÉØA).
1. AÉB гипотеза
2. ØØAÉA пункт (a)
3. ØØAÉB 1, 2, следствие (1) из леммы 5.1
4. BÉØØB пункт (b)
5. ØØAÉØØB 3, 4, следствие (1) из леммы 5.1
6. (ØØAÉØØB)É(ØBÉØA) пункт (d)
7. ØBÉØA 5, 6, modus ponens
В силу 1-7, AÉB |― ØBÉØA, откуда (e) получаем по теореме дедукции.
(f) |― AÉ(ØBÉØ(AÉB)).
Очевидно, A, AÉB |― B. Применив дважды теорему дедукции, получаем |― AÉ((AÉB)ÉB). По пункту (e) имеем |―((AÉB)ÉB)É (ØBÉØ(AÉB)). Наконец, применив следствие (1) из леммы 5.1, получаем |―(AÉB)É(ØBÉØA).
(g) |―(AÉB)É((ØAÉB)ÉB).
1. AÉB гипотеза
2. ØAÉB гипотеза
3. (AÉB)É(ØBÉØA) пункт (e)
4. ØBÉØA 1, 3, modus ponens
5. (ØAÉB)É(ØBÉØØA) пункт (e)
6. ØBÉØØA 2, 5, modus ponens
7. (ØBÉØØA)É((ØBÉØA)ÉB) схема аксиом А3
8. (ØBÉØA)ÉB 6, 7, modus ponens
9. B 4, 8, modus ponens
Итак, AÉB, ØAÉB|― B. Применив два раза теорему дедукции, получаем (g).
Лемма 5.3.Если G, A |― B и G, ØA |―B, то G |― B.
Доказательство. По лемме 5.2(g) формула (AÉB)É((ØAÉB)ÉB) является теоремой. Таким образом, G |―(AÉB)É((ØAÉB)ÉB). Кроме того, по теореме о дедукции G|― AÉ B и G|―ØAÉB. Теперь дважды воспользуемся теоремой 5.1.
Лемма 5.4.[23, стр. 43]Пусть A с высказывательными переменными X1, X2,..., Xm и пусть задано некоторое распределение истинностных значений для X1, X2,..., Xm. Пусть тогда X'i есть Xi, если Xi принимает значение И, и Ø Xi, если Xi принимает значение Л, и пусть, наконец, A' есть A, если при этом распределении A принимает значение И, и ØA, если A принимает значение Л. Тогда X'1, X'2,..., X'm|―A'.
Если, например, A обозначает Ø(ØX1 É X2), то для каждой строки истинностной таблицы
| X1 | X2 | Ø(ØX1 É X2) |
| И | И | Л |
| Л | И | Л |
| И | Л | Л |
| Л | Л | И |
лемма 5.3. утверждает факт соответствующей выводимости. Так, в частности, третьей строке соответствует утверждение X1, ØX2 |― ØØ(ØX1 É X2), а четвертой строке ØX1, ØX2 |― Ø(ØX1 É X2).
Доказательство. Проведем доказательство с помощью математической индукции по числу n вхождений в A логических связок.
Базис индукции. Если n=0, то A представляет из себя просто высказывательную переменную X1, и утверждение леммы сводится к X1|―X1 и ØX1 |― ØX1.
Индуктивный переход. Допустим теперь, что лемма верна при любом j<n.
Случай 1. A имеет вид отрицания: ØB. Число вхождений логических связок в B, очевидно, меньше n.
Случай 1a. Пусть при заданном распределении истинностных значений B принимает значение И. Тогда A принимает значение Л. Таким образом, B' есть B, а A' есть ØA. По индуктивному предположению, примененному к B, мы имеем X'1, X'2,..., X'm|―B. Следовательно, по лемме 5.2(b) и modus ponens, X'1, X'2,..., X'm|―ØØB. Но ØØB и есть A'.
Случай 1b. Пусть B принимает значение Л; тогда B' есть не ØB, а A' совпадает с A. По индуктивному предположению, X'1, X'2,..., X'm|―ØB, что и требовалось получить, ибо ØB есть A'.
Случай 2. Формула A имеет вид BÉC. Тогда число вхождений логических связок в В и С меньше, чем в А. Поэтому, в силу индуктивного предположения, X'1,X'2,..., X'm|―B', X'1, X'2,..., X'm|―C'.
Случай 2a. Формула B принимает значение Л. Тогда A принимает значение И, и B' есть ØB, а A' есть A. Таким образом, X'1,X'2,..., X'm|―ØB и, по лемме 5.2 (с), X'1,X'2,..., X'm|―BÉC, но BÉC и есть A.
Случай 2b. Формула C принимает значение И. Следовательно, A принимает значение И и C' есть C, а A' есть A. Имеем X'1,X'2,..., X'm|―С, и тогда, по схеме аксиом А1, X'1,X'2,..., X'm|―BÉC, где BÉC совпадает с A.
Случай 2c. Формула B принимает значение И и C принимает значение Л. Тогда A' есть ØA, ибо A принимает значение Л, B' есть B и C' есть ØC. Имеем X'1,X'2,..., X'm|―B и X'1,X'2,..., X'm|―ØC. Отсюда, по лемме 5.2 (f) получаем X'1,X'2,..., X'm|―Ø(BÉC), где Ø(BÉC) есть A'.
Теорема 5.3. (Пост, 1921) Формула A в исчислении высказываний является теоремой тогда и только тогда, когда A - тавтология.
Доказательство. Нам осталось доказать только половину теоремы, другая половина доказана в теореме 5.2. Итак пусть A есть тавтология, докажем, что она доказуема. Предположим, что X1, X2,..., Xm - все высказывательные переменные, содержащиеся в A. При каждом распределении истинностных значений для переменных X1, X2,..., Xm мы имеем, в силу леммы 5.4, X'1, X'2,..., X'm|―A (A' совпадает с A, так как A есть тавтология). Поэтому в случае, когда Xm принимает значение И, мы применив лемму 5.4, получаем X'1, X'2,..., Xm|―A; когда же Xm принимает значение Л, то по той же лемме получаем X'1, X'2,..., ØXm|―A. Отсюда, по лемме 5.3, X'1, X'2,..., Xm-1|― A. Точно таким же образом, рассмотрев два случая, когда Xm-1 принимает значение И и Л, и снова применив леммы 5.4 и 5.3, мы исключим Xm-1 и так далее; после m таких шагов мы придем к |―A.
Исчисление высказываний можно описать системами аксиом, отличными от A1, A2 и A3. Например, если использовать штрих Шеффера x|y = Ø(x&y), то достаточно одной схемы аксиом
((P|(Q|R))|(S|(S|S)))|(T|Q)|((P|T)|(P|T)))
и единственного правила вывода "из A и A|(B|C) следует C".