Гильберт, Бернайс - Основания математики. Теория доказательств (947376), страница 91
Текст из файла (страница 91)
'1 См. т. 1, с. 419 — 427 и с. 509. 513, а также с. 74 — 75 настоящего тома. ь) См. с. 329 — 335. "! См. с. 367 и далее. !4* 420 ВЫХОД ЗА РАМКИ ТЕОРИИ ДОКАЗАТЕЛЬСТВ !гл ч 421 НЕПРОТИВОРЕЧИВОСТЬ АРИФМЕТИКИ Аналогично для двуместного функционального знака 1, вводимого равенствами 1(и, О) =а(и), ((и, и')=Ь(и, л, ((а, и)) (в качестве переменного параметра здесь всегда можно брать переменную и), номер выражения (!с, Ь! в его зависимости от номеРов аРгУментов с и Ь бУдет изобРажатьсЯ фУнкцией б )а"„ (эи+ „ причем если 1 и 1 суть номера выражений а(и) и Ь(а, Ь, с), то в качестве и мы будем брать значение выражения 21 3'. Таким изображением рекурсивно введенных функциональных знаков мы добиваемся, в частности, того, что по номеру любого рекурсивного терна можно получить набор всех тех рекурсивных равенстве которые участвуют в его рекурсивном построении '). Номер последовательности, состоящей из этих рекурсивных равенств, записанных в порядке возрастания их номеров, рекурсивно зависит от номера рассматриваемого терма.
Пусть 1(т) обозначает некоторую рекурсивную функцию, выражающую эту зависимость. С помощью этой функции мы изобразим в (Хи) понятие значения рекурсивного терма без переменных. Действительно, вычисление значения такого терма 1 может быть формализовано посредством вывода, который от рекурсивных равенств, участвующих в рекурсивном построении 1, ведет к равенству 1=- ш, где ш — значение этого терма.
При этом используются аксиома равенства (3г), правила подстановки и средства исчисления высказываний. С помощью подходящей рекур. сивной формулы 3 (т, )г, п) можно изобразить высказывание «список формул о номером т является выводом формулы с номером 1, использующим аксиому равенства (3в)„правила подстановки и средства исчисления высказываний». И поэтому значение терма 1 в его зависимости от номера этого терма в формализме (ЕР) изображается функцией )г„-(уЭ(у,1(а), 70 11' 13" ). 2.
В критериях опровержимости, полученных нами с помощью теоремы Эрбрана, было использовано общее понятие выяислимой функции'). Ограничение рассматривавшихся там функций вычислимыми было произведено для того, чтобы придать рассмотрению финитный характер, Априори не ясно, как само по себе неточное ') Нв возможность такой нумерации рекурсивио введенных фуикциоивль. иых вникав, которая удовлетворяла бы уквввииаму условию, вероятио, воер.
вые указал Рудольф Квривц (см. Сит о яр и. Ьой!всЬе Буо1вх бег БргвсЬе.— %1еп, !934, 5. 59). г) См, с, 223, в также с. 214 и далее. интуитивное понятие вычислимости может быть подвергнуто формализации. Однако в последнее время зто уточнение все-таки было осуществлено, причем таким образом, что при этом заодно получилась и формальная изобразимость этого уточнения в формализме !Л„). Уточнение это было произведено посредством трех существенно отличных друг от друга понятий, относительно которых впоследствии было установлено, что они описывают одну и ту же совокупность функций.
Это — восходящее к Эрбрану и Геделю понятие обшерекурсивной функции, принадлежащее Черчу и Клинн понятие ).-оп редели ион функции и введенное А. М. Тьюриигом и Э. Л, Постом понятие вы числ имой функции. Совпадение объемов первых двух понятий было установлено Черчем и Клини, а совпадение объемов третьего и первых двух— Тьюрингом (с использованием уже обнаруженного совпадения объемов первых двух понятий) '). Здесь мы приведем лишь существенный для данного контекста результат этих исследований. По поводу его обоснования мы отсылаем читателя к Приложению П в), а здесь только отметим, что это обоснование опирается на одно предположение, которое вследствие неточности обиходного понятия вычислимости лишь может быть сделано правдоподобным и оправданным последующими результатами.
Речь идет о предположении, что любая вычислительная процедура может быть изображена в виде вывода в подходящем, специально для этой цели построенном дедуктивном формализме, причем этот формализм может быть устроен так (и это существенно!), что на основе надлежащим образом выбранной нумерации совокупность номеров выводимых в этом формализме выражений совпадает с совокупностью значений некоторой конкретной рекурсивной функции. Это в высшей степени правдоподобное предположение в качестве одного нз своих следствий позволяет нам заключить,.что любая вычислимая функция ((и) одного аргумента (рассмотрсние многоместных вычислимых функций легко сводится к рассмотрению одноместных) может быть изображена в формализме (Ли) г)06 этом см.
СЬцгсЬ А!опго. Ац ццво1чвЫе ргоЫеш о1 е!ешео1вгу пшцЬег !Ьеогу. — Ашег, Л Мв!Ь„1936, 58, № 2; К! е е п е 5. С. Оеоегэ! гесцгв!Те !ццсцоцэ о1 пвщтв! ВшцЬегв. — Мвтй. Апц., 1936, 112, № 5; К 1 е е и е 5. С. А-бе1!цвь!1!1у вцб гесцгв!Тецеэв.— Ешйе Мв!Ь. 3., 1936, 2, № 2; Р ав1 Е. Е. Ршце сошЫпв1огу ргосеээев.— Л. 5ушьо11с Ьой!с, !936, 1, № 2 [русский перевод: Пост Э. Л, Фииитиые камбиивториые процессы.— В кил Уса е ис к и й В, А.
Машина Поста. Мл Наука, 1979, с. 89 — 951; Т и г | а К А. М. Оп со|арц1вЫе цшцЬетэ, и!1Ь вп врр!!сэ1!оп 1о пйе ЕцтвсЬе!бапявргоЫеш,— Р|ас. Ьоод. Мень зос., зет, 2, 1936/37, 42, АРРеаб!х; Тат|их А. М. Соп|- ра1вЬ|рну вод А-ае!!овЬ|1!1у.— Л 5ушЬо1!с 1.ой!с, 1937, 2, № 4, ') См. с, 477 и далее, 423 НЕПРОТИВОРЕЧИВОСТЬ АРИФМЕТИКИ 422 в виде ()(р И(1. п, хИ, чхщуИ(1, х, д) вхЗУИ(1, х, у). ВЫХОД ЗА РАМКИ ТЕОРИИ ДОКАЗАТЕЛЬСТВ [Гл.
ч где ()(пг) — некоторая не зависящая от ! рекурсивная функция '), И(к, 1, т) — тоже не зависящая от ( рекурсивная формула, не содержащая свободных переменных, отличных от й, 1 и ю, а !в цифра, зависящая от определения функции 1, такая, что для любой цифры ! может быть указана некоторая цифра щ, находящаяся с 1 и 1 в отношении И(1, 1, щ). Функция ((и) изображается указанным выражением в том смысле, что для любой цифры 1, если и является значением ((1), то формула ()(р,„И(1, 1, х)) и выводима н (Хн) и даже в некотором (определенном независимо от функции ! (а)) подформализме формализма (У,„) ').
С другой стороны, можно непосредственно убедиться, что если цифра 1 обладает тем свойством, что с помощью некоторой конкретной процедуры для любой цифры 1 может быть указана цифра !и, для которой выполняется отношение И(1, 1, щ), то выражение ()((з„И(1, п, х)) изображает (в только что разьясненном смысле) некоторую вычислимую функцию аргумента и. Таким Образом, в качестве формализации в формализме (Х ) Р совокупности вычислимых функций можно рассматривать совокупность тех чисел 1, которые удовлетворяют условию, изображенному формулой А понятие значения вычислимой функции при чзч!Ксироваином значении аргумента формализуется термом 1)(р.И(й, 1, х)), где переменная Й представляет зависимость от функции, а переменная ! — зависимость от значения аргумента. Правда, надо отметить, что это изображение вычислимых функций в формализме (ЕР) все-таки не является таким изображением в полном смысле слова, какое мы имеем для рекурсив» ных функций в (7„).
Более того, можно показать з), что существуют числа 1 такйе, что для каждой цифры 1 можно указать 9 Под рек урси внымв функцнямн здесь, кзк в ранее, воннмзютсв такие функцна, которые могут быть определены крнмнтнвнымв рекурсиями. '! Зтат формзлнзм ввлветсв твквзе подформзлнзмом рзссмотревного нзмк в конце гл. П (с. 163 — 165) непротиворечивого врвфметнческого формализма. '! Зто следует нз одной общей теоремы Кзннн, доказанной в его уже упоминавшейся работе збепегз! геснгяче 1ннсцопз о! Озюгз! Оншьегзз (творе мз Х!!!), цифру щ, связанную с 1 и 1 отношением И(1, 1, а), без того, чтобы формула была выводимой в (ХР), — по меньшей мере в предположении, что для любой рекурсивной формулы 21(а, Ь) из выводимости в (2Р) формулы чхЗуе((х, у) может быть извлечена эффективная возможность для каждой цифры щ указывать некоторую цифру и, связанную с ш отношением р((щ, и).
3. Иногда в наших доказательствах непротиворечивости используется один вид полной индукции, который не формализуется схемой индукции рекурсивной арифметики, Этот выход за рамки рекурсивной арифметики связан с тем, что в наших формулировках н доказательствах время от времени встречаются такие допущения, в которых говорится об истинности некоторых всеобщих предложении; таковы, например, предположение о невыводимости или о неопровержимости какой-либо формулы, или предположение о непротиворечивости какого-либо формализма, нлн же предположение о верифицируемости какой-либо формулы, что, согласно определению, означает, что эта формула при любои замене свободных переменных цифрами оказывается истинной.
Любое высказывание, содержащее такого рода предположение, представляет трудности и для финнтного понимания. Как известно, фннитное допущение всегда относится к какой-либо наглядно характеризуемой ситуации. Но истинность всеобщего предложения не может считаться таковой. Правда, вместо предположения, что рассматриваемое всеобщее предложение истинно, можно взять предположение о том, что истинность этого предложения установлена. В этом случае мы имеем допущение о наличии некоторого доказательства. Но при этом данное доказательство должно допускаться как неформальное; а неформальная убедительность доказательства опять-таки не является интуитивно ясной. Интуитивная неясность неформального представления о доказательстве как раз и является причиной, вызывающей необходимость формализации доказательств, с помощью которой— по крайней мере в рамках определенных дедуктивных формализмов — оказываегся возможной наглядно определенная характеризация доказательства как такового.
Однако на самом деле и в тех случаях, когда мы пользуемся предположениями вроде предположения о верифицируемости какой-либо формулы Я, мы ссылаемся вовсе не на структуру какого-либо возможного неформального доказательства верифнцнруемости Я; самое большее, что подразумевается в таком предположении, — это то, что в любом месте рассуждения, где речь идет о какой-то формуле, получающейся из р( в результате подста- 424 выход зл РАмки теоРии доклзлтельств 1гл.
ч 425 НЕПРОТИВОРЕЧИВОСТЬ АРИФМЕТИКИ ковки, мы можем воспользоваться тем, что рассматриваемая формула является истинной. Поэтому было бы правильным утверждения, у которых в качестве посылок фигурируют какие-либо всеобщие предложения, в рамках финитного рассмотрения оформлять не в виде предложений, а в виде правил умозаключений, как мы это уже и делали при изложении критериев опровержимости формул исчисления предикатов '). Такие правила, в частности, могут применяться в сочетании с полной индукцией так, что переход от п к и+ 1 происходит не с помощью какого-то предложения, а о помощью некоторого правила.
В таком случае вторую посылку схемы индукции мы не можем изобразить в рамках рекурсивной арифметики формулой 2((п) -+.и'(и+ 1). Такой случай имел место, например, в одном ранее проведенном нами рассуждении '). В этом рассуждении рассматривался арифметический формализм, получающийся из исчисления преднкатов путем добавления к нему символов О, ', +, и =, аксиом а=а, а Ь-Р(а=с-РЬ=с), а=Ь а'=Ь', а'чь0 и рекурсивных равенств для сложения и умножения. Непротиворечивость этого формализма получалась прямо из ип-теоремы, из которой мы, кроме того, получили, что любая формула, выводимая средствами упомянутого формализма с добавление»«, быть может, верифицируемых иоходных формул, не содержащих формульных и связанных индивидиых переменных, является верифицируемой, На основании этого результата и со ссылкой на одно проведенное в гл.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
