Гильберт, Бернайс - Основания математики. Теория доказательств (947376), страница 126
Текст из файла (страница 126)
у, и) — «и = г) -»- [аа„„(А (и, о), а, В, п)-«С„„(Я(А, и, о, и), а, В, и'И. Из полученных таким образом формул ьзц»» (хе (и, о), а, В» 0) и ЧхЧу шгЧ и (В (х, у, и) -«и = г) — « [ЯЯ!в!А1„,(Е, а, В, и)-«=(Е!згхл„,(У, а, В, и')1 при помощи полной индукции мы получим требующуюся нам ') В первом издании нашей книги вместо последнего члена заключения Эха(л (и, о)- о=к) втой формулы стояло выражение »Уи(и(п-«нх»го(г(и, о)-» о х)). Тем самым зтот вывод — подобно дедекиндову доказательству выполнимости рекурсивных равенств (см.
т, 1, с. 500! — оказывался связанным с порядковым отношением (. То, что здесь можно обойтись без привлечения етого отношенвя, было показано П. Лоренценом в его работе: Ьогепхеп Р. Рме Ве1»и!поп богсЬ то1!з1апб!Ее 1пбпй11оп.— Мопа1зЬ, Ма1Ь. РЬуз., 1938/39, 47, 5.
356 — 358. Приведенный выше вывод в точности соответствует рассуждению Лоренцена.— другое, тоже не использующее отношения порядка доказательство выполнимости рекурсивных равенств было дано Л. Кальмаром. См, его работу: К а! ш а г Ь. Оп Ьйе роза!Ь»1!1у о1 беппгИоп Ьу гесцгмоп.— Ас1а 11Н. зс!еп1. йей. 17п!и. Нцпяагкае ..., Бес11о зс1еп1. ща1Ь., 1940, 9, № 4, Р. 227 — 232. ПРИЛОжвния формулу ЧхЧуЗгЧи(В(х, у, и) ~и=«) — ~-ЗЕ~МО„,(г, а, В, и).
Из нее мы без труда получим формулу [3) ЧхЧуЧиЧО(В(х, у, и) й В (х, у, о) -~ и = о) -э Кс„а, (а, В (х, у, г), и, Ь) й Кс„т, (а, В (х, у, г), и, !) - й = !). Формулы [21 и [31 изображают тот факт, что определенный нами предикат Кс, универсальный для рекурсивных предикатов, каждому числу и однозначным образом сопоставляет некоторое число й — в предположении, что в качестве В(1, т, г) взята фор- мула, удовлетворяющая формулам единственности по третьему аргументу,— а формулы [11 выражают тот факт, что при этом выполняются условия рекурсии, определенные аргументами а и В. С помощью символа Кс„„,(а, В(х, у, г), и, й), производя соответствующие подстановки, мы получим формулы для пред- ставления рекурсивных функций; именно, для любой т-местной рекурсивной функции 1(п„..., и„) у нас получится некоторая формула, представляющая равенство ((и„..., и,)= и.
Так, например, для функции а+Ь представляющую ее фор- мулу Аб(а, Ь, с) можно получить при помощи определения Аб(а, Ь, с) цс„у,(а, х=хйу'=г, Ь, с)„ из которого получаются формулы Аб(а, О, а), Аб(а, Ь, с)-~Ад(а, Ь', с'), Ад(а, Ь, й)й Аб(а, Ь, !)-~й=!. Для умножения а Ь представляющая формула Мр (а, Ь, с) полу- чается при помощи определения Мр(а, Ь, с) Кс,„,(0, х=хйАб(у, а, г), Ь, с), Формула, представляющая функцию ( ), дается выражением КС„У,(0, Аб(х, у, г), п, й).
Поэтому для функции ') т(а, Ь) представляющая ее формула Т(а, Ь, с) получается при помощи определения Т(а, Ь, с) ЗИЗО(Аб(а, Ь, и)й Кс„к,(0, Аб(х, у, г), и', о) йАс$(о, а, с)), Га+Ь+1~ т) т(а, Ь) ~ )-1-а. См. с. 553, а также т. 1, с. 397, 2 ) т П испОльзОВАние сВязАниых аОРмульных пеРеменных 393 Из этого определения выводятся формулы ЗхТ(а, Ь, х), З«ЗуТ(х, у, с), Т(а, Ь, с)йТ(а, Ь, 4-~с=И, Т(а, Ь, й)йТ(с, д, й) — а=сйЬ=И. Теперь мы перейдем к теории положительных действительных чисел. Для изображения положительных действительных чисел целесообразно воспользоваться сечениями.
Такое изображение может быть формализовано с помощью определения 6 „(А(х, у)) ЧхЧу(А(х, у)-ь.хчьОйу~О]й ЗхЗуА(х, у)йЗ«Зу(х~Ойу=Ой )А(х, у))й ЧхЧуЧиЧо(х~Ой ЧгЧв(Мр(х, о, г) й Мр(у, и, в)-~г(вй А (и, о)-~-А (х, у)) й ЧхЧу(А (х, у)-~-ЗиЗОЗ«Зв(Мр(х, о, г)й Мр(у, и, в)йг«-вй А(и, о))), которое здесь играет роль определения символа 6(а) в формализмах Н и К. Отношение порядка для таких чисел в данном случае формализуется при помощи определения «= „,„(А(х, у), В(и, о)) Ч«Чу(А(х, у)-+ В(х, у)). Арифметические действия над положительными действительными числами могут быть изображены предикатнымн символами вида 1[)„„„(А(х, у), В(и, о), а, Ь), причем на основе определения соответствующего символа может быть выведена формула 6„„(А(х, у)) й6,„(В(х, у))-ь 6„у(7,,(А(и, о), В(в, г), х, у), Так, например, изображение операции умножения двух положительных действительных чисел дается следующим определением предикатного символа ><„У,„(А(х, у), В(и, о), а, Ь): :~С„У„(А (х, у), В(и, о),а, Ь) З1ЗиЗЬЗв[А(1, и) йВ(о, в)й ЗхЗуЗг(Мр(1, о, х)йМр(и, в, у)й Мр(х, Ь, «)йМр(у,.а, «))).
пянложянив пу Число О и отрицательные числа могут быть изображены при помощи следующих определений: О„„(А(х, у)) ЧхЧу(А(х, у) х=Ойу~О), 6„„(А(х, у)) ЗУ<мЗУ<м (6 е(У(х, у))й О„„(д(х, у)) й ЧхЧд(А(х, д)-и(х, у) Ч Р'(х, д))). После этого понятие действительного числа формализуется посредством определения 6„"„(А(х, у)) 6„„(А(х, у)) ~/0„„(А(х, у)) Ч 6„„(А(х, у)), с которым связывается следующее определение равенства; =„„„,(А(х, у), В(и, о)) ЧхЧу(А(х, у) В(х, у)). Арифметические действия над действительными числами изображаются аналогично случаю положительных действительных чисел.
Понятие последов ат ел ь ности дейст в и т е л ь н ы х чисел формализуется посредством определения 6„*е,(А(х, у, г)) Чх6„*,(А(х, у, г)). Формализацию понятия у п о р я д о ч е н н о г о ч и с л о в о г о множества дает нам определение Об„э(А(х, у)) ЧхЧу(А(х, у) ~/ А(у, х) А(х, х)йА(у, у))й ЧхЧу (А (х, у) й А (у, х) -~ х = у)й ЧхЧуЧг(А(х, у)й А(у, г)-РА(х, г)). С помощью этого определения можно получить формализацию понятия вполне упорядоченного числового множе- ства. Она дается определением Р(„„(А(х, у)) Об„„(А(х, у))й ЧХПП(ЭгХ(г)-Р "=(д (Х (у) й Чг (Х (г) й А (г, г) -+ А (у, г)))). Общие теоремы о множествах действительных ч и с ел такие, например, как теорема о точной верхней границе, не могут быть формализованы в Л формулами, но их можно формализовать схемами формул.
Если бы мы захотели включить в формализм В обсуждавшийся нанн частный случай принципа выбора, то это можно нспользовлннс связлнных Фогмяльных пьвемвнных аозт было бы сделать добавлением соответствующей схемы формул. Простейшей подходящей для этого схемой является следующая схема: ЧхЛУ~ПЯ,(х, г'(г))-+.-(У~те,(х, 'г (х, г)). Из нее применением формул для предиката Т(а, Ь, с) может быть установлена выводимость следующей схемы формул: ЧхЗ)'"~Л„„(х, у (и, о))-+ =П' мЧхЛ„„(х, )'(х, и, о)).
ПРИЛОжВНИВ 'Р ДОКАЗАТЕЛЬСТВА НЕПРОТИВОРЕЧИВОСТИ АРИ ФМЕТИ ЧЕСКОГО ФОРМАЛИЗМА 9 1. Доказательство Кальмара' ) В качестве арифметического формализма, непротиворечивость которого будет здесь доказываться, мы возьмем систему (Е). Установив непротиворечивость (Х), мы докажем тем самым и непротиворечивость (У ). Это вытекает из соотношения, существующего между двумя данными формальными системами ввиду определимости )с-символа через с-символ и теоремы об устрани- мости характеристика).
В системе (Х ), как мы помним, могут быть явно определены примитивно рекурсивные, а в некотором более общем смысле и квазирекурсивные функции '). С другой стороны,' в планируемом доказательстве не возникнет никаких осложнений и в том случае, если формализм (Е) расширить с самого начала, разрешив введение специальных символов для вычислимых функций одного или нескольких натуральных аргументов, т. е. для таких арифметических функций, значения которых при любых значениях их аргументов могут быть найдены при помощи надлежащей вычислительной процедуры. С понятием вычислимости естественным образом связываются понятия сатаяной и ложной формулы, а также понятие верифицирРалюй формулы.
Формулы или термы мы будем называть нумер ическ ими, если они не содержат никаких переменных'). Нумерическое равенство будет называться истинным, если в результате вычисления всех входящих в него функций обе его части принимают одно и то же значение. В противном г) Изложенное ниже доказательство, принадлежащее Ласло Кальмару, ранее не публиковалось. Оно было представлено з сентябре 1938 г.
в ваде подробной рукописи. з) См. с. 401 данного тома (последннй абзац). Система (л) была введена в г. 1 на с. 454, символ ркА (к) в т. 1 на с. 481, а система (л ) в т. П на с. 366. Теоремз об усгрзннмостн харзктернсгнн доказана в гл. 7П!. г. 1. ') См. г. 1, с. 499 — 509 н г. 11, Прнложенве 11, с. 483 — 485. .«) Такое употребление термина <нумернческнйз представляет собой некоторое расширение нашего прежнего определения, сформулированного в г. 1 на с. 283 н в т. П на с. 56, согласно которому формула без переменных назывзетсн нумернчесаой лншь в том случае, если все входящие в нее термы авлнютса цифрами. доклзлтельство кАльмАРА случае равенство будет называться ложным. Истинному равенству приписывается значение «истина», а ложному — значение «ложьз.
Так как в формализме (2) после добавления к нему вычислимых функций все элементарные формулы будут по-прежнему являться равенствами '), то мы должны будем рассмотреть только такие нумерические формулы, которые строятся из нумерических равенств с помощью связок исчисления высказываний. Для такого рода формул их истинностные значения однозначно получаются из истинностных значений составляющих их элементарных формул на основе понимания связок исчисления высказываний как истинностных функций. Подобно тому, как это делалось раньше'), формулу без связанных индивидных и без формульных переменных мы будем называть верифицируемой, если она при любой подстановке цифр вместо всех входящих в нее свободных индивидных переменных переходит в истинную нумерическую формулу.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
