Теорема дедукции

Теорема дедукции

§ 1. Формулировка теоремы и некоторые следствия

Теорема (дедукции). Если

j1, j2, …, jn, j ├ ψ,

то

j1, j2, …, jn├ (j → ψ).

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

j1, j2, …, jn−1├ (jn → (j → ψ));

…

├ (j1 → … → (jn−1 → (jn → (j → ψ)))…).

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

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

j1, j2, …, jn├ (j → ψ),

то

j1, j2, …, jn, j ├ ψ.

Для доказательства предположим, что

v1

v2

… (1)

vN = (j → ψ)

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

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

v1

v2

… (2)

vN = (j → ψ)

j

ψ

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

§ 2. Леммы к теореме дедукции

Лемма 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).

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

Лемма доказана.

Лемма 2. Если

j1, j2, …, jn├ (j → ψ)

и

j1, j2, …, jn├ (j → (ψ → χ)),

то

j1, j2, …, jn├ (j → χ)

(своеобразный modus ponens!).

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

− это аксиома № 2 и, следовательно, выводимая в ИВ формула;

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

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

(j → χ)

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

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

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

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

1) формула ψ выводима в ИВ;

2а) ψ совпадает с одной из гипотез j1, j2, …, jn;

2б ψ = j.

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

(ψ → (j → ψ))

ψ

(j → ψ)

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

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

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

§ 4. Доказательство теоремы дедукции в общем случае

Пусть

v1

v2

…

vN = ψ

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

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

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

j1, j2, …, jn├ (j → vi)

и

j1, j2, …, jn├ (j → (vi → ψ)).

Но тогда по лемме 2

j1, j2, …, jn├ (j → ψ),

QED.

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