Справочная книга по математической логике, часть 4, Теория доказательств и конструктивная математика, Барвайс Д., 1983

Справочная книга по математической логике, Часть 4, Теория доказательств и конструктивная математика, Барвайс Дж., 1983.

Последний том «Справочной книги по математической логике» содержит обзоры по наиболее современным направлениям теории доказательств и конструктивной математики. Эти обзоры не претендуют на полное описание новейших достижений теории доказательств. Это было бы очень трудно сделать в рамках одной книги. Составители ограничились обзорами небольшого числа тех областей теории доказательств, которые в последнее время активно развивались и которые тесно переплетаются с другими областями математической логики, алгебры и топологии. В худшем положении оказалась конструктивная математика. В посвященной ей главе 5, написанной А. С. Трулстрой, термин «конструктивная математика» трактуется очень широко: по А. С. Трулстре конструктивная математика включает в себя интуиционизм. Поэтому в главе 5 уделяется много внимания различным современным вариантам интуиционизма, а некоторые важные специфические понятия и результаты собственно конструктивной математики не затронуты.

Справочная книга по математической логике, Часть 4, Теория доказательств и конструктивная математика, Барвайс Дж., 1983

Программа Гильберта.
На рубеже столетия математику преследовали различные трудности, начиная с антиномий и парадоксов и кончая противоречиями как формальными, так и личными. Трудности встречались в математике и раньше, но их удавалось устранить или обойти. Древние греки в конце концов пожали плечами и приняли иррациональные числа; специалисты в области математического анализа избежали парадоксов, связанных с бесконечно малыми величинами, когда сумели, наконец, выделить и строго ввести понятия предела и непрерывности. Даже в теории множеств Цермело предложил решение проблемы парадоксов еще в 1908 г. Прежде чем аксиоматизировать некоторую область математики, мы должны знать, о чем говорим. Поэтому вместо того, чтобы взять в качестве аксиом теории множеств некоторые интуитивно очевидные свойства конечных множеств, некоторые очевидные свойства множества всех подмножеств данного множества и еще несколько очевидных свойств какой-нибудь третьей сущности — процесс, который почти гарантирует противоречие, — Цермело сначала описал кумулятивную иерархию, а затем перечислил аксиомы для этой единственной сущности. До последних работ по большим кардиналам все аксиомы, добавленные позднее, были просто очередными свойствами, очевидным образом истинными для этой иерархии, но формально невыводимыми.

Ситуацию, которая возникла затем, социологи описали бы в терминах «культурной отсталости». Несмотря на наличие непротиворечивой теории множеств, математики продолжали беспокоиться о непротиворечивости. Некоторые сомневались даже в непротиворечивости самой арифметики! Ситуацию еще более ухудшали гротескные попытки Л.Э.Я. Брауэра превратить математику в религию.

СОДЕРЖАНИЕ
§ 1. Программа Гильберта.
§ 2. Теоремы Гёделя.
2.1. Предварительные сведения.
2.2. Доказательство теоремы о неполноте.
2.3. Что будет.
§ 3. Кодирование.
3.1. Примитивно рекурсивное кодирование конечных последовательностей.
3.2. Примитивно рекурсивное кодирование синтаксиса.
3.3. Теорема Россера.
3.4. Теория рекурсии .
3.5. Иерархия формул.
§ 4. Метаматематические свойства, отличные от непротиворечивости..
4.1. Принципы рефлексии.
4.1а. Соображения иерархии.
4.2. w-непротиворечивость.
4.3. Свойства полноты.
4.3а. Теорема Кента.
§ 5. Два приложения.
5.1. Теорема о неподвижной точке.
5.2. Результаты о консервативности.
§ 6. Формализованная теорема о полноте.
6.1. Теорема Гильберта — Бернайса о полноте.
6.2. Теоремы о неполноте.
6.3. Комментарии.
Литература.