2. Применение к системам (А), (В) и (Z).

У некоторых систем аксиом те или иные представляющие формулы оказываются излишними. Рассмотрим с этой точки зрения системы Система (А), правда, непосредственно не попадает в сферу действия нашей общей теоремы, так как формула в ней среди аксиом не встречается. Тем не менее данное обстоятельство не препятствует применению этой теоремы, так как в системе (А) аксиома может быть выведена из аксиом

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

или же формулу

так что каждая из этих двух формул вместе с может заменить в системе (А) аксиому

В самом деле, если мы в (А) заменим аксиомой и воспользуемся только что упоминавшимся выводом формулы то окажутся выводимыми формулы

Привлекая формулу

мы получим, с использованием аксиом формулы Из с помощью аксиомы мы получим, далее, формулу

и, с учетом , получим

Две последние формулы, в сочетании с формулой выводимой в (А) без использования дают формулу использованием

С другой стороны, если вместо добавить к системе (А) в качестве аксиомы формулу

то можно будет получить формулу

а из нее с помощью аксиомы можно будет снова получить формулу

В случае системы (В) мы вернемся к рассмотрению уже приводившегося хазенъегеровского вывода формулы . В этом выводе аксиома равенства используется только для вывода следующих трех формул:

Третья из них есть первая получается из в сочетании с формулой

а вторая получается из

в результате подстановки. Тем самым в хазенъегеровском выводе аксиома может быть заменена формулами

С другой стороны, располагая формулой

мы можем получить формулу

пользуясь схемой индукции и, кроме того, формулами а также формулой

(которая может быть получена из

Но, как было замечено выше, используя формулы и добавив к ним формулу можно вывести

Таким образом, в итоге получается, что в системе (В) аксиома может быть заменена формулами взятыми вместе с формулами

Здесь можно произвести еще одно упрощение, поскольку две последние формулы, с учетом наличия аксиомы делают ненужными аксиомы Итак, в конце концов вместо системы (В) получается следующая система аксиом:

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

Но последние четыре формулы с помощью формул и схемы индукции могут быть выведены из рекурсивных равенств для а

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

и аксиому

можно объединить в одну формулу

Если же мы, кроме того, заменим аксиому индукции равносильной ей схемой индукции, то получится система, состоящая из аксиом

и схемы индукции.

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

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