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

Д. ГИЛЬБЕРТ П. БЕРНАЙС Перевод с немецкого Н. М. НАГОРНОГО Под редакцией С. И. АДЯНА МАТЕМАТИЧЕСКАЯ ЛОГИКА И ОСНОВАНИЯ МАТЕМАТИКИ МОСКВА »НАУКА» ГЛАВНАЯ РЕДАКЦИЯ ФИЗИКО-МАТЕМАТИЧЕСКОЙ ЛИТЕРАТУРЫ 1979 ОСНОВАНИЯ МАТЕМАТИКИ ЛОГИЧЕСКИЕ ИСЧИСЛЕНИЯ И ФОРМАЛИЗАЦИЯ АРИФМЕТИКИ МОСКВА «НАУКА» ГЛАВНАЯ РЕДАКЦИЯ ФИЗИКО МАТЕМАТИЧЕСКОЙ ЛИТЕРАТУРЫ 1979 22.12 Г 47 УДК 517.11 ОГЛАВЛЕНИЕ 11 17 19 20 23 23 23 26 29 31 31 32 35 33 38 39 45 45 43 51 53 55 55 56 59 59 йр перевод яа русский явмн, Главная редакяяя фяэвко-матежвтячсснай натер«туры явдат«лье«за «наука», 1919 20203 — 145 Г 053»02)-79 68-79 1702020000 Предисловие редактора русского перевода Предисловие ко второму иадакию . Предисловие Гильберта к первому издаипю Предисловие к первому издавию . Г л а в а !.

Проблема вевротиворечивости в аксиоматвчесивх исследоваииях вак логическая проблема разрешимости 5 1. Формальная вксиоматика 1. Отиопгевве формальной аксиоматики к содержательной; вопрос о иепротиворечивости; арифметиэация 2. Пример: аксиомы геометрии 3. Касто логический подход к аксиоматике . 5 2. Проблема раврешимости 1. Общезначимость и выпелиимость .

2. Распоэиававие в случае конечных иидивидвых областей 3. 51етод построевия модели $3. Вопрос о вепротиворечявости в случае бескоиечиой индивидвой области 1. Формулы, иевыполииыые в колечком; натуральный ряд как модель 2. Проблематика бесконечного 3. Установление иепротиворечивоств как доказательство иевоэможиоств; метод арифметиэацви . Г л а в а 11. Элементарная арифметика.

Фвивтвый способ рассуждевий и его граю«цы . 1 1. Рассуждения иа иктуитивиом уровие и их ярвмеиевие валемеитарвок арифметике . 1. Понятие цифры; отиошеиие порядка; сложение . 2. Закоиы арифметических действий; полвая ивдукция~ умиожевие; делймосттд простыв числа 3. рекурсивные опредедевия 4. Одно доказательство вевоаможвоств $2. Дальнейшие примеиевия ивтувтиввых рассуждений 1. Отвошеиие арифметики к учению о количестве 2. Формальная точка зревия в алгебре $3. Фивитвая точка зрения; выл«од эа ее пределы в области арифметики 1. Логическая характерпэация фииитвой точки вревия 2. «Тег«шш поп да«пг» для целых чисел; принцип ваимевьшего числа 1 4. Пефииитвые методы в аиалиэе 1.

Раэличиые определения действительного числа ОГЛАВЛЕНИЕ ОГЛАВЛЕНИЕ 144 144 147 156 67 68 74 74 74 77 80 164 172 172 188 191 85 191 194 202 99 103 103 209 209 106 112 120 226 120 235 239 128 128 239 130 134 141 2. Верхняя грань чпслозой последовательности; верхняя грань мио "кества чисел 3. Принцип выбора 1 5. Исследования, направленные на непосредственное финптиое построение анализа; возврат к прежней постановке проблемы; теория доказательств Г л а в а 1П. Формализация процесса логического вывода 1: Исчисление высказываний 1 1. Теория пстивносткых функций 1.

Истпиностные функции и их таблицы 2. Заменлиосттб правила замены 3. Примеры заменимости 4. Двойствеппостгд конъюнктпвная и дизъювктявиая нормальные формы; тождественно истинные выражения; распознающая процедура 5. Совершенная нормальная форма; распознавание заменимости; примеры 1 2. Применение теории истинностных функций к логическому выводу; формализация умозаключений в логике высказываний с помощью тождественно истинных выражений, правила подстановкп и схемы заключения 1 3.

Дедуктивная логика высказьгвав1ш 1. Постановка задачи 2. Одна система исходных формул для дедуктивной логики выскааываний; полнота атой систеыы 3. Позитивная логика; регулярные имплпкатпвные формулы; поавтнвно тождественные импликативные формулы; возможные упрощения $4. Докааательства неаависпмости, проводпмые методом сценок 1. Логическая интерпретация как оценка; общий метод 2.

Доказательство независимости рассматриваемой системы исходных формул; еще одно доказательство независимости 3. Применение метода оценок к вопросу о аамене формул схемами 6 5. Возврат к рассмотренному в 1 2 способу формалпзацпп вывода; сокращенные правила; замечание, касающееся противоречпвостп системы Г л а з а 1У.Формалиэацняпроцессавывода П: Псчислеииепредикатов 1 1. Введение индивпдных переменных; понятие формулы; правило подстановки; пример; параллель с содержательными рассуждениями 4 2. Связанные переменные и правила для кзапторов всеобщности п существования 1. Недостаточность свободных переменных 2.

