Теоремы Гёделя о неполноте

Лев Дмитриевич Беклемишев

Программа курса

1. Аксиоматический метод, формальные аксиоматические теории, программа Гильберта (теория и метатеория, установление консервативности versus установление непротиворечивости, финитизм).
2. Язык и аксиомы арифметики Пеано PA. Арифметика Робинсона. Выразимость предикатов и функций в стандартной модели арифметики. Арифметическая иерархия.
3. Кодирование двоичных слов числами. Выразимость конкатенации слов и экспоненты в языке арифметики.
4. Машины Тьюринга, их конфигурации и протоколы вычислений.
5. Вычислимость (частичных) функций по Тьюрингу, тезис Чёрча-Тьюринга. Разрешимые и перечислимые множества и предикаты. Вычислимая универсальная функция для множества всех одноместных вычислимых функций. Пример вычислимой функции, не имеющей всюду определённого вычислимого продолжения. Пример перечислимого неразрешимого множества.
6. Эквивалентность перечислимости предиката и его и Σ₁-определимости в стандартной модели арифметики. Кодирование машин Тьюринга, их конфигураций и вычислений.
7. Первая теорема Геделя о неполноте.
8. Представимость предикатов и функций в арифметике. Доказуемая Σ₁-полнота арифметики Робинсона. Теорема о представимости вычислимых функций в арифметике Робинсона.
9. Рекурсивно неотделимые пары множеств, теорема Гёделя-Россера.
10. Формула доказуемости, лемма о неподвижной точке. Условия Бернайса-Лёба. Вторая теорема Геделя о неполноте (недоказуемость непротиворечивости), теорема Лёба, теорема Тарского о невозможности определения истинности. Теорема Чёрча об алгоритмической неразрешимости арифметики и чистой логики предикатов.
11. Схемы рефлексии. Локальная и равномерная рефлексия. Определение истинности для Σ_n-формул. Теоремы о неограниченности для схем рефлексии.
12. Модальная логика доказуемости GL. Её арифметическая корректность. Семантика Крипке для логики доказуемости. Теорема о полноте по Крипке. Теоремы Булоса-Артемова и Горячева для локальных схем рефлексии.