Гильберт, Бернайс - Основания математики. Логические исчисления и формализация арифметики (947375), страница 73
Текст из файла (страница 73)
Здесь снова а (а) и Ь (а, и, т) — термы, независимые от вводимого функционального знака, и наши обозначения снова следует понимать в том смысле, что в а (а) нв должны встречаться никакив переменные, кроме а, а в Ь (а, и, т) — никакие переменные, кроме а, и и т, причем некоторые иэ этих переменных, вообще говоря, могут и отсутствовать. В рекурсии для ( (а, и) переменная и является в ы д е л е ны о й в этой рекурсии, в то время как а выступает в ней только в ролип а р а м е т р а.
Если вместо одного параметра мы допустим в рекурсии большее их количество, то у нас получится схема рекурсии для функции )(а, „)а, и) с более чем двумя аргументами: ( (а, ..., Й, О) = а (а, ..., Й), ) (а, ..., гс, и') = Ь (а, ..., га, и, ( (а, ..., й, и)). Из соглашений, касающихся схемы рекурсии, в частности, вытекает, что в каждом рекурсивном равенстве в правой части должны встречаться только такие переменные, которые являются аргументами в левой его части; однако ые обяаатвльно, чтобы все стоящие слева аргументы встречались также и справа. Рекурсивные равенства для суммы а + Ь и произведения а Ь получаются в качестве частных случаев схемы рекурсии для функционального знака с двумя аргументами, с тем лишь несущественным различием, что вместо стоящих перед аргументами греческих букв мы пользуемся здесь общеупотребительным способом записи.
Выражения а (а) н Ь (а, и, т) в случае рекурсии для суммы имеют вид а и т', а в случае рекурсии для произведения — вид О ит+а. Мы видим, что очередность рекурсий для суммы и проиаведения должна быть выбрана таким образом, чтобы рекурсия для суммы производилась ранее; тогда в рекурсии для произведения терм т + а будет удовлетворять условию независимости его от вводимого функционального знака.
Формализация иытуитивной процедуры рекурсивного определения с помощью схемы рекурсии основывается на том, что при рекурсивном введении функционального анака ( (а,..., ес, и) мы для каждой цифры Ь получаем некоторое раеенсигео )(а, ...,)с, Ь)=~(а, ...,й), выводимое с помощью рекурсивных равенств и аксиом равенства (здесь | (а,..., й) представляет собой терм, независимый от фуыкционального знака ( ( )) Рассмотрим этот вопрос для случая функционального энака с двумя аргументами. Допустим, что функциональный знак гр (а, и) 23 д.
Рилъаерт, и. Бернааа сгл. Рп РЕКУРСИВНЫЕ ОПРЕДЕЛЕНИЯ 354 1 0 некОтОРые пояснения пРинципиАльного ХАРАктеРА 355 вводится рекурсивными равенствами ф (а, 0) = а (а), ф (а, и') = Ь (а, и, ф (а, и)), и возьмем в качестве 3 цифру 0". Тогда речь будет идти о том, чтобы вывести некоторое равенство вида ф (а, 0 ) = 1 (а), в котором 1 (а) — какой-то терм, не зависящий от функционального знака ф (, ). С этой целью во второе из рассматриваемых рекур- сивных равенств мы вместо переменной и подставим по очереди 0 и 0'. Тогда мы получим формулы ф(а, 0') =Ь(а, О, ф(а, 0)), ф (а, 0") = Ь (а, 0', ф (а, 0')). Теперь, с помощью аксиом равенства, мы можем вывести формулу г = г — ~- Ь (а, с, г) = Ь (а, с, з).
Эту формулу мы используем для двух различных подстановокс один раз мы подставим ф (а, 0) вместо г, а (а) вместо э и О вместо с, а второй раз подставим ф (а, 0') вместо г, Ь (а, О, а (а)) вместо з и 0' вместо с. В результате получатся следующие две формулы: ф (а, 0) = и (а) з- Ь (а, О, ф (а, 0)) = Ь (а, О, а (а)), ф(а, 0')=Ь(а, О, а(а))-РЬ(а, 0', ф(а, 0'))=Ь(а, О, Ь(а, О, а(а))). Первая из них вместе с рекурсивным равенством ф (а, 0) = а (а) дает формулу Ь(а, О, ф(а, 0))=Ь(а, О, а(а)), которая в сочетании с ф (а, 0') = Ь (а, О, ф (а, 0)) и с использованием второй аксиомы равенства дает формулу ср (а, 0') = Ь (а, О, а (а)).
Если мы возьмем эту формулу вместе со второй иэ двух полученных выше формул, то по схеме заключения получим Ь(а, 0', ф(а, 0'))=Ь(а, 0', Ь(а, О, а(а))). А эта формула в сочетании с формулой ф (а, 0") = Ь (а, 0', ф (а, 0')), ранее полученной нами иэ второго рекурсивного равенства, позволяет с использованием аксиомы (у ) получить ф(а, 0")=Ь(а, 0', Ь(а, О, а(а))),~ что и дает искомое равенство, в правой части которого стоит независимый от функционального знака ф (., ) терм, не содержащий никаких переменных, кроме а..
Пользуясь этим способом, мы, например, смоясем для любой цифры 3 с помощью рекурсивных равенств для суммы и аксиом равенства вывести равенство а+3=а(1). Аналогично, для любой отличной от нуля цифры 3' с помощью рекурсивных равенств для произведения можно будет вывести равенство а Ь'=т(а), где т (а) означает выражение, которое получается изпеременной а в результате 3-кратного приписывания вырансения +а (с заклю- чением в скобки результата каждого такого приписывания). Вообще, этот способ позволяет для любого рекурсивно вве- денного функционального знака ) (...) и для любой заданной цифры 3, подставляемой вместо выделенной в данной рекурсии.
переменной, вывести некоторое равенство ((а, ..., Й, 3)=1, где стоящий в правой части терм не зависит от функционального знака ((...) и не содержит никаких отличных от а, ..., сс переменных. Если мы подставимвзторавенствовместопараметрова,..., а некоторые цифры а,..., р, то получим равенство )(а, ..., с, 3)=с, в правой части которого стоит терм без переменных, который тоже не зависит от функционального знака ( (...) и у которого аргу- ментами самых внутренних функциональных знаков являются цифры. Это выражение представляет собой как раз то, что мы полу- чаем при обычном способе вычисления вначения ( (а,..., Р, 3), когда функциональный знак ) (...) исключается нами путем повторного применения описывающих его рекурсивных равенств.
Если с — цифра, то вывод равенства 1(а, ..., с, 3)=с дает нам полную формализацию вычисления значения выражения 1( а,..., с, 3). Мы теперь покажем, что и в том случае, когда с еще содержит рекурсивно вводимые функциональные знаки, гз» $ И некОГОРые пОяснеНия пРинципиАльнОГО хАРАктеРА 357 игл, чп РЕКУРСИВНЫЕ ОПРЕДЕЛЕНИЯ продоля«ение процесса вычисления тоже будет допускать формализацию, так что если ( представляет собой цифру, получающуюся в результате вычисления значения ((а, ..., Ь, Ь), то нам удастся получить вывод равенства ) (а, ..., Ь, Ь) = 1.
Для этого мы рассудим следующим образом. Допустим, что для'каждого введенного до ) (...) функционального знака при фиксации значений его аргументов цифрами удается вывести равенство, у которого в левой части стоит этот функциональный знак с цифрами в качестве аргументов, а в правой части — та цифра, которая получается в качестве значения функции в результате естественного процесса вычислеяий.
Тогда мы можем вывести равенство а тем самым и )(а, ...,1, Ь)=1. «В самом деле, вывод равенства с = 1 мы получим совершенно тем же способом, которым от выражения «мы переходим к его значению 1 при естественном процессе вычисления. Это делается таким образом, что вместо каждого самого внутреннего функционального знака мы подставляем его значение, которое является цифрой, затем с получившимся выражением поступаем точно таким же образом, исключая шаг за шагом все функциональные знаии. Этот процесс всегда завершается, так как в выражении с имеется лишь конечное число вложенных друг в друга функциональных знаков.
Это исключение функциональных знаков из выражения «мы можем полностью промоделировать в нашем дедуктивном формализме. Действительно, каждый иэ фигурирующих в этой процедуре функциональных знаков вводится ранее функциональногп знака ) (... ); поэтому, если а (ш,..., Г) — один из этих фунициональных знаков с цифрами в качестве аргументов, а а — его значение, то согласно нашему предположению выводимо равенство о(ш, ..., Г)=а, и чтобы:испольэовать это равенство для замены выражения б (а,..., Г) цифрой а, нам недостает лишь формализации принципа замены равного равным. Но эта последняя может быть полу- 11 11 чена с помощью аксиом равенства.
Как было замечено в гл. У ), с помощью аксиом равенства можно для каждого (построенного нз функциональных знаков, переменных н цифр) терма «(с) вывести формулу а = Ь -Р1 (а) = «(Ь), 1) См. с. 2ЗЗ. а тем самым и получить равенство ~( )=«(Ь), коль скоро а = Ь. Таким образом, вывод равенства )(а, ..., У, Ь)=1, если он еще не был получен прямо с помощью рекурсивных равенств для ((...), сводится посредством однозначно описанной процедуры к выводу конечного числа конкретных равенств вида б(ш ' Г)=2 где б — некоторый функциональный знак, рекурсивно введенный ранее ) (...), а а — значение выражения 8 (ш,..., Г) с цифрами ш,..., т в качестве аргументов, получающееся в результате соответствующего рекурсивного вычисления.
Эта процедура сведения может быть повторена необходимое количество раз, и тогда не позже, чем после ц-кратного ее применения, где ц есть число функциональных знаков, рекурсивно введенных ранее ) (...), Мы получим вывод равенства ((а, ..., Ь, Ь) =Х. Итак, применяемый в финитной арифметике метод рекурсивных вычислений можно полностью промоделировать в нашем формализме, надлея.ащим образом испольауя в процессе дедукции рекурсивные равенства. Принимая во внимание это положение вещей, мы будем считать оправданной такую терминологию, когда введение какого-либо функционального знака при помощи рекурсивных равенств мы будем называть рекурсивным определением и будем говорить о «функцииэ, определенной с помощью рекурсии.
Однако мы должны отчетливо понимать то обстоятельство, что речь при этом идет не об определении в смысле простого разъяснения знаков, т. е. не о введении символа, служащего сокращением для составного выражения. Определение в таком более узком смысле слова мы будем называть явным определением.