3. Невозможность вывода непротиворечивости рекурсивных определений в качестве следствия непротиворечивости систем предыдущих аксиом

Заменимость арифметических аксиом явными

определениями; явное определение символа при помощи соответствующей рекурсивной функции; вывод основных свойств символа С.

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

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

и

а кроме них, — еще две формулы

и

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

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

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

Если мы теперь добавим к этой системе аксиом рекурсивные равенства

то система перестанет быть непротиворечивой. Именно, второе из этих равенств при подстановке вместо даст

а из аксиомы

мы путем подстановки получим

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

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

Эта формула вместе с

и

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

в то время как среди наших аксиом имеется формула

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

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

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

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

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

Вывод формулы

получается введением рекурсивных равенств

Действительно, вторая из этих формул в результате подстановки дает

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

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

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

Получающаяся отсюда путем контрапозиции формула

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

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

Для вывода формулы

мы возьмем уже приводившиеся выше рекурсивные равенства

Второе из них при помощи подстановки дает формулы

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

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

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

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

Но эта формула получается путем контрапозиции из формулы

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

выводимой с помощью аксиом равенства.

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

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

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

А затем явно определим формулу а при помощи эквивалентности

Используя эту эквивалентность, формулы

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

А эти последние можно будет вывести с использованием схемы индукции.

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

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

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

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

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

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

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

и

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

Теперь, исходя из этого специального, полученного индукцией по равенства

при помощи схемы индукции и аксиомы равенства можно будет вывести формулы

В то же самое время, используя формулу мы можем получить формулу

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

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

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

Нам остается вывести формулу Для зтого рассмотрим два случая: и . С формальной точки зрения это означает, что формулу мы получим

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

и

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

А эта формула получается контрапозицией из формулы

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

с использованием аксиомы равенства.

Для вывода второй формулы

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

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

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

и формулы

которую мы по правилу силлогизма получим из формул

и

Первая из этих формул получается в результате подстановки

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

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

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

мы получим вспомогательную формулу

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

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

Сначала выведем формулу

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

Следовательно, выводима формула Если мы сможем вывести еще и то с помощью схемы индукции получим искомую формулу

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

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

Для вывода формулы

т. е. (после соединения посылок)

мы сначала с помощью формул

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

Легко показать, что нам остается вывести формулу

Для вывода этой формулы мы используем следующие две формулы:

и

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

а вторая — с помощью формулы

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

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

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

а отсюда, ввиду того, что формулу

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

а эта последняя по определению выражения переводится в формулу

Следует, впрочем, отметить, что из формулы с помощью формул

разбором случаев и без труда получается формула

Выводя нашу формулу мы попутно получили и формулу

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

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

а с другой стороны, дает формулу

Из выведенных формул и только что упомянутой формулы

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

как это было установлено в гл. VI.

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

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

При этом подходе арифметические аксиомы, касающиеся штрих-функции и предиката заменяются рекурсивными равенствами, к которым дополнительно присоединяется нумерическая формула