§ 6. Добавление: распространение теоремы о возможности замены аксиомы равенства (J2) в случае добавления i-правила

Здесь мы покажем, что доказанная в гл. VII теорема о возможности замены аксиомы равенства или соответственно схемы равенства

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

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

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

1. Формулы

2. Формулы вида

3. Формулы вида

где обозначают предикатный символ и функциональный знак с аргументом а и, быть может, какими-нибудь другими аргументами.

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

С учетом этого обстоятельства мы докажем наше утверждение в несколько уточненной формулировке: Если a и b — термы, а формулы, то формула

может быть выведена из аксиом при помощи средств исчисления предикатов и -правила.

Это утверждение может быть доказано следующим образом. Прослеживая построение формул, — аналогично тому, как это делалось в уже упоминавшемся рассуждении из гл. мы сначала убеждаемся в том, что формула

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

где и суть термы, которые входят в или соответственно в в качестве внешних -термов (в отличие от вложенных в другие -термы). Наше предположение о том, что являются формулами, включает в себя допущение, что входящие в -термы [в частности, стало быть, и термы вводятся по -правилу при помощи соответствующих формул единственности. Разумеется, здесь вместо может фигурировать и какая-нибудь другая связанная переменная.

Теперь каждую из формул

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

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

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

к формуле

С другой стороны, применив формулы

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

а эта последняя, вместе с предыдущей формулой, по правилу силлогизма даст нам формулу

Таким образом, в итоге получается, что при помощи средств исчисления предикатов, -правила и формул формула

может быть выведена из формул вида

у которых число входящих в них -символов меньше, чем у формулы

Повторное применение этой процедуры в конце концов сводит вывод формулы

к выводам таких формул

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

Тем самым для вывода формулы

оказывается достаточно средств исчисления предикатов, i-правила и формул что и требовалось доказать.