Курс посвящён введению в одну из наиболее важных формальных систем – арифметику Пеано – и доказательству некоторых относящихся к ней классических результатов, лежащих в основе структурной теории доказательств. Будут рассмотрены следующие темы:

Секвенциальное исчисление для логики предикатов. Теорема об устранении правила сечения и ее следствия: теорема Эрбрана и интерполяционная теорема Крейга. Доказуемость трансфинитной индукции для начальных отрезков ординала $\varepsilon_0$. Недоказуемость трансфинитной индукции до ординала $\varepsilon_0$ в арифметике Пеано (теорема Генцена). Доказуемо рекурсивные функции. Иерархия функций Харди и порожденные ей классы. Недоказуемые комбинаторные утверждения.

Курс рассчитан на студентов, прослушавших вводный курс математической логики.

Тема 1. Исчисление секвенций для логики предикатов в форме Тейта.

1.1. Секвенциальное исчисление для логики предикатов в форме Тейта.
1.2. Теорема об устранении правила сечения.
1.3. Следствия теоремы об устранении правила сечения: свойство подформульности, теорема Эрбрана (для экзистенциальных формул), интерполяционная теорема Крейга.
1.4. Формализация арифметики Пеано в секвенциальном исчислении. Система $\mathrm{РА(Х)}$ арифметики со свободными предикатными переменными.

Тема 2. Арифметика ординалов.

2.1. Вполне упорядоченные множества, операции сложения, умножения, возведения в степень.
2.2. Канторовская нормальная форма.

Тема 3. Омега-логика.

3.1. Омега-правило и омега-логика. Система арифметики с омега-правилом $\mathrm{РА}_\omega$.
3.2. Доказуемость истинных $\Pi_1^1$-утверждений в $\mathrm{РА}_\omega$.
3.3. Погружение выводов в арифметики $\mathrm{РА(Х)}$ в $\mathrm{РА}_\omega$.

Тема 4. Устранение сечения в арифметике с омега-правилом.

4.1. Высота и ранг омега-вывода. Устранение правила сечения в арифметике с омега-правилом с оценками ранга и высоты.
4.2. Принцип трансфинитной индукции. Арифметическая схема трансфинитной индукции для арифметически определимой системы ординальных обозначений.
4.3. Лемма о нижней оценке высоты вывода без сечений формулы трансфинитной индукции в системе $\mathrm{РА}_\omega$. Недоказуемость трансфинитной индукции до ординала $\varepsilon_0$ в арифметике Пеано (теорема Генцена).

Тема 5. Система обозначеній для ординала ординала $\varepsilon_0$.

5.1. Примитивно рекурсивные функции, кодирование конечных последовательностей, возвратная рекурсия.
5.2. Преобразование данного вполне упорядоченного множества типа а в множество типа $\omega^\alpha$. Примитивно рекурсивная последовательность систем обозначений для ординалов $\omega_0=1,\omega_{n+1}= \omega^{\omega_n}$.
5.3. Доказуемость трансфинитной индукции для начальных отрезков ординала $\varepsilon_0$ в арифметике Пеано (теорема Генцена).
5.4. Канторовская система обозначений для ординала $\varepsilon_0$; её примитивная рекурсивность.

Тема 6. Теоретико-доказательственные ординалы.

6.1. Система арифметики второго порядка $\mathrm{АСА}_0$. Ординал теории как супремум всех порядковых типов доказуемо фундированных в $\mathrm Т$ вполне упорядочений.
6.2. Теорема: для любого $\Pi_1^1$ -предложения $\pi$ найдется примитивно рекурсивное дерево $\mathrm Т$ такое, что $\pi$ эквивалентно утверждению о фундированности $\mathrm Т$.
6.3. Порядок Клини-Брауэра на омега-дереве. Эквивалентность его фундированности и фудированности дерева. Формализуемость в $\mathrm{АСА}_0$.
6.4. Построение разрешимого вполне упорядочения универсального для множества всех доказуемо фундированных в теории $\mathrm{Т}$ примитивно рекурсивных вполне упорядочений. Совпадение его порядкового типа и ординала теории.
6.5. Следствие: ординал $\Pi_1^1$ -корректной теории меньше супремума ординалов всех рекурсивных вполне упорядочений (ординала Чёрча-Клини).
6.6. Неизменность ординала $\Pi_1^1$ -корректной теории при ее расширении множеством истинных $\Sigma_1^1$-предложений.
6.7. Всякий рекурсивно перечислимый ординал примитивно рекурсивен.

Список литературы
[1] W. Pohlers, Proof theory: First steps into impredicativity. Springer-Verlag Berlin Heidelberg, 2009 (темы 1-5).
[2] M. Rathjen, The realm of ordinal analysis. Cambridge University Press, 1999 (тема 6).
[3] Х. Швихтенберг, Некоторые приложения устранения сечения. В кн.: Справочная книга по математической логике (под ред. Дж. Барвайса), Часть IV (гл. 2). М., Наука, 1983. (темы 1-4).

Расписание на осенний семестр 2023/2024 учебного года:

Время занятий: вторник 16:45 – 18:15

Первое занятие: 12 сентября

Лекторы
Беклемишев Лев Дмитриевич
Яворская Татьяна Леонидовна

Организации
Математический институт им. В.А. Стеклова Российской академии наук, г. Москва
Математический центр мирового уровня «Математический институт им. В.А. Стеклова Российской академии наук» (МЦМУ МИАН)