Гильберт, Бернайс - Основания математики. Теория доказательств (947376), страница 95
Текст из файла (страница 95)
Такая неформальная интерпретация логического формализма в сочетании с общеупотребительным пониманием арифметических символов дает нам некоторую содержательную верификацию для аксиом и схем системы (3). Однако, став на путь такого содержательного понимания следования, мы совершенно отходим от гильбертовских идей теории доказательств, и потому напрашивается вопрос, не можем ли мы при доказательстве непротиворечивости системы (Х) избежать этого содержательного понимания, даже если мы и выходим за рамки финитного рассмотрения, допуская (хотя бы в интерпретированном виде) в качестве посылок предложения типа всеобщности. з) Зто нстолниззнне близко х ншоляоззнню нмплнкзцнн И-ьщ, данному Колмогоровым з рамках его интерпретации гейтннгизсниго нсчнслення зыснн зывзннй кзн исчисления задач: «н нредииложеннн, чти дано решение зздзчн м, ешнть задачу Е» (см.
Ко! шой ос о!1 А. 2иг 1)еи!ицй бег !П1ицшпий!зсЬен ойй.— Мзй. 3., 1932, 36, № 1). Кроме того находясь на позициях теории доказательств мы будем ощущать некоторую неудовлетворенность, если для системы (Е) у нас будет только такое доказательство непротиворечивости, которое в сущности основывается на некотором истолковании какого-то формализма. Рассматривая формализм рекурсивной арифметики и устанавливая его непротиворечивость, мы также не удовлетворились одной лишь ссылкой иа возможность его финитного истолкования, а еще убедились в этом с помощью специально разработанного метода возвратного переноса подстановок в исходные формулы и дополнительного рассмотрения, проведенного для схемы индукции.
Так, и 'для формализма (Х) тоже желательно было бы найти такое доказательство его непротиворечивости, которое основывалось бы на прямом рассмотрении этого формализма. Обоим указанным требованиям удовлетворяет доказательство, непротиворечивости формализма (2), которое недавно было дано Герхардом Генценом '). Мы изложим здесь это доказательство без подробностей, а более детально остановимся только на одном существенно используемом в ием способе рассуждений из канторовской теории множеств, представляющем собой как раз ту часть доказательства, которая не укладывается в рамки формализма (Хи). н) Трансфинитная индукция одного частного вида и ее применение в геиценонском доказательстве непротиворечивости системы (Х). До сих пор в качестве средств, выводящих при доказательствах непротиворечивости за рамки формализма (Уи), нам х) Оеп1зеп О.
Рде %гйегзргисьз1ге!Ьец бег ге!Вен ЕАЬ!еи!Ьеог!е.— МА1Ь. Апи., 1936, 112, № 4; ание Рзззиий без %ьйегзргисьз!гейензЬеже!зез !йг б!е геше Аллеи!Ьеиг!е.— Рогзсьиийеи зиг Ьой!н ипб зиг Огипб1ейиий бег ехзй!ен %!Меизсьзиеп, Хеие Ро13е, ! 938, № 4. (Русские переводы обеих работ имеются з сб. «Мзтемзтнчеснзя теория логического зызодзм — Мл Фнзмзтгнз, 1967, с. 77 — 153 н 154 — 190.— Прим. перев.) Во второй рзбчге содержится методически улучшенное н более элементарное наложение этого доязззтельстзз. С другой стороны, материал, содержзщнйся з первой работе, является более обширным, тзн язн, кроме непротиворечивости рассматриваемого формализма, тзм устанавливается еще н некоторое свойство р едуц яр у емос тн любой выводимой формулы этого формализма. Добззленне нрн втором нздзннн.
Опубликованному з Мзй. Апп. генценизсному доказательству непротнзоречнзостн предшествовало еще одно, более рзннее доказательство, которое з сзое время по техническим нрнчннзм — нлн, кзн бы мы сегодня, пожалуй, сказали: необосназзнно — было отклонено а вследствие этого заменено Генценом донзззтельстзом, апублннованным з Мзй. Анн. Это более раннее доказательство, гранки которого сохранились, содержится в английском нздзннн собрания сочинений Геяценз, вскоре выходящем з свет под редакцией Манфреда Сабо. Несколько упроЩенное изложение этого доказательства содержнтея з работе Бернайса: В е гнзуз Р.
Оп йе ог!3!пз! Оен1зеп соизийепсу ргоо1 1ог пии|Ьег йеогу.— 1и: 1пьимошзш зпб Ргоо1 ТЬеогу: Ргосеенцийз о1 1Ье 3шишег Сон!егеисе з! Ви)- 1з1о, Ь1, Ъ', Ашз1егбзш: Хогй-Но!!знй !968. 441 ИЕПРОТИВОРЕЧИВОСТЬ АРИФМЕТИКИ 44О ВЫХОД ЗА РАМКИ ТЕОРИИ ДОКАЗАТЕЛЬСТВ [гл ч были известны лишь различные определения истинности. И в только что рассмотренном доказательстве непротиворечивости системы (2), опирающемся на определенное истолкование системы (3), выход за пределы формализма (Хп) тоже происходит за счет того, что формализация этого истолкования формализма (3) сводится к некоторому определению истинности. В генценовском доказательстве непротиворечивости формализма (Х) появляется другой тип выхода за рамки (гп).
Этот выход происходит в связи с обоснованием одного конкретного обобщения принципа полной индукции. Речь идет об одном специальном способе уь:озаключений, применяемом в канторовской теории множеств, который называется трансфинит ной индукцией, потому что он представляет собой распространение обычного принципа индукции для конечных чисел на «трансфинитные» порядковые числа. Принимая во внимание наше стремление подчеркивать методические различия, это название следует признать вводящим в заблуждение. На самом деле немалую часть теории трансфинитных порядковых чисел можно рассматривать вполне финитными методами. Так, в частности, тому специальному случаю принципа трансфинитной индукции, который мы в дальнейшем будем рассматривать, можно придать вид некоторого логико-арифметического принципа.
Чтобы выразить этот принцип в нужном нам виде, мы определим рекурсивным образом некоторые, зависящие от числа и отношения порядка а -~Ь. П Отношение а -4 Ь по определению будет означать обычное а отношение порядка а» Ь. Отношение а -4 Ь по определению будет означать, что Ь~ О П+! и что либо а=О, либо у числа Ь имеется такой простой делитель гов который в разложение Ь входит в степени большей, чем в разложение а, и номер которого ! в отношении -~ находится П после номеров всех тех отличных от (о! простых чисел, которые в разложения а и Ь входят в различных степенях. (Отношение а -ьЬ словами будет читаться следующим образом: П «число а предшествует в порядке -ь' числу Ь», или «число а П в порядке -ч находится до числа Ь», или «число Ь в порядке -~ П П находится после числа а».) Формально данное определение может быть изображено с использованием переменной п следующим образом: а -бЬ а<Ь, о и --!с Ь~Ой(а=О~/Эх(х =.Ьйт(а, г)(т(Ь, х)й П' яг(я~шах(а, Ь) йх-т'г- т(а, г)=т(Ь, г)))).
В последней эквивалентности, согласно установленному ранее !), кванторы могут быть исключены, так что выражение, стоящее в правой части, может быть переведено в некоторый рекурсивный предикат. Отсюда видно, что отношение а -~ Ь представляет собой П рекурсивный предикат, зависящий от а, Ь и и. Далее, легко убедиться, что при любом фиксированном п отношение а -4Ь обла- П дает свойствами отношении порядка, которые выражаются посред- ством формул ') < 1(а -ь' а), П а -чЬйЬ-чс-ьа -)с, П П П и что, кроме того, имеет место альтернатива (2) а=Ь~/а -4Ь~/Ь -(а.
П и Затем, как и для обычного отношения порядка между числами, имеют место следующие соотношения: с=~=бйа -ьЬ-ьа с -4Ь с, П П ачь Ойсчьбйсчвб'-ьа -за с. С другой стороны, если с отлично от О, а а и Ь взаимно просты с с и если а -чс и Ь -ь'с, то а Ь -чс. П П П Кроме того, имеет место следующее, характеристическое для взаимосвязи между отношениями -ь' и -~ соотношение П П+! (3) «о» т )! П-~-! П В каждом из порядков -~ число О предшествует всем осталь- П ным, а вслед за ним идет !.
Поэтому простое число )оо, т. е. 2, ') См. с. 273 — 274. !) В настоящем рассмотрении мы используем зти формулы только и качестпе сокращений для утперждеяяй, которые сами по себе мыслятся кяя неформальные. 442 выход з» Рлмки теогии доклзлтельств [гл. ч 443 НЕПРОТИВОРЕЧИВОСТЬ АРИФМЕТИКИ $»] предшествует, согласно (3), всем остальным простым числам н следующее за ним простое число есть 3. Отсюда в свою очередь получаем, что в каждом из этих порядков после ! непосредственно следует число 2. К перечисленным элементарным свойствам отношений -4 добав- П ляется еще одно, которое, говоря на теоретико-множественном языке, характеризует эти отношения порядка как полные порядки.
Воспользовавшись принципом «(егВшп поп да(пг» для целых чисел, это свойство можно выразить при помощи некоторого обобщения принципа наименьшего числа, которое, подобно этому принципу для отношения а(Ь, изображается формулой А (а)-» Лх(А (х) й Уу(А (у) -»х= у~/х -»у)). Преобразуя эту формулу с использованием альтернативы (2) и подстановки формулы ) А (с) вместо формульной переменной А(с), мы получаем следующую дедуктивно равную ей формулу: Чх(1!у(у -~х-~-А (у))-Р А(х)) — » А(а). Таким образом, последняя формула изображает некий принцип, который, если принять «(егЕштп поп да(цг», равносилен принципу наименьшего числа.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
