Гильберт, Бернайс - Основания математики. Теория доказательств (947376), страница 90
Текст из файла (страница 90)
Таким образом, в предположении непротиворечивости форма- лизма (ЕР), мы получаем, что введение посредством формул (А1) предикатйого символа М (и, й) представляет собой некий акт выхода за рамки формализма (7„). Формулы (Ж) имеют вид М (п, 0) 31(п), М(п, 73') (3(1(п) й 117хМ (( (и, х), й)) ~( (3(3(п) й =(хМ(((п, х), й)). 3) Сзь с. 343. ВЫХОД ЗА РАМКИ ТЕОРИИ ДОКАЗАТЕЛЬСТВ [ГЛ. Ч ПриэтомИ(п), Их(п) иИ,(п)суть рекурсиеныеформулы, а((п, т)— рекурсивныи терм, в котором фигурируют только явно указанные переменные.
Следовательно, такого рода схема не может быть общим способом сведена к явным определениям в (У ). С другой стороны, следует отметить, что схема указанного вида, как и примитивная рекурсия, носит характер некоторого определения.. Действительно, для любой цифры 1 оиа дает !Как мы уже убедились в этом для формул (Ь)] некоторую эквивалентность М(п, 1) ат(п), где «т(п) — формула из (Хи).
С друеой стороны, эта схема имеет нефинитный характер, т. е. Она не может быть интерпретирована как способ, позволяющий для любых заданных чисел п и 1 выяснить, имеет ли место М (и, 1). Но в любом случае, если содержательно допустить принцип «1ег1!шп поп да(пг» для целых чисел, эта схема будет представлять собой изображение некоторого рода абстрактного определения двуместного преднката. Значит, выход такой схемы за рамки формализма (Еи) свидетельствует о том, что в формализме (Ев) невозможно полностью формализовать содержательное применение принципа «1ег1[шп поп да1иг» для целых чисел.
Можно даже предполагать, что эта неформальная точка зрения вообще т[е может быть исчерпывающим образом формализована никаким дедуктивным формализмом, удовлетворяющим условию') 6,). Выход определения (З) за рамки формализма (Ев) (в предположении его непротиворечивости) проявляется еще в одном пункте. С помощью символа М(п, й), как мы знаем, получается формальное выражение У[е (и) для предиката «число и является номером некоторой истинной формулы формализма (Х)».
Теперь, опираясь на это формализованное определение, можно дать и формальное доказательство непротиворечивости формализма (Х), В самом деле, с помощью рекурсивных определений для %«(п), рг(п), (д(п), (де(п) и 31(п, /е), которые все в (Ев) сводятся и явным определениям, с помощью определения Й[е(п) (д(п)ЙУх(31(п, х)Й[:е(х) — »Ве(Я(рГ(х)ЙМ(рг(х), 2))), е также фоРмУл (Ь) и сРедств фоРмализма (Еи) можно вывести,— чтб мы здесь лишь упомянем, ие вникая в подробности, — формулы :-(ХЗ»(х, и)-»3)?е (и) Ю[е (п) -» ) 3)1« (3 и), т) См.
с. 354, 4 2! ФОРМАЛИЗАЦИЯ АРИФМЕТИЧЕСКОГО ФОРМАЛИЗМА 4!7 из которых получается формула 'ЗХЕ,(х, и)-» ) Зхбт(х, 3 и). Если бы определение (Ж) сводилось к какому-нибудь явному определению в формализме (Хи), то мы получили бы в (УР) и вывод формулы Вх'Вт(х, и) — » ) ЧХЭ«(х, 3 и), а тем самым — поскольку эта формула принадлежит формализму (Х) — и вывод ее в (Х). По второй теореме Геделя о неполноте отсюда следовало бы, что формализм (Х), а тем более и (Е„), противоречив. Этот путь заодно убеждает нас в том, что для проведения формального доказательства непротиворечивости формализма («,) ие требуется введения связанных переменных какого-либо нового сорта. Следует также обратить внимание на то, что, вследствие представимости рекурсивных функций в системе (Х), в использованной нами схеме определения, имеющей вид М(п, О) И(п), М(п, й') (И,(п) ЙтУХМ(((п, х), й)) ~/ (Из(п)Й=)ХМ(((п, х), й)), рекурсивные формулы И(п), И,(п) и И,(п) могут быль заменены соответствующими формулами т[(п), е[т (и) и р[е(п) из (Х), а кроме того, вместо рекурсивной функции ! (п, т) может быть введена представляющая ее формула з4[(п, т, [) из (Х), которая в рамках (Хв) переводима в равенство ((и, т)=(.
Тем самым схема эта может быть взята в виде М(п, О) Р[(п), М(П, й') (е[,(П)Й т[Хз[[у(Ч)(П, Х, у)-»М(у, й)) [/ (е[з (и) Й пхЗу (ф (и, х, у) Й М (у, и))), где в правых частях эквивалентностей, кроме символа М, фигурируют лишь выражения из (Х). И уже добавление такой схемы определений к формализму Я) дает возможность формально доказать непротиворечивость этого формализма'). 3 а м е ч а н и е. Характерным во внешнем виде этой допплер[- тельной схемы является то, что в выражении для М(п, й') символ М фигурирует со связанной переменной на месте первого т) В данном случае предполагать непротиворечивость (л) не требуется, потому что если »тот формализм противоречив, то для вывода формулы В»Ю, [х, и) -» ~ Зхэ,(х, 3 п) хватает его собственных средств. 14 Д.
Гильберт, П. В«раааа 418 НЕПРОТИВОРЕЧИВОСТЬ АРИФМЕТИКИ 4 ь1 ВЫХОД ЗА РАМКИ ТЕОРИИ ДОКАЗАТЕЛЬСТВ 4!9 !ГЛ. Р аргумента. Как показал Т. Сколем, некоторые более простые схемы этого рода еще могут быть сведены к явным определениям в (Х) '). Благодаря нашему последнему рассмотрению утверждение второй теоремы Геделя о неполноте в применении к формализмам (Х) и (Х„) получает некоторое позитивное дополнение. Однако наши представления относительно возможности формального доказательства непротиворечивости системы (Х) еще ничего не решают в вопросе о том, как обстоит дело с возможностью финитного доказательства непротиворечивости этого формализма. Этим вопросом мы теперь и займемся.
ф 3. Выход за рамки рассматривавшейся до сих пор методической установки теории доказательств.— Доказательства непротиворечивости формализма арифметики а) Рассмотрение вопроса о формализуемости проводившихся до сих пор метаматематических рассуждений. В предшествующем изложении мы установили применимость второй теоремы Геделя к формализмам (Х) и (Х„). Применимость эта, как мы убедились, имеет место в том усиленном смысле слова, что для формализма (Х) не может существовать такого доказательства его непротиворечивости, которое с помощью построенной нами нумерации этого формализма могло бы быть формализовано внутри (Х„). Поэтому, если бы для системы (Х) оказалось возможным какое-либо финитное доказательство непротиворечивости, то оно бы не могло быть формализовано в (У ) с помощью пан!ей нумерации для (Х).
С другой стороны, если мы рассмотрим доказательства различных полученных нами метаматематических теорем с точки зрения возможности их формализации, то убедимся, что ббльшая часть встречающихся в них понятий и умозаключений допускает формализацию уже в рамках рекурсивной арифметики ') (хотя фактическое осуществление такой формализации для большинства доказательств было бы делом в высшей степени утомительным). При этом можно ограничиться первоначальным формализмом рекурсивной арифметики, в котором схемой индукции является '1 См.
5йо1ещ ТЬ. ОЬег д!е хогйсй!йьгЬагйе!! е!и!пег бпгсЬ йе!гпгь!опсп дени!ег!ег гге!а!!опеп ан1 апщгпен«сйе,— Ас!а Бс1, Бьейеф 1937, 8, № 2, 3, Соответственно этому схема рекурсии ч"(й, о) - е (й), Ч' (й, л') Вх (Ч' (х, л) а 2! (й, х, л)), приведенная Бернайсом в его работе: В е г и а у ь Р.
1)пе!Чпеь ро!п!ь емепце1ь бе 1а гпщапгапйегпаисое. — Ь'епье!дпещеп1 Май., 1935, 34, р. 90, еще не пред- стааляег собой примера рекурсии, не укладмвагощейся в рамки формалиама (вв). ') См. с. 271 и далее. обычная (и единственная) рекурсивная схема — схема примитивной рекурсии; кроме того, как мы знаем, эту схему достаточно применять только к одноместным и двуместным функциям. Разумеется, во многих случаях оказывается, что этого формализма уже недостаточно для проведения требующейся нам формализации. Но в этих случаях всякий раз оказывается возможной формализация в (У„). Ряд методов, выходящих за пределы рекурсивной арифметики (в первоначальном смысле этого слова), был рассмотрен нами уже в гл.
ь7П т. 1: Мы имеем в виду определение функций с помощью перекрестных рекурсий, а также некоторые обобщения схемы индукции. При этом мы указывали на возможность формализации этих схем рекурсии и индукции в рамках формализма для арифметики в целом'). Мы вкратце обсудим здесь и некоторые другие типичные примеры этого рода. 1. Как мы показали, в любом формализме, удовлетворяющем определенным условиям, понятие значения выражения, определяющего число„не может быть формализовано с помощью какой- либо функции, изобразимой в самом рассматриваемом формализме '). Можно убедиться, что эти условия выполнены для формализма рекурсивной арифметики, и таким образом получается, что значение рекурсивного пгерма без переменных в его зависимости от номера этого терма не может быть изображено (на основе нашей нумерации рекурсивной арифметики) никакой рекурсивной (т.
е. определяемой примитивными рекурсиями) функцией. Чтобы убедиться в выполнении упомянутых предположений, можно взять следующую нумерацию формализма рекурсивной арифметики: Для свободных переменных, для символов исчисления высказываний и для арифметических символов О, ' и = изображение берется тем же самым, что и в нумерации, построенной нами для формализма (У )'), а для функциональных знаков, вводимых рекурсиями, изображение строится способом, указанным ниже. Если ( — какой-либо одноместный функциональный знак, вводимый рекурсией ((0)=п, ((а')=Ь(п, ((а)), то номер выражения ((с) в его зависимости от номера аргумента с мы будем изображать функцией б 1"и, причем если 1 и 1 суть номера выражений а и Ь(а, 6), то в качестве п мы возьмем значение выражения 2 3!.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
