Гильберт, Бернайс - Основания математики. Теория доказательств (947376), страница 130
Текст из файла (страница 130)
Для любого такого вывода †будем называть его редуцированным — при помощи проведенного нами рассуждения, путем надлежащей оценки тех входящих «0« 613 докАзАтельство кАльмАРА 4П 612 ПРИЛОЖЕНИЕ в концевой фрагмент молекул, которые являются экзистенциаль* ' ными формулами, можно будет убедиться, что заключительная формула нашего вывода в силу ее нумеричности является истинной. Тем самым будет показано, что заключительная формула- первоначального вывода тоже является истинной, так как при ', производимых нами операциях устранения индукции и квантора: существования заключительная формула не меняется вообще,: а при вычислении нумерических термов в концевом фрагменте.' хотя эта формула сама и может измениться, но ее нстинностное значение останется без изменений. Таким образом, непротиворечивость системы (Х) будет установлена, если мы сможем показать, что последовательность 'применений операций устранения индукции и квантора существова-, ния, производимых в соответствии с принятыми соглашениями над любым построенным по правилам нашего формализма выводом, после конечного числа шагов должна оборваться, т.
е. привести к редуцированному выводу. С этой целью мы воспользуемся введенными в гл. Ч О-ш-фигурами ') и некоторым сопоставлением фигур этого рода формулам наших выводов. Мы напомним определение этих фигур и отношения порядка между ними, причем заодно мы произведем и некоторую разбивку этих фигур на ярусы. В роли фигуры нулевого яруса у нас будет выступать один только символ О; фигурами первого яруса будут суммы вида газ+сиз+...+аз, состоящие по крайней мере из одного члена; мы будем считать, что О предшествует любой фигуре первого яруса и что порядок между фигурами этого яруса устанавливается по числу членов в них.
Вместо шз мы для краткости будем также писать 1. Пусть теперь О-в-фигуры вместе с отношением порядка для них введены до яруса с номером Й включительно, причем ' так, что фигуры каждого из этих ярусов превосходят фигуры предшествующих ярусов. В качестве фигур (й+1)-го яруса мы возьмем выражения вида сваг+гааз+., + сваг (с чь О) у которых формальные показатели степени аы а„..., а, являются О-ш-фигурами ярусов не выше й-го, причем а, принадлежит в точности )с-му ярусу, а кроме того (в обычных обозначениях), а,=- ~аз~...= а,. Порядок для фигур (3+1)-го яруса устанавливается таким образом, что из двух различных фигур а и Ь ') См. с.
451 — 452. Зтат способ введения каитаравских порядковых чвсел, меньших первого иавтаравскаю а-числа, восходит к Г. Гсикеву. См. ага работу: бе п с ге п О. )севе Газзввх с1аз 9С!6сгзргисйз!ге!Ье!!зЬсгче!звз 10с 6!в геше ха)пепгвсас!е.— гасзсйипхев гвс Ьах!Ь вид гвс Ссввд!ехипх двс ехай1ви в!!ашизсьас!сп Хсие га13е. 1938, № 4, 8. 38, 39. фигура а считается большей, если у первого слева различающегося члена этих фигур показатель степени у а больше, чем у Ь, или если а получается из Ь добавлением одного или нескольких членов. Кроме того, все фигуры (й+ 1)-го яруса считаются ббльшими, чем все фигуры предшествующих ярусов. После того как таким способом рекурсивно определены О-в- фигуры и отношение порядка между ними, получается, как легко видеть, что определение сравнения двух фигур одного и того же яруса может быть применено н к фигурам различных ярусов, так как у любой фигуры (1+1)-го яруса первый член имеет больший показатель степени, чем у любой фигуры более низкого (ненулевого) яруса.
Фигура О меньше всех остальных О-в-фигур. Вез труда можно убедиться, что определенное нами отношение порядка для О-ш-фигур является транзитивным. Затем можно доказать, что если а — О-ш-фигура, то ша †то О-в-фигура, и что если а и Ь вЂ д О-ш-фигуры такие, что а ~Ь, то имеет место и неравенство ва( ш~. Таким образом, соответствие, сопостав. ляющее фигуре д фигуру саа («показательная функцияз), является (в обычном смысле) строго монотонным. Кроме того, ш' всегда больше а. При итерациях показательной функции скоб- С ками можно и не пользоваться: например, выражение ш"в может вс пониматься только так, что ш" является в нем показателем степени, а у шв показателем степени является ш'. Натуральную сумму а~ 3 мы определим как функцию двух аргументов, значениями которых являются О-ш-фигуры.
Мы положим (по определению) а~О а, О~ а а. Если же а и Ь отличны от О, то я ~ Ь мы определим как О-ш-фигуру, которая получается, если взять все слагаемые фигур а и Ь с учетом их кратности и упорядочить их так, чтобы ни одно слагаемое с меньшим показателем степени не предшествовало ни одному слагаемому с ббльшим показателем '). Из этого определения без труда получается, что для любых О-ш-фигур а, Ь и с имеют место равенства а~3 Ь4Ьа и а~ 4$(Ь4рс)=(а3ЬЬ)~с. Поэтому можно рассматривать многочленные натуральные суммы (без скобок), не принимая при этом во внимание порядок расположения слагаемых. Можно показать, что если в натуральной сумме увеличить одно или несколько входящих в нее слагаемых, то увеличится и значение суммы.
') Гсаивав определение натуральной суммы представляет собой чзстиый случай прииадлсжащсса Герхарду Гессевбергу более общего аиределвиия натуральной сумиы для ираизвальиых парядкавых чисел. См. сга рабату: Н е аз е и Ь е г 8 О, Сквадьсхг!11в двс Мепася1еЬсе, — АЬЬ. 6. сс)еззсйсв $сЬв!в, Хеие Ра!Ев, В6 1, Со!!!пхсв, 1906, 8, 479-706. 615 пРиложение э и докАЕАтельство кАльмАРА Таким образом, натуральная сумма, подобно показательной функции, является строго монотонной.
А теперь формулам рассматриваемого нами вывода мы сопоставим в качестве их порядковых чисел некоторые 0-а-фигуры. При этом мы будем придерживаться следующих соглашений. Всем исходным формулам, за исключением'аксиом для кван- тора существования, сопоставляется порядковое число 0; аксиомам для квантора существования сопоставляется порядковое число 1. Если верхней формуле некоторой схемы вывода для квантора существования сопоставлено порядковое число а, то нижней формуле этой схемы сопоставляется число а Ф 1. Нижней формуле схемы заключения, верхним формулам которой сопоставлены порядковые числа а и Р, сопоставляется число а ф з, если высота верхних формул равна высоте нижней формулы; если же высота верхних формул на й превосходит высоту нижней, то порядковым числом нижней формулы мы будем считать порядковое число, полученное из а Чч Р в результате й-кратного применения показательной функции: щаФ9 Пусть верхние формулы схемы индукции имеют порядковые числа а и Р.
Если З равно О, то порядковое число ее нижней формулы будет равняться а ~ 1; если же Р отлично от 0 и первый его член (может быть, единственный) равен а', то нижняя формула в качестве порядкового числа будет иметь а41а'и'. Таким образом, в любом случае порядковое число нижней формулы нашей схемы индукции будет больше любой из натуральных сумм а ЧР з Ч1 з ЧР ... ЧГ Р. содержащих одно слагаемое а и любое конечное число слагае- ' мых Р; в частности, оно больше а.
Этим определением каждой формуле любого вывода, произве- . денного по правилам рассмотренного нами формализма, однозначно . сопоставляется некоторое порядковое число. Порядковое число . заключительной формулы вывода объявляется порядковым числом ' самого этого вывода. Следует заметить, что при нахождении порядковых чисел, соотносимых формулам данного вывода, должны учитываться высоты этих формул, поскольку порядковое число нижней формулы схемы заключения зависит от разности высот ее верхних формул и нижней формулы.
Эта разность может быть отлична от нуля только тогда, когда верхние формулы схемы заключения имеют степень, более высокую, чем ее нижняя формула. В то время как высоты формул вычисляются снизу вверх, начиная с заключительной формулы, порядковые числа формул растут сверху вниз, начиная с исходных формул. Отметим также, что прн формальном переходе от формулы Я (г) к формуле Я (6), производимом двукратным применением схемы заключения с использованием истинной иумерической формулы ~=6 и соответствующей формулы равенства с=6, г=6- (Я(г)-э-Я(6)) Я (г), Я (г) -+ Я (6) Я (6) все формулы, кроме, быть может, равенства г=6 (которое, как мы знаем, имеет степень 0), имеют одну и ту же степень. Следовательно, для этих схем заключения разность соответствующих высот равна нулю.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
