Гильберт, Бернайс - Основания математики. Теория доказательств (947376), страница 103
Текст из файла (страница 103)
Тогда кванторов ликвидируем выделенную роль переменной этн схемы формул будут иметь вид УРЯ (Р) -«Я (1) и Я (1) -« =БАРЯ (Р), а модифицированные схемы (а) и (Р) запишутся в виде Я-«6(6) 6(6)-«Я и 1 Я-~ В(~) ~~в(у)-Я б " пе еменной 6 и для связанной переменной х причем для сво однои пер~же должно выполняться условие, что 6 не входит в дит в Е(6). Т т факт что правило переименования становится р п онзводы, вытекает из того, что ным, если за основу взять эти две схем, с помощью этих схем может быть вывед н е а любая,о,мула вида Чуй (х) -«ЧРЯ (з), Равно как и любая формула вида 34Я (Р) -« Э~Я (Р). ПРИЛЕ)ЯВН|4В П 476 пьнложеннв Например, для того чтобы вывести формулу Вхг)(х)- Ээу|(у), мы возьмем не входящую в 6(й) свободную иидивидную переменную с. Схема формул для квантора существования даст нам формулу И (с) -э =!ЭИ (р), а иэ этой последней по модифицированной схеме (р) мы получим формулу ВТИ(Т) ЪИ(р).
Таким образом, мы приходим к некоторой видоизмененной форме исчисления предикатов, где в качестве исходных формул мы допускаем: !) формулы, получающиеся в результате подстановки из тождественно истинных формул исчисления высказываний, 2) формулы, получающиеся из схем для кваиторов, 3) собственные аксиомы и формулы, получающиеся из схем аксиом. Переход от исходных формул или соответственно от ранее полученных формул к последующим формулам производится исключительно при помощи модифицированных схем (а), (р) и схемы заключения. Наконец, укажем на возможность произвести исключение (Ьормульных переменных с сохранением правила подстановки вместо свободных индивидных переменных, а танхсе правила переименования связанных переменных.
Тогда на месте исходных формул, содержащих связанные переменные, у нас появятся такие схемы формул, которые от соответствующих формул будут отличаться только тем, что эти формульные переменные будут заменены буквами, обозначающими формулы; так, в частности, вместо основных формул (а) и (Ь) у нас появятся схемы формул УхИ (х) -+-И (а) и И (а) ч- ВхИ (х), а вместо аксиомы равенства (|,) появится схема а Ь -~- (И (а) -~- И (Ь)). В остальном же первоначальный формализм останется без изме- нений. УТОЧНЕНИЕ ПОНЯТИЯ ВЪ|ЧИСЛИМОЙ ФУНКЦИИ И ТЕОРЕМА ЧЕРЧА О ПРОБЛЕМЕ РАЗРЕШИМОСТИ В !. Понятие регулярно внчнслнмой функции.
Вычисление в формализме (2ь) |~(п) ((Ч()(п) "" Ч (а))' при помощи которой исходная функция ((ам ..., и,) представляется в виде ((пм ..., и,) (ч(т!(с)(ам ..., и,)),' Рд (с) ... г!(с) могут быть определены посредТак как функции т|, т!,, ..., г! х ек сий, вычисление значений функции ( ством примитивных рекурси, ентов сводится к вычисдля заданной системы значений ее аргументов свод и об атно: вычисление пению некоторого значения функции,; р значений функции (ч сводится к вычислен ислению значений функции Ниже речь пойдет об уточнении понят ия вычислимой ариметической функции и, как следует из толь только что п оведенного с) См. ч, Ээв. Под а ифметической функцией мы понимаем функцию, облаа г ментов которой является натуральный ряд стью изменения аргументов к (мы считаем его начинающимся о кулис и в тоже являются натуральными.
ий с П и любом с -» 1 рассмотрение арифметических функц аргументов может быть сведен р р го При лю ом но к ассмот еиию функций одного г ента. Это делается при помощи введенной в гл. настоаргумента. щего тома~) рекурсивной функции т!" спм ..., пы и о р (с) ... (с) (а), устанавливающих ее рекурсивных функции т!, (и), ..., т!, „у взаимно однозначное соответствие м ду еж с-членными наборами чисел и самими этими числами.
Действительно, для лю о ункции с аргументов 1(аи ..., а,> м (( ... а ) можно определить функцию одйого аргумента 478 ПРИЛОЖЕНИЯ ПГ 29 479 ч !! РЕГУЛЯРНО В ЫЧИСЛИМЫЕ ФУНКЦИИ. ФОРМАЛИЗМ ( рассуждения, мы можем прп этом ограничиться рассмотрением функций только одного ареугяента'). Относительно процедур вычисления арифметических функций Одного аргумента можно считать, что каждая такая процедура может быть изображена в виде процедуры вывода в подходящем дедуктивном формализме, содержащем цифры, знак равенства и одноместный функциональный знак ((и) нли же какое-нибудь составное выражение 1(т) с одной аргументной переменной, представляющее вычисляемую функцию. Вычисление значения этой функции для значения аргумента, равного ш, мы будем интерпретировать как вывод равенства ((ш) = и, где и — значение вычисляемой функции для данного аргумента; при этом для любой цифры 1, отличной от у), равенство ((ш) =1 должно быть невыводимым.
Если это условие выполнено для некоторой функции ( н данного формализма Р, то функцию ( мы будем называть вычислимой в формализме г'. Факт переноса вычисления в дедуктивный формализм сам по себе еще не обязательно дает какое-либо пригодное для применений уточнение понятия вычислимости, если не потребовать, чтобы оперирование с выражениями происходило в этом формализме по четко описанным правилам. Поэтому мы введем предположение, которое однажды уже было положено в основу изложения теорем Геделя: мы будем считать, что может быть установлена такая нумерация выражений нашего формализма натуральными числами, при которой номера выводимых формул будут представлять собой значения некоторой рекурсивной функции') )(и). Замечание. Это условие, как ранее было показано'), выполняется всякий раз, когда нумерация выражений формализма такова, что может быть указан некоторый рекурсивный предикат Е(пг, н), который для любых чисел ш и и выполняется тогда и только тогда, когда ш является номером некоторой последователь- ') Впрочем, все дальнейшие определения я теоремы, формулируемые для фуяяцяй одного аргумента, соввршеяяо аналогичным образом могут быть рвсорострвяеяы я вв фуяяцяя нескольких аргументов, я вто вокввыввет, что полученное таким образом яоеятяв вычясляцой функции яесяольявх вргуцея.
тов в чвстя ревультвтов совпадает о твм уточнением, яоторов получвется яз уточяеяяя вояятяя вычвсяяцой функции одного вргумвятв посредством только что уявввяяого сведения фувхцвй нескольких вргуыеятов я функциям одного аргумента с помощью фуяяцяя Ч(Г)(л,, ..., л ) я вв обращений. в) Термин р в я у р св в яый цы будем здесь употреблять втоц жв самом смысле, в яаком оя употреблялся явця в рекурсивной арифметике. Твк, под рвкурсяввой фуяяцвей мы будем пояямвть Гвкую функцию, которая может быть определена прв помощи ярвмвтвввых рекурсий. Сц, с.
271. в) Сц. с. 345 — 347. таран представляет собой вывод формулы с номе- иости фоРмУл, котоРаЯ п ром ц. е оп щению мы добавим два — не очень сущ ественных — ограничения на пуме ациен что можно Указать Рекур тем сВОЙстВОм, чт то любые два числа и огда 1 является номером — иф а Будем также считать, н только тогда, к ек снвную функцию Г(т), что зна=г г е à — некоторая ци ра. что можно указать такую рекурсн чение ее для числ а 1 являющегося номером р и — цифра, рав но самой этой цифре и. ем определению: арифметическую Так мы приходим к следующему оп е г вита мы будем называть регулярно функцию одного аргумен а ", если она вычислима в т аком дедуктивном фор- вычислимой, ажно установить нумера- мализме г', дл р я вы ажений которого м о перечисленным условиям.
цню, удовлетворяющу ю только что пе ь словиями рекурсив- Увловия эти мы будем называть у с л о ности. м оп еделении является то, что для каждой может б т выб ан отдельной подлежащ " а ей вычислению ункции свой формализм Р. Согласно сказанному этот формализм всякий оторой процедуры вычис- раз представляет со бой изоб ажение нек об зом и нормируется, но ления, которж, юы опр д оп еделенным ра оп е елена с достаточно' все-таки может быть Опр д Однако может быть указ казан некоторый ор.
ег ля но вычислимая р функция вычис- тем сВОйством, что Всякая изме п ичем этот орм л лима и в этом формалж , р взят довольно узким. Достаточно взять, нап о фо мализма представляет собой равенб ми. В качестве термов мы ство ~~~ду Р термы Рекурсивной Рифмег Р У метики е кур с В берутся только одноместными и двуместными, о-в р счны~~ы Выраж~н я нд )ь„ " те м. В-т етьих, термами очи осре ство явны оп е- ния представляющие собой введенные и 1 ные знаки с термами в р качестве аргументов. делений функциональные зн р ных пе емениых какими-либо тер- нескольких свободных индивидных перемен мами '). ') В отличие от установленных нами правил оперирования со свяввяяыяя пускать яоллязяй вврвцевяымя, обычное огрвявчеяя, р ение, требующее яе до е и в я йы и я сц., в я пример, с.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
