2. Формальная реализация; возможность обобщения этого метода.

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

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

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

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

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

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

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

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

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

Вывод формулы может быть проведен индукцией по Формула переводима в

а эту последнюю можно получить из равенства

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

Для того чтобы получить формулу

мы сначала индукцией по а выведем формулу

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

причем переменная а в не входит.

Формулу , а тем самым и формулу

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

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

а для этого достаточно будет вывести формулу

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

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

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

то придем к формуле

Возьмем формулу

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

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

и

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

Объединив полученные нами формулы, мы придем к

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

Из нее мы получим также и формулу

Тем самым индукцией по а мы получаем формулу

т. е.

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

Теперь применим еще раз формулу

подставив на этот раз вместо Воспользовавшись снова формулами

и

мы получим формулу

Потом возьмем (см. с. 505) формулы

и

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

Воспользуемся, кроме того, формулой

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

получим формулу

Объединив эту формулу с полученной ранее, а также с формулой

мы придем к формуле

Опираясь на выводимую формулу

мы перейдем от этой формулы к формуле

из этой формулы мы сначала получим формулу

а отсюда, далее, получим

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

вывод которой мы и стремились получить.

После этого индукцией по может быть получена формула т. е. формула

Если мы теперь образуем терм

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

Опираясь на эту формулу и применяя к терму

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

Тем самым мы теперь близки к поставленной цели — нахождению терма для которого выводимы равенства

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

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

Кроме того, во втором равенстве вместо здесь можно написать Действительно, равенство

может быть выведено следующим образом.

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

и

Вторая из этих формул дает нам, далее,

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

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

и тогда получится

Таким образом, мы пришли к равенствам

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

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

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

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

(здесь b и n являются выделенными переменными рекурсии, в то время как а выступает только в роли параметра) могут быть разрешены при помощи некоторого терма для которого в удается вывести равенства

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

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