Читать онлайн «Основания математики»

Оглавление МАТЕМАТИЧЕСКАЯ ЛОГИКА И ОСНОВАНИЯ МАТЕМАТИКИ МОСКВА «НАУКА» ГЛАВНАЯ РЕДАКЦИЯ ФИЗИКО-МАТЕМАТИЧЕСКОЙ ЛИТЕРАТУРЫ 1982 ОСНОВАНИЯ МАТЕМАТИКИ ТЕОРИЯ ДОКАЗАТЕЛЬСТВ Д. ГИЛЬБЕРТ П. БЕРНАЙС Перевод с немецкого Н. М НАГОРНОГО Под редакцией С. И. АДЯНА МОСКВА «НАУКА» ГЛАВНАЯ РЕДАКЦИЯ ФИЗИКО-МАТЕМАТИЧЕСКОЙ ЛИТЕРАТУРЫ 1982 32. 12 Г 47 УДК 517. 11 D. Hilbert und P. Bernays GRUNDLAGEN DER MATHEMATIK. Метод исключения связанных переменных при помощи гильбертова е-символа 17 § 1. Процедура символьного решения экзистенциальных формул 17 § 2. Гильбертов 8-символ и s-формула 27 § 3, Доказательство первой s-теоремы 37 а) Подготовка 37 б) Гильберювский подход 40 в) Типы комбинирования е-символов; степень и ранг е-терма 43 г) Устранение критических формул в общем случае 47 д) Обобщение результата 51 § 4 Доказательства непротиворечивости 55 а) Одна общая теорема о непротиворечивости 55 б) Приложение к геометрии 61 Глава П. Исследование арифметики при помощи связанных с е-символом методов теории доказательств 74 § 1 Применение нп-теоремы к арифметике 74 § 2. Распространение первой е-теоремы на общую аксиому равенства 82 а) Подготовительные соображения; основной тип; формулы е-равенства 82 б) Совместное устранение критических формул и формул е-ра- е-равенства 93 в) Усиленный вариант первой е-теоремы и нп-теоремы 109 § 3. Причины, препятствующие распространению процедуры устра- устранения е-символов на неограниченную схему индукции. Форма- Формализация принципа индукции с помощью второй формулы для е-символа. Переход к первоначальному гильбертовскому подходу ИЗ § 4. Первоначальный гильбертовский подход к проблеме исключения е-символов и его дальнейшее развитие 124 g ОГЛАВЛЕНИЕ а) Простейшие частные случаи 124 б) Подготовка к рассмотрению общего случая 129 в) Реализации гильбертовского подхода в случае е-термов ранга 1 140 г) Построение последовательности общих замен в общем случае 146 д) Построение резольвенты в случае, когда все критические формулы являются формулами первого рода . . . . 150 е) Несостоятельность рассмотренного метода в случае критиче- критических формул второго рода с произвольным рангом. Дополнение к предыдущему результату 156 ж) Использование полученного результата в нп-теореме ... . 161 Глава III. Использование е-символа в изучении логического формализма 167 § 1. Вторая е-теорема 167 § 2. Распространение второй е-теоремы на общую аксиому равен- равенства Смежные проблемы 176 § 3. Теорема Эрбрана 189 § 4. Критерии опровержимости в чистом исчислении предикатов 212 § 5. Применение полученных критериев к проблеме разрешимости 230 а) Общие сведения о выполнимости.