Теорема дедукции в УИП

Теорема (дедукции). Если формула В выводима в УИП из (конеч­ной) совокупности формул Г и формулы А, причем в этом выводе не затрагивается никакая свободная переменная формулы А, то формула А ® В выводима из Г.

Доказательство. Индукция по длине k вывода. Заметим, что по условию теоремы правила навешивания кванторов на свободные пере­менные формулы А не используются.

БАЗИС. k = 1. Возможны следующие случаи.

1. В есть А. Тогда ├ А ® А, поэтому Г ├ A ® А.

2. ├ В. Тогда ├ А ® В (ПВЗ). Поэтому Г├ A ® В.

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

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

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

1. В есть А. 2. ├ В. 3. В Î Г.

Эти случаи рассмотрены в базисе.

4. В (= В_k) получается из двух формул В_i и В_i ® В_k вывода по правилу заключения. Этот случай рассматривается аналогично дока­зательству теоремы дедукции в исчислении высказываний.

5. Пусть Г,А ├ В и В₁,В₂,...,В_i,...,В_k, где В_i = С ® D(x), B_k = В = С ® ("x)D(x), есть вывод длины k формулы В из Г,А. Причем В получено из В_i с помощью "-правила, при этом формула С не содер­жит х свободно. Формула А тоже не содержит х свободно, иначе сво­бодная переменная формулы А использовалась бы в выводе формулы В. Так как длина вывода B₁,В₂,...,В_i из Г,А меньше k, то по предпо­ложению индукции

(1) Г ├ А ® (С ® D(x)). Далее

(2) Г ├ А & С ® D(x), ПВ14(1), соединение посылок;

(3) Г├ А & С ® ("x)D(x), "-ПР(2);

(4) Г├ А ® (С ® ("x)D(x)), ПВ15(3), разъединение посылок,

т.е. Г ├ А ® В.

6. Пусть Г,А ├ В и В₁, В₂,...,В_i,...,В_k, где В_i = D(x) ® С,

B_k = В = ($x)D(x) ® С, есть вывод длины k формулы В из Г,А. Причем В получено из В_i с помощью $-правила, при этом формула С не содержит х свободно. Формула А тоже не содержит х свободно. Так как длина вывода В₁,В₂,...,B_i из Г,А меньше k, то по пред­положению индукции

(1) Г ├ A ® (D(x) ® С). Далее

(2) Г ├D(x) ® (А ® С), ПВ13(1), перестановка посылок;

(3) Г ├ ($х)В(х) ® (А ® С), $-ПР(2);

(4) Г ├ A ® (($x)D(x) ® С), ПВ13(2), перестановка посылок,
т.е. Г ├ А ® В. Теорема доказана.

Приведем несколько примеров доказуемых в УИП формул и неско­лько вспомогательных правил вывода.

Правило вывода 19. ("x)A(x) ├ A (x).