Гильберт, Бернайс - Основания математики. Теория доказательств (947376), страница 54

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла (страница 54)

Поэтому представляется правдоподобным, что многие рассуждения, относящиеся к теории выполнимости, результаты которых ввиду совпадения выполнимости и неопровержимости могут быть сформулированы и в виде теорем о неопровержимости, т. е. в виде теорем теории доказательств (что, конечно, еще не доказывает этих теорем с финитной точки зрения), с помощью наших критериев опровержимости и неопровержимости могут быть непосредственно переведены в те или иные финнтные рассмотрения теории дока .ательств. г) Один пример. С помощью доказанной им основной теоремы Эрбран выполнил такого рода перевод для всех имевшихся в его время теоретико-модельных доказательств'). С тех пор в теории выполнимости было получено много новых замечательных результатов ').

Мы не будем здесь заниматься переводом всех этих исследований на язык финитной теории доказательств, хотя такой перевод и мог бы быть осуществлен во всех этих случаях. Мы ограничимся изложением методики этого перевода на примере одной теоремы, недавно доказанной Й. Пепишем'). Теорема эта утверждает, что для любой формулы !у исчисления предикатов можно указать равнозначную ей по выполнимости формулу, имеющую вид (1) Ч!УгьЗГРЭЕА (Х, у, г) 81'ЧГП1... Уцшьг(ц„..., иш), где х, д, г, ц„..., цш — полный список входящих в иее индивидных переменных. Пепиш доказывает это следующим образом').

Прежде всего, можно считать, что рассматриваемая формула 5 исчисления предикатов имеет вид') чгйз ° ° чгйьЛ1)1 ° =)1)зЕ(Е1 "° Ею Ры "ь рз), 1) См. уже цитированную выше работу Эрбраиа 13иг 1а ргаЫавв 1аидавеп1а! да !а !агийие ва1Ьева1!Чиеь, сь. П, П1. ' ') См. обзор, приведеииый иа с. 259 — 262. з) Р ар !э зозе1. УБ1егзисьицяеп йЬег даз ЕБ1зсье!бицязргаЫев бег ва!Ьэва1!зсьеп Еая!Ь.— Гиидагц.

ва1Ь., !938, 30. Эта работа представляет собой продолжение другого, более раннего исследования Пепиша: Р е р! з 3. Ве1- 1гаге зиг Еебий!ацз1Лааг!е бщ !айцюьеп ЕБ1заье!бипйзргаЫевз — Ас1а За!. Ма1Ь. Ззеяеб, !936/37, 8. з) Изложение, приведенное здесь, атличзется ат изложения Пециша лишь несущественными деталями. з) Впрочем, как показал Пециш в ага рабате: Р ар 1з Д Е1ц 'ь1еггаьгац бег яьаийеваизгЬеп ьай!Ь.— 3. ЯувЬанс Еаг!с, 1938, 3, этого подготавливаю- щего дальнейшие изложения использования теоретико-модельной скалемавскай иармальиай формы здесь можно было бы и избежать. Тем самым мы даби. лись бы некоторого усиления результата.

гДе гз, ..., Ег Р„..., Рз — полный список вхоДЯЩих в нее инДИ- видных переменных, а г и б отличны от нуля, Будем также считать, что 5 не содержит формульных переменных без аргументов. Как мы знаем, любая формула исчисления предикатов эквивалентна по выполнимости некоторой такой формуле. Конечно, эту формулу мы можем выбрать еще и так, чтобы она не содержала формульной переменной А (с аргументами). Пусть нам дана модель этой формулы 5 с какой-либо индивидной областью У '), и пусть для выполняющих логических функций выбраны какие-нибудь символы. Пусть в результате внесения этих символов в формулу 5 вместо ее формульных переменных выражение Е(Г1, " Е, 9 "ьрз) переходит в выражение ~(Е1 " ь ЕГ Р1 " ра).

Наше рассуждение мы начинаем так же, как начиналось доказательство теоремы Левенгейма. Прежде всего, с помощью принципа выбора мы получаем, что при некоторых, надлежащим образом выбранных г-местных функциях у„..., Хз, заданных в области ), формула 3ФЕ1...7ЕФЕ(Е1, ..., Ещ Х1(81, ..., Е,), .... Хб(81, ..., Е.)). отнесенная к области ), является истинной. Опять выделим какой-нибудь элемент из У и возьмем в качестве обозначающего его символа букву а.

Мы опять будем рассматривать выражения, построенные из символов а, ул, ..., )(. Но, вместо того чтобы прямо перечислять их, мы применим следующее, несколько более общее вспомогательное РассУждение. ПУсть 1Р„ ..., 1Рз — аРифметические функции от г аргументов, образующие разделяющую систему функций. Пусть 3з обозначает совокупность тех чисел (цифр)'), которые не являются значениями ни одной из функций 1Р„..., фз. ТОГДа КажДОЕ ЧИСЛО бУДЕт ОДНИМ И ТОЛЬКО ОДНИМ способом представляться с помощью терма, построенного из функциональных знаков гр„..., фз и чисел, принадлежащих Дз. Это утверждение может быть доказано с помощью полной индукции. Покажем, что оно выполняется для числа О.

Действительно, О принадлежит 3з, потому что значения функций ф„... з чр всегда превосходят значения своих аргументов, и, значит, 1) Мы могли бы воспользоваться здесь теоремой Лвввигейма, иа эта иа привело бы иас ии к каким упрощениям. з) Числа здесь следует образно представлять в вида цифр. Заметим, кстати, чта зза наше рассуждение ие претендует иа та, чтобы быть фиаитиым.

