Гильберт, Бернайс - Основания математики. Теория доказательств (Гильберт Д. - Основания математики и прочие работы)

Д. ! ИЛЬБЕРТ П. БЕРНАЙС Перевод с немецкого Н. М, НАГОРНОГО Под редакцией С. И. АДЯНА МАТЕМАТИЧЕСКАЯ ЛОГИКА И ОСНОВАНИЯ МАТЕМАТИКИ МОСКВА «НАУКА» ГЛАВНАЯ РЕЛАКИИЯ ФИЗИКО-МАТЕМАТИЧЕСКОЙ ЛИТЕРАТУРЫ 1Я32 ОСНОВАНИЯ МАТЕМАТИКИ ТЕОРИЯ ДОКАЗАТЕЛЬСТВ МОСКВА «НАУКА» ГЛАВНАЯ РЕЛАКНИЯ ФИЗИКО. МАТЕМАТИЧЕСКОЙ ЛИТЕРАТУРЫ $922 2232 Г47 УДК 517.11 ОГЛАВЛЕНИЕ 9 11 Предисловие ко второму изданию Г л а а а 1. Метод исключения сказанных переменных ири помощи гильбертова е-симиола 17 Г л а а а 1!.

Исследование арифметики ири помощм связанных с е-символом методов теории доказательстя ..., .......... 74 й 1. Применение нп-теоремы к арифметике ....., $ 2. Распространение первой е-теоремы аа общую аксиому раненстаа а) Подготовительные соображения; оснонной тип; формулы е-раненстна б) Совместное устранение критических формул и формул е-разенстаа н) Усиленный иариаит первой г-теоремы и нп-теоремы...., 2 3. Причины, препятстиуюшне распространению процедуры устра. пения з-снмзолои на неограниченную схему индукции.

Форма. лизация принципа индукции с помощью второй формулы для е-симиола, Переход к первоначальному гильбертоискому подходу $4. Первоначальный гильбертозский подход к проблеме исилючения з-симиолои и его дальнейшее развитие 74 82 82 93 109 ф Перевод нв руескна язык Нвдвтельство Наука Главна» редвнвкя энлнконвтенвтнчесноа лнтервтуры, нмз 113 1702020000 — 078 à — — — 54.82 053(02).82 124 Предисловие редактора русского перевода Предисловия авторов к первому изданию $ 1.

Процедура символьного решения экзистенциальных 4 2. Гильбертов з-символ и з-формула 4 3. Доказательстио первой е-теоремы а) Подготовка б) Гильбер~озский подход . и) Типы комбинирования а-симиолоз; степень и ранг г) Устранение критических формул и общем случае д) Обобщение результата $4. Доказательства непротиворечивости а) Одна общая теорема о непротиворечивости б) Приложение к геометрии формул 17 37 37 40 з-терма 43 47 51 55 55 61 оглдвлпыие ОГЛАВЛЕНИП 370 38! 401 4!8 418 167 167 176 !89 2!2 230 457 457 462 471 473 230 2.'15 245 248 259 489 505 512 512 520 532 321 321 321 337 352 362 362 367 а) Простейшие частные случаи б) Подготовка к рассмотрению общего случая в) Реализации гильбертовского подхода в случае э-термов ранга ! г) Построение последовательности общих замен в общем случае д) Построение резольвенты в случае, когда все критические формулы являются формулами первого рода....,......

е) Несостоятельность рассмотренного метода в случае кршнче- ских формул второго рода с произвольным рангом. Дополнение к предыдугцсму результату ж) Использование полученного результата в нп-теореме Г л а в а П 1. Использование а-символа в научении логического формализма 4 1. Вторая е-теорема 9 2.

Распространение второй э-теоремы на общую аксиому равенства. Сь«ежные проблемы й 3. Теорема Эрбрана 4 4. Критерии опроверн<имости в чистом исчислении преднкэтов $ 5. Применение полученных критериев к проблеме разрешимости а) Общие сведения о выполнимости. Теоретико-модельная сколемонская нормальная форма б) Теорема Левенгейма н теорема Геделя о полноте в) Учет требований фнннтной точки зрения г) Один пример д) Теоретико-модельные нормальные формы Г л а в а !Н.

