3. Переход к аксиомам без связанных переменных с усилением экзистенциальных аксиом; символ 0; цифры в новом смысле; аксиомы, Пеано; получившаяся система аксиом.

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

Кроме того, немного упростим последнюю формулу. Из этой формулы в результате подстановки вместо с, перестановки членов конъюнкции и применения правила разъединения посылок мы получим

а отсюда — поскольку получается подстановкой из мы получим

С другой стороны, из этой формулы можно снова получить последнюю формулу нашей системы; действительно, из аксиом равенства, как было показано ранее. выводима формула 4)):

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

которая вместе с формулой

по правилу силлогизма дает формулу

Таким образом, в силу аксиом равенства эта формула оказывается равнозначной формуле

Теперь связанные переменные остаются только в двух формулах:

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

мы осуществим, взяв вместо нее формулу

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

мы введем индивидный символ 0. Теперь вместо формулы мы сначала возьмем формулу

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

дедуктивно равна формуле

Итак, теперь вместо двух рассматриваемых формул

у нас будут иметься формулы

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

Итак, все связанные переменные теперь удалены, и мы пришли к системе, состоящей из следующих пяти формул:

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

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

а исходя из символа выражения такие, как

В соответствии с нашими соглашениями все эти выражения являются термами, т. е. мы будем допускать подстановку их вместо свободных индивидных переменных.

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

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

Конечно, это преимущество было бы достигнуто и в том случае, если бы мы стали использовать знаки

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

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

Две последние формулы

и

соответствуют двум аксиомам из числа тех пяти, с помощью которых Пеано дал свою характеризацию натурального ряда 2). Свои аксиомы Пеано изобразил с помощью логической символики; одна из них является формулировкой принципа полной индукции, который мы обсудим впоследствии 3). Остальные выглядят следующим образом:

Нуль есть число.

Если — число, то а также является числом.

Из следует

Для всякого

Заметим, что в этой системе аксиом понятие числа совпадает с понятием элемента индивидной области, так

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

Нуль есть число .

Если — число, то также является числом достигается уже в результате введения символов и штриха в сочетании с правилом подстановки вместо индивидных переменных. Две остальные аксиомы формализуются посредством наших формул

и

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

Импликация

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

Подытожим еще раз систему наших аксиом: