Гильберт, Бернайс - Основания математики. Теория доказательств (947376), страница 78
Текст из файла (страница 78)
') См. с. зээ. ») См. е, 347, и ззб 4 И ггхницы изовэхзимостн и зыводимост Наконец, мы еще добавим следующие условия на вывод и м о с т еи 1. Если в Р можно указать вывод формулы с ном р е ом) из формулы с номером 1, то в Р выводима формула Зх6 (х, 1)-«. Зхб (х, 1). 2. Формула дх6(х, е(й))-~=)х6(х, е(б()е 1))) выводима в Р. а ий пе еменных, 3 Если ((т) — рекурсивныи терм не содержащии ер отличных от перем еременной т, а е — номер равенства 1(а) =О, то 1(т) =О-«-=)х6(х, б(е, т)) выводима в Р. оамечани 3 е. Формула упомянутая в условии, р д н2 пеставия: «если в Р собой формализацию следующего высказыван ание о м лы Л (с номером 1), то для любой ф ы 1 в Р выводимо и отрицание ч рмулы, п ци гры в Я в результате подстановки цифры 1 вм р есто пе еменной а», «еперь, пос ле того как мы перечислили наши предположения Р, мы должны еще выбрать в качестве ф р у относительно , мы д во ечивости Р.
о н из формализаций утверждения о непроти ор одну из фо Формализация этого утвержд рждения может быть произведена при помощи формулы )(6(1, п) Й6(т, е(п))), е е( ) — фиг рирующая в предположении бе) рекурсивная функ- " формулы нз Р сопоставляет номер ция„которая номеру всякой „ ее отрицания. ю ая в дедуктивном Этой формуле дедуктивно равна следующ отношении более удобная формула Зх6(х, и)»- ) Лхб(х, е(п)).
Эт формулу мы и возьмем в качестве формулы ее, из которой должна быть выведена формула )6(, ч). у орм т Напомним, что 4 определяется как номер формулы .)6(т, б(р, р)), а р — как номер формулы ) 6(т, б(а, а)), откуда, на основании пре п редположенного нами свойства рекурсивной функции б(й, 1), следует справедливость равенства б(р, р) = — 4 и выводимость этого равенства в Р. 12* 356 ВыхОд ВА РАмки теОРии дОкАВАтельстВ Номер формулы 6(а, «) мы Обозначим через г, и пусть г, обозначает номер формулы )6(а, «). Тогда будет иметь место е (г) = гд, м лы После этих приготовлений вывод формулы ) 6( у дз может быть получен следующим образом.
т, «) из форВследствие выводимости равенства 6 (в, р) = «формула ) 6(т, «) выводима из формулы )6(т, 6(р, В)). Далее, форм ла )6(, ) (т, «) в результате подстановки, Поэтому а, «), т. е. формула о номером г, выводима в Р из формулй формула (т, 6(р, р)), имеющей номер «. Поэтому согласно уел в 1 оно условию :-)хЗ(х, «)-» =)хЗ(х, г,) выводима в Г. Эта формула, взятая вместе с формулой 6(т, «)-» =)хЗ(х, «), выводимой средствами исчисления предикатов, дает формулу 6(т, «)-ч.=)х6(х, г,), а затем на основании выводимого в Р равенства е (г) = г, — формулу 6 (т, «) -~ )хЗ (х, е (г)).
Эта формула вместе о формулой :-)хЗ(х, е(я))-ьБ)хЗ(х, е(6(я, ())), которая выводима в г согласно условию 2 и в которой вместо переменную переменной я можно подставить циф ( а фру, а вместо переменной д п ременную т, дает формулу 6(т, «)-»-ЭхЗ(х, е(6(г, т))), откуда путем контрапозиции получается формула ~:-)хЗ(х, п('6(г, т)))-Р ) 6(т, «). С другой стороны, формула 6(т «) имеет в Ь(, ) — О, (, «) — р курсивный терм, содержащий единственную пере- менную т. Номером равенства Ь(а, «) =О, т. е. форм лы 6(, является число г.
По формула о г. оэтому в В, согласно условию 3, вывод има Ь(т, «) =О-».ЗХЗ(х, 6(г, т)), т. е. формула 6(дн, «)-» ЗхЗ дд, е(и т)). гРАиицы изоввлзимости и выводимости 337 $ и А теперь воспользуемся формулой (д. Эта формула в результате подстановки терма 6(г, т) вместо переменной и дает формулу :-х'3(х, 6(г, т))-~)=)хЗ(х, г(6(г т))П которая вместе с только что полученной формулой 6(т, «)- Эхб(х, 6(, т)) и ранее выведенной формулой )ЗХЗ(х, е(6(г, т)))-». 16(т, «) с помощью двукратного применения правила силлогизма дает формулу 6(т «)-+ 16(т «)» которая с помо.цью элементарного преобразования позволяет получить искомую формулу ) 6(т, «).
Таким образом, мы установили, что в формализме г" может быть осуществлен вывод формулы ) 6(т, «) из формулы д». В случае выводимости в г" формулы й в Г будет выводима и формула ) 6(т, «), а отсюда, согласно предыдущему, будет следовать противоречивость формализма Р. Итак, оказывается справедливой следующая Теорема. В непротиворечиво.ч формализме г, удовлетворяющем условиям а») и б»), а также трем сформулированным выше «условиям на выводи»даст»», не может быть выведена формула Лхб(х, и)-»- ) Эхб(х, «(п)), представлюощая собой формализацию утверждения о непротиворечивости Г. Это утверждение составляет содержание второй теоремы Геделя с неполноте в применении к формализмам, удовлетворяющим условию а,), т.
е. к таким формализмам, в которых выводимы все выводимые формулы рекурсивной арифметики, не содержащие формульных переменных, и в которых могут быть воспроизведены все умозаключения исчисления предикатов. Эта теорема может быть распространена и на формализмы несколько иного типа, Мы не обязательно должны требовать, чтобы формализм г содержал в себе формулы арифметического формализма непосредственно; вполне достаточно, чтобы соотношения рекурсивной арифметики как-то были выражены в нем с помощью соответствующих выводимых формул. Так, в частности, можно получить все те обобщения, возможность которых мы отметили при формализации первоначальной антиномии лжеца: ВЫХОД ЗА РАМКИ ТЕОРИИ ДОКЛЗАТЕЛЬСТВ гРАиицы изопплзимости и выводимости 359 1гл ч $и !.
Не теб р уется, чтобы формализм Р содержал какие-либо свободные переменные, (Достаточно, чтобы переменная а включа- 2. Если с помощью какого-либо выражения 3(х) в формализме может быть изображен предикат «объект х является числ ьно, чтобы в Р имелся специально выделенный ислом», сорт числовых переменных. Вместо цифр тоже мог ф вать какиеоже могут фигуриро- 3. М -либо соответствующие им более сложные вь е выражения.
Можно не требовать, чтобы рекурсивные функции были непосредственно изобразимы в Р. Достаточно требовать некото ой го, как это ыло сделано заменимости этих функций, наподобие того как б при замене функциональных знаков соответствующими им олами или при замене в формализме (Х) равенств ими предикат- рекурсивной арифметики соответствующими формулами. у " еет, в частности, место в модифицированном фор- мализме РНпс(р(а Ма!)!еша(!са, на основе которого Гедель изло- жил свои теоремы о неполноте.
Каждое из перечисленных обобщений требует оп ед модификации п ф редположений этой теоремы (в частности, условий определенной на выводимость), а также модификации ф (г, ф щей утверждение о непротиворечивости Р, и той ~" м случае второй теоремы Геделя необходимо тщательно еле за выполнением сл у овий ее применимости к дедуктивном фоо следить мализму. На это обстоятельство указа Г. К е), в связи с этим следующий пример. л . райзел, пост оивший виям а иб Будем исходить из формализма Р, удовлетворяю е з),) а). Будем считать, что имеется нумерация ф щ го усло- и списков фо м л ф р у, обладающая перечисленными в предположрация формул нии б,) своиствами.
дположеСле ю ду щее предположение не повлечет за собой ограничений на фо мализм Р с о никаких формализм Р, а на нумерацию наложит только некоторое несущественное ограничение: мы предполож предположим, что ме е пт, так что р ф р. улы, в которую входит цифра п!, раве н по меньшей либо о лы с р, для любой цифры е, являющеися номеро йф рму, одержащей переменную а, и для любой циф м каио- значение б(г а) авн ой цифры а этому формула (, ) р в о по меньшей мере а, и что соответстве ственно т(б(т, т) с переменной т выводима в рекурсивной арифметике а тем т) К ге!зе! С. А зпгчеу о1 ргоо1 1ьеот .— 3. Я см.
подстрочную сноск на с. 331, гу.— . уаьо!ю 1.ой!с, 1958, ЗЗ, ску на с., 333 и раздел «Мвейещае!са! 1.оя!сз в книге; ! .. есентез оп Модегп Майещае!сз 111.— Х. Зойп %!1еу 11 зопз 1пс. !955 р 154 — 155. з) См. с. 354. Кроме того, будем считать, что формализм Р удовлетворяет трем нашим условиям на выводимость'), так что по второй тео- реме Геделя о неполноте формула 6()е, о)- ) 6((, е(р)), которая в силу нумерации для Р изображает непротиворечивость этого формализма, невыводима в Р, если формализм Р действи- тельно непротиворечив '). Перейдем к рассмотрению некоторого модифицированного фор- мализма Р*, отличающегося от Р только следующим усилением условия формальной доказуемости: список формул с номером а называется выводом формулы о! в Р*, если он является выводом этой формулы в Р и если, кроме того, ни у каких двух списков формул, являющихся выводами в Р и имеющих номера, не пре- восходящие а, их заключительные формулы не совпадают (зто свойство всегда может быть непосредственно проверено путем перебора всех выводов с номерами, не превосходящими а).
Как мы уже знаем, в формализме Р высказывание о том, что список формул с номером !и является выводом формулы с номе- ром и, в силу свойств нумерации формул и списков формул изображается при помощи рекурсивного предиката 6 (т, л) формулой 6(а, и). В формализме Рв роль рекурсивного преди- ката 6(т, л) будет играть предикат 6 (т, л) Зт У иУоУтоУ г (и ~ т й о ~ т Зт 6 (и, то) Зт 6 (о, г) -ь г ~ е (ео)), который мы сокращенно будем обозначать посредством 6'(т, л). Этот предикат ввиду соотношения 6(т, л)-ьл(т тоже является рекурсивным. Так как выводимость в Р* определялась как выводимость в Р при некоторых дополнительных условиях, то всякая формула, выводимая в Р*, будет выводимой и в Р.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
