Доказательство. Теорема (дедукции). Если Г есть конечная совокупность формул, а А и В - произвольные формулы в ИВ, для которых Г,А ├ В

(1) Г, условие;…;

(2) А;

(3) ├ А ® (В ® А),

(4) В ® А, ПЗ(2,3).

Теорема (дедукции). Если Г есть конечная совокупность формул, а А и В - произвольные формулы в ИВ, для которых Г,А ├ В, то Г ├ А ® В.

Доказательство. Индукция по длине k вывода.

БАЗИС. k = 1. Возможны три случая.

1. В есть А. Тогда Г,А ├ А. Так как ├ А ® А (как то Г ├ A ® А.

2. ├ В. Тогда ├ А ® В по ПВЗ; поэтому Г ├ А ® В.

3. В Î Г. Тогда Г ├ В и по ПВЗ Г ├ А ® В.

ПРЕДПОЛОЖЕНИЕ ИНДУКЦИИ. Пусть теорема справедлива для всех выводов длины меньше k.

ШАГ ИНДУКЦИИ. Покажем, что теорема справедлива для выводов длины k. Пусть Г,А ├ В и пусть B₁,B₂,...,B_k-1,В_k (= В) есть вывод длины k формулы В из совокупности Г,А. Возможны следующие случаи.

1. В есть А. 2. ├ В. 3. В Î Г. Эти случаи рассмотрены в базисе.

4. В (= B_k ) получается из двух формул В_i и В_i ® В_k вывода по правилу заключения, т.е. вывод В_k из Г,А имеет вид

В₁;В₂;...;В_i;...;В_i ®В_k;...;В_k (=В).

Тогда Г,А ├ В_i, Г,A ├ В_i ® B_k. Так длины этих выводов меньше k, то по предположению индукции

(1) Г ├ А ® В_i;

(2) Г ├ А ® (В_i ® В_k).

Далее имеем:

(3) Г ├ (А ® (В_i ® В_k)) ® ((А ® В_i) ® (А ® В_k)),

(4) Г ├ (А ® В_i) ® (А ® В_k), П3(2,3);

(5) Г ├ А ® В_k, П3(1,4), т.е. Г ├ A ® В.

Следствие.

⊢ ⊢

⊢

Замечание. Теорема дедукции доказуема в любом аксиоматическом исчислении, содержащем аксиомы А1, А2, правило подстановки и правило заключения.