Гильберт, Бернайс - Основания математики. Теория доказательств (947376), страница 97
Текст из файла (страница 97)
И все-таки эта формула вместе с формулой 1пд„(А(х), 0) еще не позволяет применить в рамках формализма (ХР) схему индукции. Такая возможность имелась бы в том случае, если бы в нашем распоряжении были связанные формульные переменные. Тогда мы смогли бы вывести формулу') УУ1пбл(У(х), и)-ь ай!У 1пс(„((з'(х), и'). Другая возможность заключается во введении некоторого првдикатного символа (в расширенном смысле этого слова) Г,(с, А(г), и, й) с помощью следующих рекурсивных эквивалентностей: Г, (с, А (г), и, 0) А (с), Г, (с, А (г), и, й') Зц (с, Г, (у, А (г), и, и), и — й'). Вторая из этих эквивалентностей дает нам формулу 1(и-+.(Г,(с, А(г), и, и — 1) 6„(с, Г,(у, А(г), и, и — 'Г), 1)), из которой с помощью формулы 1пбл(6р(х, А (у), и), и)-ь1пбл(А(г), и'), куда вместо и нужно подставить 1, а вместо формульной пере- менной А (а) — формулу Г, (а, А (г), и, и -- Г), мы получаем формулу 1(и — ь[1пб„(Г,(х, А(г), и, и — 1), 1)ь 1пд„(Г,(х, А (г), и, и —.
Г), У)], а далее при помощи средств исчисления высказываний с использованием формул 1«=и 1'~и и 1(и-ь1~и получаем формулу [1 ~ и — 1пбл (Г, (х, А (г), и, и — 1), 1)] -е- [Г ~ и-ь 1пс(„(Г, (х, А (г), и, и — ' У), Г)]. ') При этом применение связанных формульных переменных можно была бы ограничить таким образом, чтобы вместо свободных формульных перемен. ных допускались подстановки только таких формул, которые самк связанимя формульных переменных ие содержат. Если к этой формуле добавить формулу О~и-+.1пс),(Г,(х, А(г), и, и — '0), 0), получающуюся нз формулы 1пд„(А(х), 0)„то можно будет применить схему индукции.
Эта схема даст нам формулу 1( и-ь1пби(Г,(х, А (г), и, и — '1), !) и, подставив в нее и вместо 1, мы с помощью формул и~и и — 'и=О и Г,(с, А(г), и, О) А(с) получим формулу 1пд,(А (х), и), которая дает формальное изображение обобщенного принципа индукции относительно любого порядка -4. и Этой формализации можно будет придать несколько более элементарный вид, если мы удовлетворимся тем, что вместо выво- димости формулы 1пд (А(х), и) с формульной переменной А(с) получим только выводимость формулы 1пд (Я(г), и) для каждой отдельно взятой формулы Я (с), не содержащей формульных переменных.
В этом случае для каждой отдельной формулы Я(с) (без формульных переменных), где аз, ..., а,— возможно фигу- рирующие в ней отличные от с свободные индивидные перемен- ные, мы вместо символа Г,(с, А(г), и, й) определим некоторый предикатный символ дд(с, а„..., а„и, й), который введем аналогично символу Г, с помощью некоторых рекурсивных эквивалентностей. При этом, как я в определениях рекурсивных функций, параметры а,„..., а, можно будет реду- цировать в один-единственный, в качестве которого мы возьмем переменную а. Для формулы Я(с), которая кроме с, содержит переменную а и никаких других свободных переменных не содержит, эти рекур- сивные эквивалентности, с помощью которых вводится соответ- ствующий предикатный символ Аа(с, а, и, й) с параметром а, записываются следующим образом: Аз(с, а, и, 0) Я(с), 1".!(с, а, и, й') Ър(с, Е1(у, и, и, й), и — й'). [Если формула Я(с) других свободных переменных кроме с не содержит, то вводимый предикатный символ будет содержать только три аргумента с, и и й.] Здесь Зр(с, А (у), и) представляет собой формулу !Ух]6.„(х, с) й УУ(У -4 к-~А (У))-з- ЧУ(У -~ г ]ос-~.А(У))]' л+1 и+! !б Д.
Гнльаере, П. Бернайс 4 3! непвотивовечизость АРифметики ВЫХОД ЗА РАМКИ ТЕОРИИ ДОКАЗАТЕЛЬСТВ !гл. ч поэтому выражение 6„(с, к)(у, а, п, й), и — Й') имеет вид 'чх«Иь(х, с, и, й)й )гу(Ив(х, у, и, й)-~С(у, а, и, й))-+. ву(Иа(х «з„у, п, й)-ьь)(у, а, п, й))», где И,(а, Ь, и, й) и Ив(а, Ь, и, й) — некоторые рекурсивные формулы, и может быть преобразовано в формулу Ух «-И,(х, с, и, й) )/ =«у(Ив(х, у, п, й)й ~АА(у, а, и, й)) ~/ Уу( !Иа(х «а„у, п, й) )Г' Аа(у, а, и, й))». Таким образом, рекурсивное определение символа ьа(с, а, и, й) аналогично тому, с помощью которого мы ввели символ М(п, й) при определении истинности для формализма (Х)').
Относительно введения символа «ч«(п, Й) мы выяснили, что оио выводит как за пределы формализма (Х), так и за пределы (ХР) '). В связи с этим в высшей степени правдоподобно, что приведенная выше схема, определяющая предикатный символ ~(с, а, и, й), окажется средством, не укладывающимся в рамки формализма (Уи), т. е., вообще говоря, не будет заменяться явными определениями в (Е„). То, что этот способ введения предикатных символов, а тем самым и доказательство рассмотренного частного случая трансфииитной индукции, выводит за пределы формализма (хв), следует из того, что применение этого способа умозаключений вместе с рассуждениями, которые формализуются в (2Р), позволяет провести генценовское доказательство непротиворечивости формализма (Х)з). Мы приведем здесь †хо бы в схематическом виде — ход этого доказательства, причем в новой его редакции а).
С этой целью к проведенному рассмотрению данного частного случая трансфинитной индукции мы добавим еще одно дополнительное рассуждение. Каждый из порядков -б, если отвлечься от конкретного уста ройства упорядочиваемых им элементов (в данном случае являющихся числами), по терминологии Кантора, изображает некоторый ') См. с, 4!1. а) См. с. 415. з) Зто рассуждение исооаьаует вторую теорему Геделя. В одиой более поздней работе: Сепг зев О.
Веже!зьаг1се)1 ццй 1)пьеме!зЬагае',1 чоп Ао1аойз1анео йег 1гаозйцпео 1пйцй11оо 1ц йег ге)цец Аазнец)йеог1е.-й«а1Ь Ацо., 1943, 119, Б. 140 — 161, Геицеи показал, что с помощью иекоторой модификации доказательства непротиворечивости можно и бев ссылии иа вту теорему Геаеля убедиться в том, что обобщенный цриицип индукции существеииым образом ае укладывается в рамки арифметического формализма. а) См. сноску иа с. 439. порядковый тип, причем даже некоторое порядковое число, так как все эти порядки являются полными.
Эти порядковые типы мы можем сделать более наглядными, если вместо чисел в качестве упорядочиваемих элементов возьмем некоторые выражения из формализма канторовской теории второго числового класса. Эти выражения вместе с упорядочивающим их отношением, которое мы будем обозначать обычными знаками ( и ~ для меньше и больше, мы получим с помощью некоторого рекурсивного приема: Исходным, а заодно и наименьшим по этому порядку выражением является символ О.
Если а„..., а,— уже полученные выражения (в конечном числе г), удовлетворяющие условию а,~.ав)...~.аа (знак равенства здесь означает совпадение по написанию), то из ннх может быть построено выраже- ние юаа ««юас. Число т при этом может быть равно и Е Между двумя такими выражениями юаа ««гоаа и юза+ ..-«-юза отношение порядка а, « « а, ( ба « « За вводится таким образом, что для соблюдения его должен иметь место один из следующих двух случаев: 1) а;=Ь; для «=1, ..., т и число т меньше б; 2) для йекоторого ! из списка 1, ..., т имеет место а;(Ь;, причем, если !Ф1, то а)=Ь! для 1=1, ..., ! — 1.
Полученные описанным образом выражения мы будем называть О-ю-ф и г у р а м и. По любому заданному выражению всегда можно выяснить, является ли оно О-го-фигурой, и по любым двум отличным друг от друга О-го-фигурам всегда можно узнать, которая из них является меньшей. Действительно, любая О-ю-фигура является либо символом О, либо степенным выражением ю', где в — снова О-го-фигура, либо она представляет собой построенное из таких степеней выражение, для которого дополнительно выполняется условие ат=-ав~-...~ос. Поэтому для выяснения интеРесующего нас вопроса получается некоторая рекурсивная процедура, которая от рассмотрения заданных фигур позволяет перейти к рассмотрению их составных частей и потому всегда обрывается.
15* НЕПРОТИВОРЕЧИВОСТЬ АРИФМЕТИКИ 452 ВЫХОД ЗА РАМКИ ТЕОРИИ ДОКАЗАТЕЛЬСТВ 1гл, ч Так, например, мы можем констатировать, что выражение ви'+ а~ .» о+ о+ ао является О-а-фигурой, в то время как выражения а"'+О и а"'+""+а" 0-а-фигурами не являются, а также что первая из двух 0-а-фигур а" + аа'+"'+ Ее'+оп И а"" +" + а"' меньше второй. Замечание. В суммах и степенных выражениях, участвующих в построении О-а-фигур, мы можем обходиться без каких бы то ни было скобок: в суммах — потому что процесс последовательного написания выражений ассоциативен сам по себе, а в степенях — потому что всякий раз строятся только степени вида а', так что выражение а ' может восприниматься только как степень а с показателем ш'. еь ФигУРы еР, а'"', еиа бУдУт обозначатьсЯ нами как по, Вы Во.
И вообще, посредством В„мы будем обозначать О-а-фигуру, получающуюся из В, путем и-кратного применения операции перехода от выражения а к выражению аоь). Между порядками -« и порядком, введенным для О-ш-фигур, и имеет место следующее соотношение: для всякого чивла и может быть построена функция ьп(й), отображающая числа на 0-а-фигуры, меньшие Ви+„таким образом, что числовой порядок П переходит в порядок О-а-фигур, или, другими словами, что меньшему из двух чисел в смысле порядка -«соответствует и меньшая П О-а-фигура.
Замечание. Тот факт, что для каждого числа и может существовать не более одного отображения В указанным свойст- т) В кзнторовской теории второго числового класса вместо фигуры ео пишут цифру 1, вместо п-членной суммы ао+...+е'-цифру и в вместо а'— просто е Таким обрезом оо 1 от а, оо а". Рекурсивное определение ои выглядит сдедуюшнм образом: о„ оо 1, он+1 е" «Предело поеледоввтельнооти во, оы ... являетея первым кенторевек им и-ч и слом, т. е, иенменьшим из тех чисел а второго числового илеесе, поторые удовлетворяют уоловию п ао.
Одновременно вто число является наименьшим из чисел второго чиалпвого класса, уже не представимык О-е. фигурами. зом, может быть доказан с помощью обобщенного принципа индукции для порядков — «. Однако этим обстоятельством мы здесь и пользоваться не будем. Функции ьп(м) определяются следующим образом: ьо(0) при. писывается значение 0; при 1чьО Ьо(1) в качестве значения приписывается 1-членная сумма ао+...+а'. Функция (в+,(1) определяется с помощью ьп (й): ьи+, (0) приписывается значение 0; ьо+,(2) при 1 О, 1, ...
в качестве значения приписывается (1+1)-членная сумма оР+...+оР. Если 1 отлично от нуля и не ЯвлЯетсЯ степенью числа 2 и если 1зт ... 1зт — Разложение 1 на простые множители, упорядоченные (при 6)1) таким образом, что при 1((~б либо т+, ть либо т+, -«ть то ьп+, (1) приписывается значение а " ' +...+а" со (п) си Оо) Легко убедиться„что определенные таким образом функции ги(й) доставляют нам отображения с указанным выше свойством; причем это доказывается с использованием того факта, что любая о отличная от нуля О-а-фигура, имеющая вид ам+...+а ' (здесь ат~...:-ат), тогда и только тогда меньше пи+и когда а,(ви.
Из указанного факта также следует, что для всякой 0-а-фигуры а МОЖНО ОПРЕДЕЛИТЬ таКОЕ ЧИСЛО П, ДЛЯ КОТОРОГО а(вв. В итоге мы, таким образом, убеждаемся, что числовой порядок -«совпадает с некоторым начальным отрезком упорядочения и 0-а-фигур по этому порядковому типу, т. е. если упорядочиваемые элементы рассматривать только как указатели места: именно, совпадает с тем начальным отрезком, который образуется и О-а-фигУРами, меньшими Вп+,. Этот начальный отРезок пРостирается тем дальше, чем больше число и, и каждая 0-а-фигура принадлежит некоторому такому отрезку. Но отсюда немедленно вытекает, что обобщенный принцип индукции имеет место и для О-а-фигур, упорядоченных указанным образом.
Замечание 1. Доказательство обобщенного принципа индукции для порядка О-а-фигур, естественно, можно дать и путем непосредственного рассмотрения этих фигур. Метод доказательства при этом будет лишь несущественно отличаться от метода, примененного нами для порядков -«: из справедливости этого и принципа для О-а-фигур, меньших вв (и = 1, 2, ...), мы заключаем о справедливости его для О-а-фигур, меньших пи+,. Мы рассмот- ВЪ|ХОД ЗА РАМКИ ТЕОРИИ ДОКАЗАТЕЛЬСТВ !гл. ч НЕПРОТИВОРЕЧИВОСТЬ АРИФМЕТИКИ 4 з1 рели вначале порядки -6, так как нам было важно выяснить и вопрос о формализуемости этого рассуждения в формализме (2„).