Замечания. 1. Применяя к утверждению теоремы снова несколько раз теорему де­дукции, можно, очевидно, получить новые следствия:

2. На время доказательства теоремы введём такую терминологию. Будем называть список гипотез j1, j2, …, jn коротким списком гипотез, а список j1, j2, …, jn, j – длин­ным списком.

3. Докажем сейчас, что верна теорема, обратная к теореме дедукции, а именно: если

− формативная последовательность, являющаяся формальным выводом формулы (j → ψ) из короткого списка гипотез (в силу принципа «обрубания хвостов» можно, как обычно, предполагать, что наша формула (j → ψ) является последним словом в последо­вательности (1)).

Последовательность (1) тем более можно рассматривать как формальный вывод из длинного списка гипотез (это вытекает из определения формального вывода из гипотез). Добавим в конец последовательности (1) ещё две формулы:

Новая последовательность (2) снова является формальным выводом из длинного списка гипотез. В самом деле, предпоследняя формула является гипотезою, а последнюю формулу ψ можно получить по правилу modus ponens из двух предыдущих. Как видно, формула ψ выводима из длинного списка, QED[1].

Лемма 1. Если j – выводимая формула ИВ, то результат S(j) применения к j од­новременной подстановки S также есть выводимая формула ИВ.

Доказательство. Пусть одновременная подстановка S заключается в том, что по­парно различные буквы a1, a2, …, ak одновременно заменяются в формуле j на формулы j1, j2, …, jk.

Возьмём множество всех тех и только тех букв, которые входят в запись хотя бы одной из формул j1, j2, …, jk. Их конечное число. Пусть это будут (попарно различные) буквы x1, x2, …, xn. Тогда можно записать: j1 = j1(x1, x2, …, xn), …, jk = jk(x1, x2, …, xn). Так как алфавит ИВ (точнее, множество символов переменных) бесконечен, то можно взять попарно различные буквы b1, b2, …, bn, каждая из которых не совпадает ни с одной из букв a1, a2, …, ak, x1, x2, …, xn и не входит в запись формулы j. А теперь произведём последовательно серию обычных (однократных) подстановок: сначала в формулу j вме­сто буквы a1 подставим формулу j1(b1, b2, …, bn), затем вместо a2 в новую формулу под­ставим j2(b1, b2, …, bn) и т. д.; вместо ak – jk(b1, b2, …, bn). Затем вместо букв b1, b2, …, bn последовательно подставим буквы x1, x2, …, xn. Легко видеть, что в конце мы получим S(j).

Осталось сослаться на доказанное ранее утверждение, что при применении (обыч­ной, однократной) подстановки к выводимой формуле получается выводимая формула (в ИВ).

Доказательство. Пусть (j → ψ) замыкает последовательность формул, являю­щуюся формальным выводом из гипотез j1, j2, …, jn, а формула (j → (ψ → χ)) замыкает другую последовательность формул, также являющуюся формальным выводом из данных гипотез. Приписав вторую последовательность впритык к первой, мы получим, очевидно, новый формальный вывод из данных гипотез. Добавим к этой последовательности ещё несколько формул:

− результат одновременной подстановки в предыдущую формулу: j вместо A, ψ вместо B, χ вместо C. Следовательно, по лемме 1 это будет абсолютно выводимая формула;

− результат применения правила modus ponens к предыдущей формуле и к формуле (j → (ψ → χ)), содержащейся в нашей последовательности;

− результат применения правила modus ponens к предыдущей формуле и к формуле (j → ψ), содержащейся в нашей последовательности.

Так как построенная нами длинная последовательность является, очевидно, фор­мальным выводом из гипотез j1, j2, …, jn, а формула (j → χ) в ней содержится, то лемма доказана.

§ 3. Доказательство теоремы дедукции в частных случаях

Докажем сейчас теорему дедукции в трёх важных частных случаях:

Впрочем, случаи 1) и 2а) можно объединить. Рассмотрим последовательность:

Утверждаю, что эта последовательность в случаях 1) и 2а) является формальным выводом из короткого списка гипотез (откуда вытекает утверждение теоремы).

В самом деле, первое слово есть аксиома № 1. Второе слово есть результат приме­нения одновременной подстановки в предыдущую формулу и, следовательно, выводимо в ИВ по лемме 1. Третье слово в случае 1) есть абсолютно выводимая формула, а в случае 2а) – гипотеза короткого списка. Наконец, последняя формула в нашей последовательно­сти есть результат применения правила modus ponens к двум предыдущим формулам.

В случае же 2б) надо вывести формулу (j → j) из короткого списка гипотез. Это делается с помощью подстановки в абсолютно выводимую формулу (A → A) (доказыва­лась в моём курсе ранее) вместо буквы A формулы j (и получается даже абсолютно выво­димая формула).

− формальный вывод из длинного списка гипотез. Будем доказывать теорему индукцией по N.

База индукции: N = 1. Наша последовательность состоит из одной формулы ψ. Но это означает, что ψ либо абсолютно выводима, либо совпадает с одной из гипотез длин­ного списка. В обоих этих случаях теорема уже доказана (§ 3).

Пусть теперь теорема доказана для всех формул ψ, входящих во всевозможные формальные выводы из длинного списка гипотез, имеющие длину меньшую, чем N, и до­кажем её для вышеприведённого вывода длины N. Рассмотрим последнюю формулу ψ. Если она абсолютно выводима или совпадает с одной из гипотез длинного списка, то опять-таки для этих частных случаев теорема уже доказана. Остаётся случай, когда ψ = = MP (vi, vj), i, j < N. Но тогда обязательно vj = (vi → ψ). Так как оба слова vi, vj входят в формальные выводы из длинного списка гипотез длины < N, то по индуктивному предпо­ложению

[1] Quod erat demonstrandum (лат.) – ‘что и требовалось доказать’.