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

Секвенциальное исчисление для логики предикатов. Теорема об устранении правила сечения и ее следствия: теорема Эрбрана и интерполяционная теорема Крейга. Доказуемость трансфинитной индукции для начальных отрезков ординала $\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 сентября

Программа

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

Финансовая поддержка
Курс проводится при финансовой поддержке Минобрнауки России (грант на создание и развитие МЦМУ МИАН, соглашение №  075-15-2022-265).

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