Метод арнфметиэацин метаматематики в применении к исчислению преднкатов $ !. Арифметиээцня метаматематнки исчисления преднкатов и одяа ее конкретная реализация а) Нумерация б) Вспомогательные средства рекурсивной арифметики в) Арифмстнзацпя понятия формулы г) Арифметнзация распределений истинностных значений д) Арифметизэция понития вывода 4 2. Применение метода арифметизацнн к теореме Геделя о полноте э) Формализация доказательства теоремы о полноте б) Усиление выполнимости до выводимости Г л а в а У. Причины, вызывающие необходимость расширения методических рамок теории доказательств 4 !. Границы иэобразимости и выводимостн в дедуктивных форма.

лизмах а) Антиномия лжеца; теорема Тарского о понятии истинности; парадокс Ришара б) Первая теорема Геделя о неполноте в) Вторая теорема Геделя о неполноте 9 2. Формализованная метаматематика арифметического формализма а) Описание одного арифметического формализма ....... ° б) Построение нумерации формализма (Еи) .......

° ° ° ° ° 124 129 140 146 150 !56 !6! 265 265 271 276 282 287 297 297 308 в) Проверка условия бз) для формализма (Еи) и построенной для него нумерации .. г) Проверка условий на выводимость ........,, ...,, д) Распространение второй теоремы Геделя о неполноте на формализм (Е). — Формулировка определения истинности для этого формализма й 3. Выход эа рамки рассматринавш«йся до сих пор методической установки теории доказательств. †)(окаэательства непротиво.

речивости формализма арифметики а) Рассмотрение вопроса о формализуемости проводившихся до сих пор метаматематическнх рассуждений . б) Устраннмость принципа «1егНшп поп да(цгэ при исследовании непротиворечивости системы (2) в) Трансфинитная индукция одного частного вида и ее приме. пенис в генцеповском доказательстве непротиворечивости системы (Е) . П н ложен и е 1. Сведения об исчмсэенин предикатов н приммквющнх рн к нему формализмах й 1. Чистое исчисление предикатон й 2.

