§ 5. Дополнительное рассмотрение аксиом равенства

1. Замена второй аксиомы равенства аксиомами более специального характера.

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

Мы постараемся проиллюстрировать эту мысль на примере первой из обсуждавшихся в гл. VI систем аксиом, которая кроме аксиом равенства содержит аксиомы Если из этой системы аксиом оказывается выведенной какая-либо формула, то, как мы знаем, из ее вывода можно исключить формульные переменные, сначала разложив этот вывод на нити, затем выполнив перенос подстановок вместо формульных переменных в исходные формулы и совершив произвольные подстановки вместо оставшихся формульных переменных. Тогда вместо формулы нас появятся исходные формулы вида

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

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

Факт этой выводимости вытекает из того, что:

1. Из формул как было показано ранее выводимы формулы

и

2. Из формулы для любого выводима формула

3. Из формулы

пользуясь формулой

можно вывести формулу

4. Если произвольная формула, то из формулы

средствами исчисления высказываний выводимы формулы

и

5. Из формулы

выводима формула

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

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

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

или

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

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

Так, в случае только что рассмотренной системы аксиом двум аргументам предикатного символа соответствуют две формулы а единственнному аргументу штрих-функции соответствует формула