3. Обобщенная схема индукции; устранимость этой схемы.

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

а также схему еще более общего вида:

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

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

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

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

а из нее — формулу

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

Сперва рассмотрим схему

(в которой возможность наличия в t переменных указана теперь явным образом). Пусть функция вводится

следующей примитивной рекурсией:

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

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

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

которая вместе с

дает формулу

получим

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

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

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

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

Таким образом, нами получена формула т. е.

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

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

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

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

и, в частности, формулу

а также получим переход

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

Участвующие в этой схеме термы в которые, как мы знаем, могут входить переменные a и b, запишем более развернуто в виде

Пусть функция определяется следующей примитивной рекурсией:

Отсюда обычной индукцией по получим

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

Эти формулы вместе с ((3)) (где вместо подставлено ) дают

Применив вторую посылку рассматриваемой нами схемы

(в которую вместо b подставим с), мы получим

а значит, и

откуда по схеме следует

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

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

Но из двух формул

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

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

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

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

В дальнейшем мы будем записывать эти термы более развернуто в виде . (Согласно нашему предположению, не содержит переменной )

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

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

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

Отметим также формулу

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

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

Определим теперь функцию посредством примитивной рекурсии

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

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

Формула на основании определений переводима в формулу

а затем в формулу

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

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

На основании неравенства

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

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

Это удается проделать следующим образом. На основании определения имеем

откуда с помощью можно получить

Тогда в силу имеем

Далее, определение дает нам

а значит, и

В силу имеем

Формулы вместе с третьей посылкой нашей схемы

дают

что и требовалось для завершения искомого сведения.

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

из рекурсивных равенств

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

Из первого рекурсивного равенства мы получаем

из второго —

а из третьего —

и отсюда, далее, —

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

Совершенно аналогично с помощью схемы перекрестной индукции может быть получено неравенство

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

а тем самым и

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

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