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

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

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

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

Далее, приняв ранее уже использованное предположение, что в формализме Р символы для связок исчисления высказываний, а также штрих-символ и символ равенства совпадают с симво- ») Один очень проарачный формализм »того рода, нродолжиощий набросив У. В. Куайна (см. О и! п е Ж. Н. вег-гнеогенс $оипйабои» аког!ой1с: — Ю. ЗущЬо!!с Еой1с, 1936, Ц а особенности см. с. 45, 46) и существенно испольаугощий е.симаол, построен Аккерманом а его работе Аснегщапп%. Мепйеищеогецасйе рейганомика оег Г.ой1«.

— Маси. Аин., 1937, Ый, № 1. а) См. с, 322 и далее, лами, которые ми»обычно используем для них, и распространив это предположение на символы О, ( и (, мы приходим к тому, что вместо допущений а) и в) можно Рзять следующее допущение: а,) Формализм Р содержит термы и формулы рекурсивной арифметики '), не считая, быть может, тех, в которых содержатся формульные переменные. Каждая формула без формульных переменных, выводимая в рекурсивной арифметике, выводима и в Р, и каждый выполнимый средствами рекурсивной арифметики переход от одной формулы из Р к другой выполним и в Р. Допущение б) — после того, как в предшествующих рассмотрениях мы познакомились со способами его использования,— мы сформулируем несколько уже, а кроме того, мы присоединим к нему новое предположение о рекурсивной изобразимости отношения «число лч является номером некоторого вывода формулы с номером а».

В итоге мы приходим к следующей формулировке. бг) Существует взаимна однозначная нумерация выражений формализма Р натуральными числами, обладающая следующими свойствами: 1. Номер выражения, получающегося из выражения К с номером г в результате повсеместной замены числовой переменной а цифрой (, изображается — в его зависимости от г и ( — значением некоторой двуместной рекурсивной функции 6(й, г) при значениях ее аргументов, равных г и (. 2.

Высказывание «число т является номером некоторой последовательности выражений из Р, являющейся выводом выражения с номером и» с помощью нумерации конечных последовательностей выражений из Р, получающейся из нумерации выражений из Р путем использования разложения целых чисел )2 на простые множители, изображается двуместным рекурсивным предикатом и, тем самым, в формализме рекурсивной арифметики оно выражается некоторой рекурсивной формулой') Ю(пг, и), у которой и и и суть единственные входящие в нее переменные. А теперь, чтобы на основе предположений а,) и бг) получить формализацию нашей модифицированной антиномии лжеца, достаточно установить, что в Р имеется такая формула, которая изображает утверждение о своей собственной невыводимости (в формализме Р); т. е.

если й является номером этой формулы, то она изображает высказывание: «каково бы ни было число лг, оно не является номером какого-либо списка формул, представляющего собой вывод формулы с номером 9». Так как мы не предполагали, что формализм Р содержит квантор всеобщности, то для только что приведенного высказывания, являющегося предложением типа всеобщности, мы возьмем такое ') См. с. 27! и далее, а) См. с. 272.

ВЫХОД ал РАМКИ таОРИИ ДОКАЗАтяяьбт~,х ПЛ. Н его изображение, в котором всеобщность будет:формализоваться с помощью свободной числовой переменной. л При этом мы будем опираться на вооходящий к Геделю и ранее уже применявшийся метод использования функции б(я, 1). Мы строим формулу 16(т, б(а, а)), которая, согласно предположению а,), является формулой формализма Р.

Пусть эта формула имеет номер р. Ввиду характеристического свойства функции б(й, 1) значение б(р, р) является номером формулы 16(т, б(р, р)). Если этот номер равен с, то равенство б(р, р)-ц выводимо в Р, и поэтому формула )6(т, б(р, р)) переводима в формулу 16 (т, о). Формула ) 6(т, Ч) представляет собой формализацию высказывания «каково бы ни было число т, оно не является номером вывода формулы с номером о» илн, короче, «формула с номером о невыводимаж Терм б(р, р) является выражением, определяющим цифру ц.

