Гильберт, Бернайс - Основания математики. Теория доказательств (947376), страница 88
Текст из файла (страница 88)
Возможность проведения этой индукции по и, т. е. выводимость обеих формул Ухь1(0, х) и чхь4(и, х) — «чхь4(и', х), устанавливается на основе нашей леммы, а также 6мсхем, с помощью которых, в частности, получается, что для произволь- ных формул И(с) и зр(с) формализма (Е), содержащих перемен- ную с, в (Хм) выводима формула 6А ((Й (С))) а 6А ((40 (С))) -«61 (((г (Й (г) 8'. р (2))1). Таким образом, мы убеждаемся, что и для формализма (Е) невозможно осуществить — при условии его непротиворечивости— формализованное в самом (Х) доказательство его непротиворечи- вости. Тем самым заодно мы получаем, что при условии непро- тиворечивости (Е) непротиворечивость эта не может быть доказана даже в формализме (Ем).
В ~ амом деле, по выводу формулы Чхбт(х, и)-«13х6,(х, 3 и) в формализме (ХР) мы смогли бы получить вывод этой формулы и в формализме (Е). Этот результат ставит теперь перед нами вопрос о том, каким должно быть расширение формализма (Х) для того, чтобы в ием было возможно формализованное доказательство непротиворечи- вости (Е); в частности, требуется ли для этого введение какого- 4О8 ВЫХОД ЗА РАМКИ ТНОРИИ ДОКАЗАТЕЛЬСТВ ~гл и ФОРМАЛИЗАЦИЯ АРИФМЯТИЧНСКОГО ФОРМАЛИЗМА 4от либо нового типа связанных переменных, — например, связанных формульных переменных? Прежде чем заняться этим вопросом, мы сначала найдем какое-нибудь неформальное доказательство непротиворечивости (Х). При этом мы не будем связывать себя требованиями финит.
ной точки зрения, а потому в рассмотрение сможет войти и такое доказательство, которое опирается на обычное истолкование формализма (Х), соответствующее содержательному применению принципа «1егбшп поп г)а1пг> к целым числам. Наиболее простой, напрашивающийся способ доказательства заключается в том, чтобы сформулировать для формул формализма (Х) каное-либо оп ределение понят и я истин ности, на основе которого можно было бы доказать, что всякая выводимая формула является истинной и что отрицание всякой истинной формулы истинным не является. Следует ожидать, что и ри этом, ввиду теоремы Тарского о формализации понятия истинности'), наше определение понятия истинности будет выходить за пределы формализма (Х).
В самом деле, к формализму (Х) и к нашей нумерации этого формализма, извлеченной нами из нумерации для (Х„), полностью применимо прежнее рассуждение, с помощью которого мы в свое время усилили антиномию лжеца'). Поэтому получается, что в формализме (Х), если он непротиворечив, не может существовать формулы И(о) с единственной свободной переменной а, обладающей тем свойством, что для любой цифры и, являющейся номером какой-либо формулы 6 без свободных переменных, формула йИ (и) »6 выводима в (Х), Далее, получается, что в формализме (Х„) — при условии его непротиворечивости — тоже не может быть такой формулы %(а), для которой упомянутая эквивалентность выполнялась бы всякий раз, когда 6 — какая-либо формула из (Х) без свободных переменных, а и — номер этой формулы.
Действительно, для всякой такой формулы Ю1 (а) можно было бы, исключив из нее )«-символ, построить такую формулу йИз(а), чтобы в (Х„) была выводима эквивалентность 9И, (а) йИ (а). Тогда для любой цифры и, являющейся номером какой-либо ') См. с. 328. ') Формализм (2) н наша нумерация этого формализма с самого начала удовлетворяют условию б). Предположения з) н в), правда, выполняются не полностью, тзк кзк рекурсивные функции, ваабще говоря, в (2) не нзабрззнмы, в лишь предстзвнмы. На, кзк мы помним, этот балее общий случай был взмй специально предусмотрен (см. с. 326-327).
формулы 6 из (Х) без свободных переменных, в (Х„) была бы выводима эквивалентность ~Из(п) Но так как эта эквивалентность является формулой формализма (Х), то она должна была бы выводиться и в (Х) Тогда формула %«(а) обладала бы свойством, относительно которого мы только что установили, что наличие в (Х) формулы с этим свойством не совместимо с непротиворечивостью (Х), а значит, и с непротиворечивостью (Хв) Так мы получаем метод, позволяющий про формализованные определения истинно".ти для формул формализма (Х) доказывать, что они выводят за пределы формализма (Х), а также за пределы формализма (Х ), если формализм (Х„), а следовательно, и формализм (7), нейротиворечив. Действительно, это с полной гарантией имеет место всякий раз, когда добавление этого определения к формализму (Х) дает формулу Ы (а), обладающую тем свойством, что для любой формулы 6 формализма (Х), не содержащей свободных переменных, и для ее номера и выводима формула ш) (и) 6.
А теперь, в духе этого рассуждения, мы перейдем к построению некоторого определения истинности для формализма (Х). Для этого мы будем пользоваться рекурсивными изображениями различных понятий, относящихся к формализму (Х) и к построенной нами нумерации этого формализма.
Свойство числа и быть номером постпояипогоэ) шермп изображается с помощью некоторой рекурсивной формулы ~з(п). Соответствующее определение немедленно получается из того, что любой постоянный терм из (Х) либо является цифрой О, либо имеет вид и', где и — некоторый постоянный терм, либо имеет вид и+8 или и 8, где и и 3 — какие-либо постоянные термы. Значение постоянною терма есть функция номера этого терма.
Эта функция изображается с помощью некоторой рекурсивной функции ч1 (и)'), определяемой следующим разбором случаев: «Если п=2, то ч! (п) =О; если п=3 и и «ЛАЛО, то ч!(п) =(ч)(гп))', если и = 5 11 1Зэ, то ч) (и) =ч) (а) +ч) (Ь); если п=б 11'17э то ч1(п) ч!(а) ч1(Ь); во всех остальных случаях ч1 (и) = и.» Рекурсивное изображение понятия номера формулы для формализма (Х) может быть дано совершенно аналогично тому, *) Авторы употребляют гермнн «чзг«за«еп1аз».
— Прим. перев. ') Та, чта вазмажнасть этого изображения, несмотря нз нзш прежний результат относительно изображения понятия «знзченне выражения, определяющего числов (см. с. 328), согласуется с непротиворечивостью (2), аснавывзется нз там, чта рекурсивные функции, вообще гевара, нензабрззнмы в (2). ФОРМАЛИЗАЦИЯ АРИФМЕТИЧЕСКОГО ФОРМАЛИЗМА 409 ВЫХОД ЗА РАМКИ ТЕОРИИ ДОКАЗАТЕЛЬСТВ |ГЛ. Р кан оно ранее давалось для исчисления предикатов с добавлением цифр и функциональных знаков '). Мы обозначим его через Я (п).
Без труда могут быть получены рекурсивные изображения и для следующих предикатов: «число л является номером некоторой формулы без свободных переменных» — посредством некоторой формулы Яе(и); «число и является номером некоторой формулы без переменных» — посредством некоторой формулы Я,(п); «число п является номером некоторой нвазиформулы» — посредством некоторой формулы !р(п); «число л является номером некоторой бескванторной квази- формулы» — посредством некоторой формулы 7»(п).
Затем мы можем рекурсивно определить понятие номер а предваренной нвазиформулы. Действительно, сначала можно ввести рекурсивный предикат $,(л, й), изображающий высказывание «число и является номером некоторой предваренной квазиформулы с й кванторами». Это может быть сделано с помощью рекурсивного определения, которое в неформальном виде выглядит следующим образом: «7,(п, О) имеет место тогда и только тогда, когда имеет место ~Фа (п)' г)), (и, й') имеет место тогда и только тогда, когда и =г) 50 р', где а~ 2, р — простое число, большее или равное 7, а кроме того, имеют место Ф(и) и и»)|(а, й)».
Теперь высказывание «число и является номером некоторой предваренной нвазиформулы» изобразится формулой Зх(х(ие|Ч),(л, х)), и эта формула может быть переведена в некоторую рекурсивную формулу $„(п). Формула |1)А (л) ег АО (л) будет изображать высказывание «число п является номером некоторой предваренной формулы». Теперь мы можем определить такую рекурсивную функцию рг(п), которая номеру каждой формулы ставит в соответствие номер некоторой предварениой формулы, переводимой в эту исходную формулу. Но предварительно мы определим рекурсивный предикат Зр(и), изображающий высказывание «число п является номером некоторой нвазиформулы такой, что для всякой входящей в нее связанной переменной либо все вхождения втой переменной находятся в области действия единственного в данной нвазиформуле одноименного с этой переменной квантора, либо таких кванторов е данной квазиформуле нет вообще».
") См. с. 280 и далее. Кратко говоря, смысл этого высказывания заключается в том, что и является номером такой квазиформулы, в которой связанные переменные путем соответствующих переименований обособлены друг от друга. Такого рода квазиформулу мы будем называть нормированной к в азиформ улой. Например, квазиформулы л~(Х)ЙЧХ6(Х) И г»|Х(6(хг Е)-+-Уу'|ГХЗ(хг уг Х)) ие являются нормированными, а квазиформула Чх(А (х, у)-»-ЗЕВ(х, г)), напротив, является нормированной.
Далее, может быть введена ренурсивная функция зр(и), которая номеру любой формулы ставит в соответствие номер формулы, получающейся из нее в результате замены переменных при кван- торах (в порядне появления этих кваиторов) переменными с номерами )Р„)Р„..., причем всякая такая замена распространяется на всю область действия соответствующего квантора. Формула, получающаяся в результате применения этой операции, а танже каждая являющаяся ее составной частью кваэиформула представляют собой нормированные нвазиформулы. Определение искомой функции рг(п) дается с помощью двух вспомогательных функций рг,(л) и рг,(л). Функция рг, (п) определяется следующим образом: «Если п=З т, т=д.50 р', г)(2, р — простое число, большее или равное 7, и |р,(т), то рг|(и)=и(2, |1) 50, ррг,|» а|. если ЗР(п), и=а.20 7» 11', г)(2г Ч),(а)г З),(Ь)г а=д, 50 Ра, г),~2 и р — простое число„большее или равное 7, то рг»(п) =|7, 50 рр'*(»""" ); если Яр(и), и |1 20 7 11», д~2, $а(а), 7,(Ь), Ь=г)А 50 р', |1,~2 и р — простое число, большее или равное 7, то рг,(п) =а, 50 ррг (»»ач'"")' во всех остальных случаях рг,(л) =и».
Определение функции рг,(л) выглядит следующим образом: «Если Яр(и), п=З т и тчь0, то рг»(п)=рг,(З рг,(т)); если Зр(п), и=|у 50 р, |7~2 и р — простое число, большее или равное 7, то рг» (и) — |1 50 ррг,|а| ° «[О $2) ФОРМАЛИЗАПИЯ АРИФМЕТИЧЕСКОГО ФОРМАЛИЗМА 4[[ ВЫХОД ЗА РАМКИ ТЕОРИИ ДОКАЗАТЕЛЬСТВ [ГЛ. Ч если Зр(а), а=у 20 7 11" н [7~2, то рго (и) = рг! (д, 20. 7РИ са) . 11Ро, со)) если Зр(а) и п=80 7' 11», то рг (а) = рг! [40. 7Р а!о ).
11Р [М); если Бр(п) и а=160 7' 11», то гп~ (20 7рг, соо.орга (о а),ирл сы) 11рп (оо,)ргв са).ирл со о))ь во всех остальных случаях рго(п) =а». Теперь функция рг(п) может быть определена равенством рг (и) = рг, (зр (а)). Далее, мы введем еще рекурсивное отношение 31(т, а), которое будет изображать высказывание «либо т=п, либо выражение с номером л получается из выражения с номером т в результате подстановки вместо одной или вместо нескольких переменных (индивидных или формульных)». Введем также функцию з[ (т, й, 1), которая номеру е) какого-либо выражения У[, номеру 1 какои- либо индивидной переменной с и номеру 1 какого-либо выражения Г будет ставить в соответствие номер выражения, получающегося из «) в результате повсеместной замены переменной с выражением [. Теперь искомое определение истинности может быть пос)роено следующим образом: Сначала мы определяем какую-либо рекурсивную формулу У1«(а), изображающую высказывание «число л является номером некоторой истинной формулы без переменных»'„затем мы даем формализованное определение для предиката М(п, й), изображаю- щего высказывание «число а является номером некоторой истин- ной предваренной формулы без свободных переменных с й-кван- торной приставкой».
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
