§ 3. Сведение примитивных рекурсий к явным определениям посредством функции mxA(x) на основе аксиом системы (Z)

1. Эвристический подход.

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

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

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

и

Здесь в записи термов параметры можно всюду опустить, так что эти равенства могут быть записаны просто в виде

Сначала мы изложим основные идеи решения этой задачи. Мы будем следовать Дедекинду, который в своем сочинении «Was sind und was sollen die Zahlen?» впервые показал разрешимость рекурсивных равенств, рассматриваемых как определяющие равенства для вводимой в рассмотрение функции, не пользуясь наглядными соображениями. Его доказательство заключается в том, что сначала он показывает, что для каждого числа имеется функция обладающая тем свойством, что

и что для всякого числа

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

Отсюда следует, что функция

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

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

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

эквивалентно существованию такой -членной числовой последовательности

что и для каждого индекса выполняется соотношение

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

соответствует число

где представляет собой число 2, а суть первых нечетных простых чисел. Обратно, если мы будем исходить из числа

то соответствующая последовательность

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

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

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

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

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