Следовательно, только что упомянутое высказывание формализуется и формулой 1 6 (т, б (р, р)). Так как, с другой стороны, эта формула имеет номер 4, то она является искомой формулой, формализующей утверждение о своей собственной невыводнмости. А теперь уже можно рассуждать следующим образом. Допустим, что формула 16(т, с) выводима в Р, Тогда выводима и формула ) 6(т, б(р, р)), т. е. формула с номером о. Следовательно, можно указать список формул, являющийся выводом . формулы с номером е, Если 1 является номером некоторого такого списка, то имеет место отношение 6(1, 4), которое является нумерически устанавливаемым равенством (или соответственно может ' быть преобразовано в такое равенство), и тогда формула 6(1, ч) выводима в Р.

Так как, с другой стороны, согласно сделанному предположению, выводима формула 16(т, 4)„то, согласно предположению а,), выводима и формула ) 6(1, 4). Тем самым в формализме Р появляется противоречие. То же самое следствие получается н из предположения, что отношение 6(1, а) имеет место для какой-либо цифры 1. Действительно, если это отношение выполняется, то, с одной стороны, ' в Р выводима формула 6(1, с). С другой стороны, в этом случае 1 является номером некоторого списка формул, представляющего, 4 1! ГРАницы изовРАзимОсти и Выводимости 841 собой вывод формулы с номером 4, т, е.

формулы 16(т, б(р, р)). Следовательно„эта формула выводима в Р, а значит, выводима н формула 16(т, д), из которой выводима формула 16(1, Ч). Если мы теперь еще заметим, что, согласно предположению а,), для любой цифры 1 выводима либо формула 6(1, о), которая является нумерической, либо ее отрицание ) 6(1, ц) и что одновременно с выводимостью формулы 6(1, ц) имеет место отношение 6(1, о), а одновременно с выводимостью формулы 16(1, 4) имеет место отношение ) 6(1, а), то получим следующий результат: если формализм Р непротиворечив, то для любой цифры 1 имеет место отношение )6(1, ц) и формула )6(1, ц) выводима в Р, между тем как формула 16(т, а) в Р невыводнма. То, что отношение 16(1, с) имеет место для любой цифры 1, означает, что формула ) 6 (т, о) верифицируема.

Будучи рекурсивной, эта формула переводима в некоторое равенство ((т) = О, где 1 — рекурсивно введенный функциональный знак с одним аргументом. Тем самым получается следующая Тес р ем а. Для любого непротиворечивого дедуктивного формализма Р, удовлетворяндцего условиям а,) и б,), можно указать такую одноместную рекурсивную функцию 1, чгпо формула ((т)=О невыводил«а в Р, хотя она и является верифицируемой, так что для каждой цифры 1 в Р выводимо равенство 1(() О. Эту теорему, которую Гедель получил указанным здесь способом, мы будем называть первой теоремой Геделя о неполноте. В геделевской формулировке фигурирует не сама эта теорема, а некоторое извлекаемое из нее следствие, которое говорит о существовании таких арифметических предложений, которые в рассматриваемом формализме Р являются формально н еразрешимыми, При этом под формально неразрешимым в Р предложением понимается такое предложение, которое изображается в Р некоторой формулой без свободных переменных, причем ни сама эта формула, ни ее отрицание невыводимы в Р').

з) Содержащееся в этом определении требованне ограничиваться формуламя без свободных переменных является обязательным, потому что црн нзображеннн предложений типа всеобщности с помощью формул с одной нлн несколькими свободными переменными отрицание такого предложения не изображается отрнцаннем соотвегстзующей формулы. Формула со свободнымн переменнымн, невыводнмая з данном формализме Вместе со своим отрицанием, еще может н не изображать формально неразрешимое в»том формализме предложение.

Так, напрнмер, в фсрмалнзме арифметики (если он ненротвворечяв) невыводнмы ня формула а=о, нн формула а ~ О. Формулу а=о можно считать изображением ВЫХОД ЗА РАМКИ ТЕОРИИ ДОКАЗАТЕЛЬСТВ, 1,гл. ч Для получения упомянутого следствия мы должны дополнительно предположить, что формализм Р содержит квантор всеобщности вместе с относящимися к нему формальными способами умозаключений, так что если гг((а) является формулой из Р, не содержащей связанной переменной Е, то УЕЛ(у) также является формулой из Р, а кроме того, схема формул гУЕй! (Х) -~- 31 (а) является основной или выводимой, а схема (гх) — основной или производной схемой в Р.

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

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