Применение исчисления предикатов к формализованным системам аксвом. «-правило. Арифметические формализмы ( 3. Теоремы об исчислении предикатов 9 4. Исчисление предикатов без правила подстановки П р н л о ж е н и е П. Уточнение понятия вычислимой функции и теорема Черча о проблеме разрешимости . 3 1. Понятие регулярно вычислимой функции, Вычисление в фор. мализые (2«) 4 2.

Обшерекурсивные и регулярно вычислимые функции. Нормальное представление. Вычисление в формализме (Хээ). Применение канторовской диагональной процедуры й 3. Невозможность общего решения проблемы разрешимости для исчисления прединатов П р и ложен н е П1. 0 иеноторых фрагментах исчисления высказываний и нх дедуктивном описании с помощью схем ь' 1. Позитивно тождестненные импликативные формулы....... 9 2. Позитивно тождественные 1-К-формулы.......,..... 9 3. Тождественные 1-К-Н-формулы 71 Р и л о ж е н н е Г«г.

Формализмы для дедуктивного построении анализа й !. Описнпие одного формализма й 2. Построение арифметики э 3. Теория положительных действительных чисел й 4. Теория действительных чисел. Замечания по поводу дальнейшей формализации анализа 9 5. Теория вполне упорядоченных множеств целых чисел й 6, Модификации рассмотренного формализма. Исключение в-снмвола й 7. Использование связанных офрмульных переменных ......

° 546 551 556 568 573 579 588 оглавления 598 598 624 4 1. Доказательство Кальмара $ 2. Доказательство Аккермана Алфавитный указатель 647 РАСШИФРОВКА ОТСЫЛОК ИЗ Т. 1 1. с. 505 н далее (см, т. 1, с. 172). 2, с, Ю6, сноска ! (см. т. 1, с. 187).

3. с. 109 и далее (см. т. 1, с. 202), 4. с. 233 — 235 [см. т. 1, с. 203). 5. с 489 (см. т. 1, с. 390). П р и л о ж е н н е (г, Доказательства непротиворечивости арифметического формализма ПРЕДИСЛОВИЕ РЕДАКТОРА РУССКОГО ПЕРЕВОДА Настоящая книга представляет собой перевод второго тома известной двухтомной монографии Д. Гильберта и П.

Бернайса «Основания математики». Перевод выполнен со второго немецкого издания, вышедшего в 1970 г. Второй том написан как продолжение первого. Однако его можно читать независимо, так как в Приложении 1 приводится конспективное изложение содержащихся в первом томе понятий н результатов, используемых во втором томе. Читатель, не знакомый с первым томом, должен начать чтение книги с Приложения 1. Перевод первого тома опубликован издательством «Наука» в 1979 г.

с подзаголовком «Логические исчисления и формализация арифметики», О достоинствах монографии Гильберта и Бернайса и о ее роли в развитии идей и методов математической логики уже говорилось в моем предисловии к русскому изданию первого тома. Все, что было сказано о книге в этом предисловии, относится в полной мере и ко второму тому. По предложению издательства для второго тома был введен подзаголовок «Теория доказательств», который полностью соответствует содержанию тома Во втором томе подробно излагаются и обсуждаются результаты теории доказательств, относящиеся к логическим исчислениям и к формализованной арифметике. Это известная теорема Эрбрана, дающая важный критерий выводимости формул в исчислении предикатов, теорема Черча о невозможности алгоритма, распознающего выводимые формулы исчисления предикатов, теорема Геделя о неполноте арифметических исчислений и различные доказательства непротиворечивости формализованной арифметики.

Особую ценность представляет подробное обсуждение используемых при доказательстве непротиворечивости арифметики средств, выходящих за рамки первоначальной финитной точки зрения Гильберта. В книге проводится мысль, что привлечение новых достаточно надежных средств для доказательства непротиворечивости формализованной арифмети"и ~ледует рассматривать не как отказ от первоначальных ме- го ПРЕДИСЛОВИЕ РЕДАКТОРА РУССКОГО ПЕРЕВОДА тодических установок Гильберта, а как их расширение и уточнение. В Приложении П~ приводятся дедуктивные системы, в рамках которых можно выполнить дедуктивное построение математического анализа, но вопрос о непротиворечивости анализа в книге не рассматривается.

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

Особенно велико ее влияние на развитие алгебры. Так, например, многие конкретные исследования, связанные с доказательством невозможности вывода тех или иных соотяошений в различных алгебраических системах, заданных с помощью тождественных или определяющих соотношений, можно рассматривать как фрагменты теории доказательств, развитой для алгебраических систем данного класса. Нет сомнений в том, что влияние идей теории доказательств на развитие математической науке будет расширяться и в будущем. Для широкого круга читателей, интересующихся вопросами оснований математики, книга Гильберта и Бернайса «Основания математики» привлекательна тем, что в ней основополагающие идеи теории доказательств излагаются более обстоятельно и менее формализованно, чем где-либо в другом месте.

Можно думать, что выход в свет книги Гильберта и Бернайса на русском языке будет с удовлетворением встречен в нашей стране не только специалистами по математической логике, но также и всеми квалифицированными математиками, которые в той или иной мере интересуются вопросами Оснований математики, ролью математики в современной науке, глубокими проблемами, стоящими перед математикой и математиками независимо от их узкой специальности. Москва, анвар» 1981 д С. Адян ПРЕДИСЛОВИЯ АВТОРОВ К ПЕРВОМУ ИЗДАНИЮ Настоящ " нй том завершает изл ложение теории доказательств, П. Б йсом несколько лет тому начатое мною совместно с .