М., Наука, 1979 г. – 558 с.Предисловие редактора русского перевода
Предисловие ко второму изданию
Предисловие Гильберта к первому изданию
Предисловие к первому изданиюПроблема непротиворечивости в аксиоматических исcледованиях как логическая проблема разрешимости
Формальная аксиоматика
Отношение формальной аксиоматики к содержательной; вопрос о непротиворечивости; арифметизация
Пример: аксиомы геометрии
Чисто логический подход к аксиоматике
Проблема разрешимости
Общезначимость и выполнимость
Распознавание в случае конечных индивидных областей
Метод построения модели
Вопрос о непротиворечивости в случае бесконечной индивидной области
Формулы, невыполнимые в конечном; натуральный ряд как модель
Проблематика бесконечного
Установление непротиворечивости как доказательство невозможности; метод арифметизации
Элементарная арифметика. Финитный способ рассуждений и его границы
Рассуждения на интуитивном уровне и их применение в элементарной арифметике
Понятие цифры; отношение порядка; сложение
Законы арифметических действий; полная индукция; умножение; делимость; простые числа
Рекурсивные определения
Одно доказательство невозможности
Дальнейшие применения интуитивных рассуждений
Отношение арифметики к учению о количестве
Формальная точка зрения в алгебре
Финитная точка зрения; выход за ее пределы в области арифметики
Логическая характеризация финитной точки зрения
«Tertium nоn datur» для целых чисел; принцип наименьшего числа
Нефинитные методы в анализе
Различные определения действительного числа
Верхняя грань числовой последовательности; верхняя грань множества чисел
Принцип выбора
Исследования, направленные на непосредственное финитное построение анализа; возврат к прежней постановке проблемы; теория доказательств
Формализация процесса логического вывода I: Исчисление высказываний
Теория истинностных функций
Истинностные функции и их таблицы
Заменимость; правила замены
Примеры заменимости
Двойственность; конъюнктивная и дизъюнктивная нормальные формы; тождественно истинные выражения; распознающая процедура
Совершенная нормальная форма; распознавание заменимости; примеры
Применение теории истинностных функций к логическому выводу; формализация умозаключений в логике высказываний с помощью тождественно истинных выражений, правила подстановки и схемы заключения
Дедуктивная логика высказываний
Постановка задачи
Одна система исходных формул для дедуктивной логики высказываний; полнота этой системы
Позитивная логика; регулярные импликативные формулы; позитивно тождественные импликативные формулы; возможные упрощения
Доказательства независимости, проводимые методом оценок
Логическая интерпретация как оценка; общий метод
Доказательство независимости рассматриваемой системы исходных формул; еще одно доказательство независимости
Применение метода оценок к вопросу о замене формул схемами
Возврат к рассмотренному в § 2 способу формализации вывода; сокращенные правила; замечание, касающееся противоречивости системы
Формализация процесса вывода II: Исчисление предикатов
Введение индивидных переменных; понятие формулы; правило подстановки; пример; параллель с содержательными рассуждениями
Связанные переменные и правила для кванторов всеобщности и существования
Недостаточность свободных переменных
Введение связанных переменных; кванторы всеобщности и существования; правило переименования переменных; предотвращение неоднозначностей; обобщение понятия формулы и правила подстановки
Эвристическое введение правил для квантоуов всеобщности и существования; содержательный смысл формул и схем
Окончательная формулировка правил исчисления предикатов; изображение форм категорических суждений; случай пустой индивидной области
Выводимость
Некоторые производные правила
Вывод некоторых формул
Вопросы систематики
Понятия t-тождественной формулы и формулы, тождественной в конечном; дедуктивная замкнутость совокупности t-тождественных формул; непротиворечивость исчисления предикатов; вопросы полноты
Экскурс в теоретико-множественную логику предикатов; предварительные замечания к вопросу о полноте; проблема разрешимости и ее уточнение с дедуктивной точки зрения
Изучение формализма исчисления предикатов
Понятие переводимости; производные правила
Приведение формул к предваренному виду; примеры; описание разрешимых случаев проблемы разрешимости с помощью предваренной нормальной формы
Разложение формул одноместного исчисления предикатов в примарные формулы; пример
Дедуктивное равенство и дедукционная теорема
Понятие дедуктивного равенства; два существенных случая дедуктивного равенства; переводимость и дедуктивное равенство
Дедукционная теорема
Применения дедукционной теоремы: сведение вопросов, связанных с аксиоматикой к вопросам выводимости формул в исчислении предикатов; рассмотрение одного распространенного способа умозаключения
Дедуктивное равенство произвольной формулы подходящей сколемовской нормальной форме, а также нормальной дизъюнкции; упрощение этого перехода
Исчисление предикатов с равенством. Полнота одноместнoгo исчиcления предикатов
Расширенный формализм
Знак равенства; изображение высказываний о количестве; аксиомы равенства и формальные свойства равенства
Применение аксиом равенства к различным преобразованиям, в частности к преобразованиям для оценок числа элементов в индивидной области; количественные формулы
Разложение в примарные формулы для формул расширенного одноместного исчисления предикатов
Обобщение понятия t-тождественной формулы; дедуктивная замкнутость совокупности t -тождественных формул; однозначность равенства
Добавление функциональных знаков; понятие терма; выводимые формулы
Решение проблемы разрешимости; теоремы о полноте
Распознавание выводимости таких предваренных формул исчисления предикатов, у которых все кванторы всеобщности предшествуют всем кванторам существования; разрешимость в конечном
Выводимость всякой тождественной в конечном формулы одноместного исчисления предикатов; доказательство с помощью прежней распознающей процедуры; теоретико-множественное доказательство и его финитное уточнение
Нормальная форма формулы расщиренного одноместного исчисления предикатов на основе дедуктивного равенства
Теоремы о полноте для расширенного одноместного исчисления предикатов
Непротиворечивость существования бесконечных индивидных областей. Начала арифметики
Переход от вопроса о невыводимости ряда тождественных в конечном формул исчисления предикатов к вопросу о непротиворечивости некоторой системы аксиом арифметики
Замена формульных переменных предикатными символами; одна зависимость между рассматриваемыми формулами
Привлечение аксиом равенства; дедекиндово определение бесконечности; введение штрих-символа
Переход к аксиомам без связанных переменных с усилением экзистенциальных аксиом; символ 0; цифры в новом смысле; аксиомы Пеано; получившаяся система аксиом
Общелогическая часть доказательства непротиворечивости
Выбор заключительной формулы; исключение связанных переменных; разложение доказательства на нити
Возвратный перенос подстановок; исключение свободных переменных; нумерические формулы; пределение истинности и ложности; истинность всякой формулы, выводимой без использования связанных переменных
Включение связанных переменных; мероприятия по сохранению схем при возвратном переносе подстановок; недостаточность прежних методов
Доказательство непротиворечивости с помощью процедуры редукции
Исключение квантора всеобщности; этапы редуцирования; понятие редукции формулы
Верифицируемые формулы; теорема об однозначности; леммы
Верифицируемость выводимых формул, не содержащих формульных переменных; заменимость аксиом схемами аксиом
Переход к одной (в области формул, не содержащих формульных переменных) дедуктивно завершенной системе аксиом
Выводимость ряда верифицируемых формул в рассматриваемой системе аксиом; доказательство с помощью «цифр второго рода»
Подход к пополнению этой системы аксиом; выводимостъ ряда эквивалентностей как достаточное условие
Дедуктивное сведение этих эквивалентностей к пяти добавляемым к этой системе аксиом формулам; система (А)
Полнота системы (А)
Включение полной индукции
Формализация принципа полной индукции с помощью формулы и с помощью схемы; равносильность обеих формализаций; инвариантность запаса выводимых формул без формульных переменных относительно добавления к системе схемы индукции
Упрощение рассматриваемой системы aкcиoм в результате добавления аксиомы индукции; система (В)
Доказательства независимости
Невыводимость аксиомы индукции из формул системы (А)
Доказательства независимости с помощью метода подстановок
Установление ряда других независимостей с помощью модификации процедуры редукции
Изображение принципа наименьшего числа при помощи выражающей его формулы; равносильность этой формулы аксиоме индукции на основе прочих аксиом системы (В)
Рекурсивные определения
Некоторые пояснения принципиального характера
Простейшая схема рекурсии; формализация интуитивной процедуры вычисления; сопоставление явных определений с рекурсивными
Доказательство непротиворечивости добавления рекурсивных определений в рамках элементарного исчисления со свободными переменными; привлечение схемы индукции
Невозможность вывода непротиворечивости рекурсивных определений в качестве следствия непротиворечивости систем предыдущих аксиом; заменимость арифметических аксиом явными определениями; явное определение символа < при помощи соответствующей рекурсивной функции; вывод
основных свойств символа <
Рекурсивная арифметика
Вывод законов для сложения, вычитания, умножения и для символа <
Изображение высказываний равенствами вида t = 0; суммы и произведения с переменным числом членов; изображение высказываний с ограниченными кванторами; изображение максимума и минимума
Делимость; деление с остатком; наименьший отличный от 1 делитель; последовательность простых чисел; разложение числа на простые множители; нумерация конечных последовательностей чисел; нумерация числовых пар; наибольший общий делитель; наименьшее общее кратное
Некоторые обобщения схем рекурсии и индукции
Рекурсии, допускающие сведение к простейшей схеме рекурсии (примитивная рекурсия); рекурсии пробега, одновременные рекурсии
Перекрестные рекурсии; несводимость перекрестных рекурсий определенного типа к примитивным рекурсиям
Обобщенная схема индукции; устранимость этой схемы
Представимость рекурсивных функций; переход к удовлетворительной системе аксиом для арифметики
Возврат к полному формализму; система (С); понятие сущеcтвeннoгo расширения формализма; примеры несущественных расширений; представимость функции
Доказательство того, что сумма и разность не представимы в формализме системы (В); рекурсивные равенства для сложения как аксиомы; система (D)
Доказательство непротиворечивости и полноты системы (D) с помощью метода редукции; непредставимость умножения в формализме системы (D)
Изменение ситуации в случае добавления рекурентных равенств для умножения; система (Z)
Дополнительное рассмотрение аксиом равенства
Замена второй аксиомы равенства аксиомами более специального характера
Применение к системам (А), (В) и (Z)
Применение к проблеме разрешимости; устранимость аксиом равенства из выводов формул исчисления предикатов
Понятие «тот, который» и его устранимость
ί-правило и оперирование с ним
Разъяснения неформального характера; введение ί -правила; предотвращение коллизий; изображение функций посредством ί –термов
Вложение и подчинение; символы для сокращений
Функция
