Гильберт, Бернайс - Основания математики. Теория доказательств (947376), страница 92
Текст из файла (страница 92)
»711 т. 1 раозуждение») мы сделали заключение, что это доказательство может быть распространено и на ограниченную схему индукции (т. е. на схему индукции, применяемую к формулам без связанных переменных), Действительно, для этого достаточно показать что в любом выводе нумерической формулы, осуществляемом средствами рассмотренного формализма о добавлением ограниченной схемы индукции, после исключения формульных переменных результирующие формулы всех применений схемы индукции являются верифицируемыми, Это, однако, доказывается с помощью полной индукции: мы показываем, что если результирующие формулы первых 1 применений схемы индукции являются верифицируемыми, то и результирующая формула (1+ 1)-го применения схемы индукции -в предположе- 0 См. с.
224. ») См. гл. 11, с. 75 — 77, ») См. т. 1, с. 364 — 565. иии, что таковая В рассматриваемом выводе имеется, — тоже является верифицируемой. А теперь посмотрим, как это индуктивное рассуждение может быть изображено с помощью нумерации рассматриваемого формализма. Рассматриваемый арифметический формализм, расширенный присоединением ограниченной схемы индукции, мы обозначим посредством (Е«).
Имеющаяся у нас нумерация формализма (ХР) автоматически порождает некоторую нумерацию этого формализма. Число применений схемы индукции, содержащихся в данном выводе в формализме (Х,), в его зависимости от номера списка формул, образующего этот вывод, изображается некоторой рекурсивной функцией й,(гп). Мы можем определить рекурсивную функцию й»(т, й), значение которой для числа а, являющегося номером некоторого вывода в (Е,), и для числа 1, меньшего й,(а), будет изображать номер (в рассматриваемой нумерации) результирующей формулы (1+ 1)-го входящего в этот вывод применения схемы индукции, так что если ~е — номер какого-либо вывода в (Х,), содержащего т применений схемы индукции, то 5»(Е1, О), ..., 5»(е«, т — 1) будут номерами результирующих формул этих применений схемы индукции.
Затем с помощью некоторой рекурсивной формулы Й (т) может быть изображено высказывание «число и является номером некоторого списка формул, представляющего собой вывод в формализме (Х,), осуществленный без использования формульных переменных», а с помощью другой рекурсивной формулы 2(а, Ь) — высказывание «числа а и Ь являются номерами некоторых формул из (Е») и формула с номером Ь получается из формулы с номером а путем замены каждой свободной индивид.
иой переменной некоторой цифрой». И, наконец, с помощью некоторой рекурсивной формулы И (а) может быть изображено высказывание «число а является номером некоторой формулы без переменных такой, что после вычисления всех входящих в нее функциональных выражений она становится истинной нумерической формулой». А теперь, с помощью перечисленных выше рекурсивных функций и формул, высказывание «в любом выводе в формализме (Х,), не содержащем формульных переменных, результирующая формула любого входящего в него применения схемы индукции является верифицируемой» изобразится формулой Й (т) й й ( й, (т) й 2 (й, (т, й), с) — Я (с), которая переводима в некоторую рекурсивную формулу Р (т, й, с).
Высказывание «для любого числа Й, меньшего и, имеет меото отношение «7(т, й, с)» тоже может быть изображено при помощи некоторой рекурсивной формулы Л,(гп, п, с). 427, НЕПРОТИВОРЕЧИВОСТЬ АРИФМЕТИКИ 426 ВЫХОД ЗА РАМКИ ТЕОРИИ ДОКАЗАТЕЛЬСТВ ~ГЛ. Р Но теперь для формальной реализации упомянутого индуктивного рассуждения требуется выразить заключение «если в выводе с номером «и все применения схемы индукции по п-е включительно имеют верифицируемые результирующие формулы, то применения схемы индукции по (и+1)-е 'включительно тоже имеют верифицируемые результирующие формулы», или — с помощью рекурсивной формулы ф, (л», й, с) — «если для любых чисел «и и п отношение Й»(т, и, с) имеет место для всех чисел с, .
то для тех же самых чисел «и и и и для всех чисел с будет иметь место отношение 4З,(т, п', с)». Это гипотетическое отношение, которое в рамках финитного рассмотрения допустимо как способ вывода следствия, хотя и не как финитное предложение, в рамках рекурсивной арифметики не может быть изображено какой-либо формулой. Но в рамках формализма (ЕР) оио изображается формулой »«х«»,(л», п, х)-э Чх<»,(л», п', х). Остается нерешенным вопрос о том, можно ли доказательству, которое здесь представлено схематически в довольно сыром виде, придать такую форму, чтобы оказалась возможной его формализация при помощи какой-либо из схем расширенной таким образом рекурсивной арифметики.
Вообще же надо отметить, что при формализации финитных рассуждений в системе (Х„) ббльшая часть характерных черт финитной аргументации теряется. Это объясняется тем, что формализм (Е„) ие рассчитан на то, чтобы как-то различать конструктивные и экзистенциальные рассмотрения, б) Устранимость принципа «тег11шп поп <)а(пг» при исследовании непротиворечивости системы (Х). Различные выборочные пробы, произведенные нами в процессе исследования возможности формализации полученных к настоящему времени метаматематических теорем и их доказательств, позволяют нам заключить, что методы теории доказательств, применявшиеся нами до сих пор, хотя частично и выходят за пределы рекурсивной арифметики, тем ие менее, как нам кажется, они укладываются в рамки понятий и способов умозаключений, изобразимых средствами формализма (Х„). В этом обстоятельстве мы можем усмотреть известные объяснения и причинам, по которым нам не удалось доказать с помощью этих методов непротиворечивость формализма (2).
Действительно, такое доказательство, как было установлено, непременно потребовало бы привлечения каких-либо способов рассуждения, выходящих за пределы формализма (ЕР). А теперь перед нами возникает вопрос о том, могут ли финитные методы вообще выйти за пределы формализуемых в (ЕР) способов рассуждений.
Этот вопрос в том виде, как он только что сформулирован, поставлен, конечно, неточно, потому что понятие <финитности» было введено нами не в качестве четко описанного термина, а лишь в качестве названия для некоторой методической установки, которая хотя и позволяет квалифицировать одни конкретные понятия и рассуждения как определенно финитные, а другие- как определенно нефинитные, но все-таки не указывает никакой точной границы между теми из них, которые удовлетворяют требованиям финитности, и теми, которые этим требованиям не удовлетворяют. С типичным сомнительным в этом отношении случаем мы встретились при обсуждении вопроса о допустимости предложений типа всеобщности в качестве посылок.
В этом случае мы избежали трудности путем проведения различия между предложениями и правилами умозаключений'). Однако во многих случаях это выглядит неестественным, и нам остается просто-напросто признать, что мы вынуждены сделать границы финитных рассмотрений несколько размытыми. Первоначальное более узкое понятие финитного высказывания в области арифметики состоит в том, что в качестве финитиых арифметических высказываний допускаются лишь такие высказывания, которые либо сами изображаются в формализме рекурсивной арифметики с добавлением, быть может, некоторых символов для конкретных вычислимых арифметических функций (одного или нескольких аргументов), однако без использования формульных переменных, либо имеют некоторую усиленную интерпретацию с помощью высказываний, изобразимых в таком формализме.
К высказываниям первого рода принадлежат, в частности, высказывания вида «если имеется число х со свойством 21(х), то имеет место 6». Действительно, всякое такое высказывание (если переменная а не входит в 3) изобразимо формулой 6 (а) — 3. Примерами высказываний второго рода являются высказывания вида «для любого числа х существует число у такое, что 2((х, у)». Для всякого такого высказывания в нашем распоряжении имеется усиленная версия в виде высказывания, ивобразимого формулой «( (с, «р (с)), где «р (с) — конкретная вычисл имая функция.
Примерами высказываний, не являющихся финитными в указанном смысле, служат предложения, содержащие предложения типа всеобщности в посылке. Однако для формализации ряда общих результатов теории доказательств желательно было бы допустить в качестве теоре»(( и предложения только что упомянутого типа, — например, предложения, в посылках которых стоят утверждения о верифици- ') См. в. 225, «также с. 424 я далее. 429 ВЫХОД ЗА РАМКИ ТЕОРИИ ДОКАЗАТЕЛЬСТВ 1гл. у НЕПРОТИВОРЕЧИВОСТЬ АРИФМЕТИКИ 4 »1 руемости тех или иных формул илн же о вычислимости тех или иных функций. Однократный акт такого рода не выглядит нарушением основных методических идей финитной теории доказательств. Но совершив такой шаг однажды, мы приходим к необходимости пойти в этом направлении и дальше.
Дальнейший, уже упоминавшийся шаг такого рода заключается в том, чтобы утверждения с предложениями типа всеобщности в посылках в свою очередь использовать в качестве посылок в индуктивных рассуждениях. У нас нет четкой исходной точки зрения для решения вопроса о том, какие методические расширения в указанном направлении являются еще допустимыми (при условии, что мы намерены придерживаться основных тенденций теории доказательств). Во всяком случае, имеется возможность с помощью такого рода расширений выйти за границы формализуемых в (Е„) способов умозаключений без использования типично нефийитных рассуждений.
Таким способом даже удается дать одно очень простое доказательство непротиворечивости системы (Е). К этому доказательству нас приводит следующее рассуждение: Характерной чертой типично нефинитных рассмотрений, применяемых в области арифметики, является использование Отрицания в смысле контрадикторной противоположности в применении к произвольным высказываниям, построенным с помощью понятий «все», «существует» и связок исчисления высказываний. При формализации арифметических доказательств в формализме (Х) такое употребление отрицания изображается средствами исчисления высказываний, а в основных формулах и в схемах для кванторов, а также в аксиоме индукции отрицания нет вообще. Пользуясь теперь исчислением высказываний в его аксиоматической форме, мы можем формализм (Х) ограничить таким образом, чтобы оказались изобразимыми только такие способы умозаключений, которые не зависят от предположения атом, что для любого высказывания существует другое высказывание, являющееся его контрадикторной противоположностью ').
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