230 23! Е.СИМВОЛ И ЛОГИЧЕСКИИ ФОРМАЛИЗМ [ГЛ П[ пРимгнение К ПРОБЛЕМЕ РАВРЕшнмости $5! они больше нуля. Теперь покажем, что если это утверждение выполняется для всех чисел, меньших и, то оно выполняется и для и. Действительно, и либо принадлежит з„либо является значением одной из функций [р,, ..., [р. В последнем случае— поскольку эти функции представляют собой разделяющую систему функций — число и однозначно определяет ту функцию и ту систему аргументов, для которой эта функция принимает значение и, Значения всех этих аргументов меньше и, так что к ним может быть применено наше индуктивное предположение. Итак, каждое число и единственным способом изображается функциональным выражением, построенным с помощью функциональных знаков фм ..., ф„, в котором самыми внутренними аргументами являются числа из Де.

А теперь, если в изображении числа и с помощью функциональных знаков фы ..., ф и чисел из це заменить всякое число из 3е символом а, а всякий функциональный знак [р, (1 = 1, ... ..., 6) — соответствующим знаком )[Р то у нас получится некоторое отображение, переводящее натуральные числа в элементы области ['.

Значение полученного таким образом выражения, являющееся элементом из [ и однозначно определенное числом и, мы обозначим через т[(п). Тогда для произвольных чисел и„..., и, и для [=1, ..., в значение выражения т! (р, (и„..., и,)) будет совпадать со значением выражения [[,(т[(п1), ..., т!(и,)). Кроме того, любая фигурирующая в 6 («1, ..., е,, «„..., «,) логическая функция 7(а„..., а[), заданная в области [', определяет некоторую заданную на натуральных числах логическую функцию [[)(т[(п1), ...

..., 1[(П[)); И ЕСЛИ МЫ ОбОЗНаЧИМ ЧЕРЕЗ Зе (у1, ..., «„«1, ..., «Е) выражение, получающееся из 6(у1, ..., «„«1, ..., «) в результате замены символов логических функций, заданных в области [, символами соответствующих им (только что указанным способом) логических функций, заданных на натуральных числах, то формула 1[[и "'[[Г,6" («1, ". у, ф (у " уе), ", фв(у " у,)) будет истинной в области натуральных чисел. Итог этого вспомогательного рассмотрения теперь может быть выражен в виде следующего усиления теоремы Левенгейма'): 1) Метод доказательства этого вспомогательногв утверждении позаимствовав нами из работы В. Аккермана: АсМе г ш а п и %. Вецгаяе енш Еп[зсие[бппдзргоыеш бег ша[веша[[зсиеп [па[[с,— Ма![1.

Апп., 1936, 112, № 3, к которой примыкает н изложение Пепнша. Если формула рассматриваемого нами вида ~~,...~[~Д«1...В«еЕ(~„..., те, [„..., «5) выполнима, то формула УГ1...чй.,Е(«1, ..., Ге, ф1(Е1, ..., Уе), ..., фе(Е1, "., Ие)) выполнима в области натуральных чисел для любой разделяющей систел[ы функций ф1(п„..., пс), ..., ф,(п„..., пе). Итак, для любой разделяющей системы функций ф1, мы получаем некоторую формулу [[У1 ' еасе' (51 . ° ° ~ ЕЕ ф1(51 ° ° ~ ЕЕ)~ ° фа(51 '' ЕЕ))~ истинную в области натуральных чисел.

Теперь речь будет идти о том, чтобы найти П1 возможности более простую разделяющую систему функций. Мы рассмотрим систему, определяемую итерацией только одной функции ф от двух аргументов. Эту функцию можно взять достаточно произвольным образом. От нее лишь требуется, чтобы для любых чисел а и Ь выполнялись неравенства ер (а, Ь) ) а и ер(а, Ь) » Ь, а также чтобы каждое ее значение принималось только при единственном наборе значений аргументов. Такой функцией является, например, функция ф(а, Ь)=2'(2Ь+1). А теперь для любого заданного числа 1, отличного от нуля, под ф[(а„..., а[+1) мы будем понимать функцию от 1+1 аргу- мента, определяемую выражением ф(а„ф(ае, ф(аз, ..., ф(а[, и[+1)" ))), в котором функциональный знак ф фигурирует 1 раз. Из перечисленных свойств функции ф(а, Ь) легко вытекают аналогичные свойства и для функции е([[(а„..., а[+,), а именно, что значения этой функции при 1~0 всегда превосходят любой из ее аргументов и что эта функция каждое из своих значений принимает только при единственной системе значений ее аргументов.

Характеристики

Список файлов книги