Теория доказательств и формальная арифметика

д.ф.-м.н. Лев Дмитриевич Беклемишев

Математический институт им. В.А. Стеклова
Научно-Образовательный Центр

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

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