5. Формулировка теоремы об устранимости; переводимость всякой формулы в ее редукцию; сравнение различных методов устранения.

В общем и целом, наши последние рассуждения приводят к следующему результату:

Будем исходить из некоторой формальной системы, состоящей из расширенного (при помощи аксиом равенства) исчисления предикатов, к которому могут быть добавлены какие-нибудь собственные аксиомы, а также, быть может, аксиома индукции (соответственно схема индукции). Если совокупность термов такой системы расширить путем соотнесения формулам -термов и если дополнительно принять в качестве аксиомы формулу или же добавить соответствующую схему формул, то это не расширит запаса выводимых формул, не содержащих -симво-лов. Или, как мы еще будем говорить: из вывода любой формулы, не содержащей -символов, -символы могут быть устранены. Ввиду сказанного выше, устранимость эта будет иметь место и для выводов, в которых -термы вводятся и используются в соответствии с нашим первоначальным -правилом, и для выводов, использующих обобщенное -правило.

Одновременно мы установили, что для всякой формулы, выводимой с использованием -правила, ее редукция выводима без использования -символов. В дополнение к сказанному мы покажем, что если допустить выводы с использованием -правила 2), то всякая формула будет переводима в свою редукцию. Мы докажем это индукцией по числу логических знаков в причем -символы также будем причислять к логическим знакам. Для случая, когда рассматриваемое число равно нулю, наше утверждение тривиально, так как тогда не содержит -символов и тем самым совпадает с Если составлена из каких-либо других формул с помощью связок логики высказываний, то это утверждение может быть получено средствами исчисления высказываний на основе нашего индукционного предположения. В том случае, когда имеет один из видов это утверждение совершенно аналогичным образом может быть получено средствами исчисления предикатов на основе имеющегося у нас индукционного предположения.

Остается рассмотреть случай, когда является элементарной формулой с внешними -термами

Редукция формулы в этом случае имеет вид

На основании сделанного нами индукционного предположения выводимы эквивалентности

(со свободными переменными ). Эти переменные мы выберем так, чтобы они не входили в формулу

Далее, для каждой формулы мы располагаем соответствующими формулами единственности, из которых при помощи -правила и аксиомы равенства могут быть выведены эквивалентности

Эти эквивалентности совместно с эквивалентностями, приведенными вьпйе, дают формулы

из которых, применив нужное число раз аксиому равенства мы получим импликацию

а отсюда с помощью исчисления предикатов — формулу

т.е. формулу

С другой стороны, импликация получается следующим образом. Мы исходим из импликации

выводимой средствами исчисления предикатов. Посылка этой импликации представляет собой формулу Если вместо переменных подставить -термы то на месте члена получится формула Таким образом, мы получим формулу

Но формулы выводимы с помощью -правила, и, следовательно, формулы

являются выводимыми (даже без использования -символов). Следовательно, средствами исчисления высказываний получается формула Из выведенных таким образом импликаций мы получим эквивалентность

Таким образом, опираясь на индукционное предположение, мы установили, что эта эквивалентность выводима во всех подлежащих разбору случаях.

Замечание. В первом издании этой книги доказательство устранимости -символов было проведено прямо для первоначального -правила, причем было показано, что всегда может быть устранено последнее введение -терма.

Индукция такого рода оказалась, однако, чрезвычайно утомительной. Курт Шютте привел существенно более простое доказательство, в котором за основу берется то же самое первоначальное -правило, но индукция ведется таким образом, что уменьшается максимальная «степень» -выражения, причем под степенью выражения понимается число встречающихся в нем -символов. Вместе с тем доказательство Шютте дает более сильный результат, так как оно относится и к таким формальным системам, в которых имеются свободные и связанные функциональные, а также связанные формульные переменные и в которых 1-символ употребляется в сочетании с функциональными, а также с формульными переменными, так что формализованными оказываются также характеристики функций и предикатов.

По сравнению с методом, предложенным Шютте, примененный нами метод Россера — Хазенъегера допускает несколько более легкую проверку, поскольку главная часть рассуждения ограничивается в этом случае рассмотрением одной-единственной схемы формул.