Теорема дедукции. 
Дискретный анализ. 
Формальные системы и алгоритмы

Доказательства выводимости сильно упрощает следующая теорема.

Теорема 1.22 (теорема дедукции). Для произвольного лтожества формул Г и произвольных формул А, В выводимость Г U {Л} h В равносильна выводгхмости Г b А-+В.

Поскольку эта теорема очень важна для дальнейшего, приведём более развернутую формулировку: формула В выводима из множества гипотез Ги {Л} тогда и только тогда, когда формула А—ьВ выводима из множества гипотез Г.

Доказательство. В одну сторону теорема дедукции очевидна: если существует вывод формулы А—>В из множества формул Г, то после добавления к этому выводу формул Л.

В

(гипотеза) (МР из Л, Л->?).

получаем вывод формулы В из множества формул Г U {Л}.

В другую сторону будем доказывать индукцией по длине вывода. Пусть имеется вывод длины п формулы В из множества формул Г U {Л}: В, …, В_п = В.

Для первой формулы в выводе есть три возможности:

• • В является аксиомой;
• • В принадлежит множеству Г;
• • В] = А.

В первых двух случаях для построения вывода Л—>В из множества Г используем лемму 1.15. В третьем случае нужно построить вывод формулы Л—>А, что сделано в лемме 1.13. База индукции доказана.

Предположим, что построен вывод В' = (В[,…, B'_N) формул Л—?В 1, Л—>В<2, …, А—>Вк из множества формул Г. Для формулы Bk₊1 есть четыре возможности. Первые три из совпадают с описанными выше для формулы В. В этих случаях мы поступаем так же, как и в случае В. Остаётся рассмотреть лишь применение правила вывода. Тогда Bj = = Bi~>Bk+1, i, j < к + 1. Добавим к выводу В' следующие формулы:

Здесь через N' обозначен номер формулы Л—>(Д —>Д_:+1) = = Л—в выводе В', а через N" — номер формулы Лн>Д в том же выводе. Теперь получен вывод В" формул А—

A—«j??2i • • • 1 A—>Bk+i- Шаг индукции доказан, что завершает доказательство теоремы. ?

Приведём примеры использования теоремы дедукции.

Лемма 1.23 (транзитивность). {А—>В, В—>С} I- А—>С.

Доказательство. Построим вывод {Л, А^В, ??—"С} Ь С

• 1. Л (гипотеза)
• 2. Л—(гипотеза)
• 3. В (МР 1,2)
• 4. В—(гипотеза)
• 5. С (МР 3,4)

и применим теорему дедукции. ?

Лемма 1.24 (снятие двойного отрицания). Доказательство. Для (а) построим вывод 11Л IЛ.

и применим теорем}' дедукции.

и применяем теорему дедукции. ?

Лемма 1.25 (принцип контрапозиции).

Доказательство. Для (а) построим вывод А, 113—>1/1 Ь В

и дважды применяем теорему дедукции.

Для (б) поступаем аналогично. Строим вывод формулы 1А из формул А—1В

и дважды применяем теорему дедукции. ?

Лемма 1.26. Если 1Т А, ЛТ — 1 А, гпо Ь Т.

Доказательство. По теореме дедукции выводимы формулы 1Т—>Л, ЛТ—?~А. Вывод Т получается добавлением к их выводам аксиомы (ЛТ—>ЛА) —>((ТГ—>А)—>Т), за которой следует два применения modus ponens. ?

Задачи.

• 1.11. Докажите, что в исчислении высказываний Ла YЬ.
• 1.12. Пусть для любой формулы В в исчислении высказываний выполнено В ~ А. Докажите, что формула А — тавтология.
• 1.13. Пусть для любой формулы В в исчислении высказываний выполнено А Ь В. Верно ли, что формула А невыполнима?
• 1.14. Для формул А, В исчисления высказываний выполняются условия А Ь В и В h ЛА. Докажите, что 1А тавтология.