Введение связанных переменных; кзанторы всеобщности п существования; правило переименования переменных; предотвращение неоднозначностей; обобщение понятия формулы и правила подстановки . 3. Эвристическое введение правил для квавторов всеобщности к существовании; содержательный смысл формул и схем 4. Окончательная формулировка правил исчйсления лредикатов; изображение форм категорических суждений; случай пустой ипдивидной области 1 3. Выводимость 1. Некоторые производные правила 2.

Вывод некотормх форыул 1 4. Вопросы систематики 1. Понятия 1-тождественной формулы к формулы, тождественной з конечиом; дедуктивная замкнутость совокупности 1-тождественных формул; непротиворечивость исчисления предикатов; вопросы полнотьг 2. Экскурс в теоретико-множественную логику предикатов; предварительные замечания к вопросу о полноте; проблема разрешимости и ее уточнение с дедуктивной точки зрения 1 5. Изучение формализма исчисления предпкатов 1. Понятие переводимости; производные правила 2.

Приведение формул к предваревному виду; примеры; описакие разрешимых случаев проблемы разрешимости с помощью предваренной нормальной формы 3. Разложение формул одноместного исчислении предикатов в примарные формулы; пример 4 6. Дедуктивное равенство и дедукционная теорема 1. Повятие дедуктивного равенства; два существенных случая дедуктивного равенства; переводимость и дедуктивное равенство . 2. Дедукцяониая теорема 3.

Применения дедукционпой теоремы: сведение вопросов, связанных с аксиоматвкой. к вопросам выводимости формул з исчислении предикатов', рассмотрение одного распространенного способа умозаключения 4. Дедуктивное равенство произвольной формулы подходящей сколемозской нормальной форме, а также нормальной дкзъюикции; упрощение этого перехода Г л а в а т. Исчисление предикатов с равеметвом. Полнота одноместмого исчисления предикатов $1. Расширенный формалвам 1. Знак равенства;иаображепяе высказываний о количестве; аксиомы равенства и формальные свойства равенства 2. Применение аксиом равенства к различным преобразованиям, в частности к преобразованиям для оценок числа элементов в пндиввдпой области; количественные формулы .

3. Разложение в примарные формулы для формул расширенного одноместного исчисления предикатов 4. Обобщение пеняют 1-тождественной формулм; дедуктивная замкнутость совокупности 1-тождественных формул; одноаначность равенства . 5. Добавление функциональных знаков;понятие терма; выводимые формулы 1 2.

Решение проблемы разрешимости; теоремы о полноте 1. Распознавание выводимости таких предзаренных формул исчисления предикатов, у которых все квавторы всеобщности лредшеству.ют всем квавторам существования; разрепзимость в конечном 2. Выводпмость всякой тождественной в конечном формулы одноместного исчисления преднкатов; доказательство с помощью прежней распознающей процедуры; теоретико-множественное доказательство и его финитное уточнение 3. Нормальная форлга формулы расширенного одноместного ОГЛА Н ЛЕ НИП ОГЛАВЛБННИ 261 351 Глава 4 1.

281 380 269 273 273 366 378 279 326 381 289 390 400 43 405 419 318 314 322 324 434 330 336 336 453 456 456 459 исчисления преднкатов на основе дедуктивного равенства ремы о полноте для расширенного одноместного исчисления предикатов . Глава Ч1. Неп и . Непротиворечивость существования бесконечных няднвидных областей. Начала арифметики З . реход от вопроса о вевыводимости ряда тождественных в ко- 11. Пе печном формул исчисления нредикатов к вопросу о непротиворечивости некоторой системы аксиом ари метики мена формульных переменных предикатвыми символами', одна зависимость между рассматриваемыми формулами 2. Привлечение аксиом равенства; дедекиндово определение 3.

бесконечности; введение штрих-символа . Переход к аксиомам без связанных переменных с усилением экзистенциальных аксиоы; символ О; цифры в новом 2. Об е смысле; аксиомы Пеано; получившаяся система акспо 4 . щелогическая часть доказательства непротиворечивости пом 1. В . Выбор заключительной формулы) исключение связанных 2. пе еменвых; разложение доказательства на ннтв озврз твми перенос подстаповок; исключение свободяыхпеременвых; нумерические формулы; определение истинности и лоуквости) истинность всякой формулы, выводимой без использования связанных переменных 3.

В ключение связанных переменных; мероприятия по сохранению схем при возвратном переносе подстановок; недостаточность прежних ыетодов З . Д казательство непротиворечивости с помощью процедуры з3. До редукции 1. И сключенне квавтора всеобщности; этапы редуцирования; понятие редукции формулы 2.

Вернфицируемые формулы; теорема об однозначности; леммы 3. Верифицнруемость выводимых формул, не содержащих формульных переменных; заменимость аксиом схемами аксиом а . Переход к одной (в области формул, не содержащих формульа 4. вых переменных) дедуктивно завершенной системе акс о. к м . Выводимость ряда верифицируемых формул в рассматриваемой системе аксиом; докааательство с помощью «цифр второго родаэ 2„П . Подход к пополнению этой системы аксиом; выводпмость 3. ряда эквивалентностей как достаточное условие . Дедуктивное сведение этих эквивалентностей к пяти добавляемым к атой системе аксиом формулам; система (А) 4.