ГЛАВА VII. РЕКУРСИВНЫЕ ОПРЕДЕЛЕНИЯ

§ 1. Некоторые пояснения принципиального характера

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

В системе (В) нашли свою формализацию все пять аксиом арифметики Пеано. Именно, две из них были формализованы введением символа и символа штриха, две другие — выводимостью формул наконец, аксиома полной индукции — введением формальной аксиомы индукции.

Поэтому можно было бы думать, что в теоремах, доказанных нами относительно системы (В), вопросы непротиво речивости и полноты арифметики нашли свое окончательное решение.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Выражения и в случае рекурсии для сумйы имеют вид

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

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

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

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

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

вводится рекурсивными равенствами

и возьмем в качестве цифру Тогда речь будет идти о том, чтобы вывести некоторое равенство вида

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

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

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

Первая из них вместе с рекурсивным равенством

дает формулу

которая в сочетании с

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

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

А эта формула в сочетании с формулой

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

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

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

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

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

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

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

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

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

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

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

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

а тем самым и

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

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

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

коль скоро

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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