C 23.03 в связи с эпидемической обстановкой курс переходит в удаленный режим. Лекции будут продолжать записываться без слушателей и выкладываться на этом сайте и в youtube в еженедельном режиме. Лекторы постараются подготовить записки по материалам лекций и/или снабдить видеозаписи подробными ссылками на литературу. Следите за объявлениями здесь.

Курс планируется как годовой. В первой части (осенний семестр) планируется изложить основы лямбда-исчисления и его связь с системой естественного вывода для интуиционистской логики (соответствие Карри‒Говарда).
Примерный список тем первого семестра:

1. Бета-редукции. Свойство Чёрча‒Россера. Стратегии редукций. Слабая и сильная нормализуемость для типизованного лямбда-исчисления.
2. Теорема о неподвижной точке для бестипового лямбда-исчисления. Кодирование рекурсивных функций.
3. Алгоритм выведения типов для простого типового лямбда-исчисления.
4. Эта-редукция. Теоретико-множественная интерпретация лямбдаисчисления, теорема о полноте.
5. Интуиционистская логика высказываний. Семантика Крипке, теорема о полноте. Соответствие Карри‒Говарда.
6. Исчисление гильбертовского типа и комбинаторная логика.
7. Интерпретация типизованного лямбда-исчисления на декартово замкнутых категориях.

Во второй части курса планируется рассказать о семантике Скотта для бестипового лямбда-исчисления, гёделевской системе T и и её связи с классами доказуемо тотальных вычислимых функций в арифметике 1-го порядка. Примерный список тем второго семестра:

1. Семантика бестипового лямбда-исчисления, модели Скотта и Плоткина, полные частично упорядоченные множества.
2. Интуиционистская и классическая арифметика. Негативный перевод. Перевод Фридмана‒Драгалина. Доказуемо тотальные вычислимые функции.
3. Функционалы конечных типов. Гёделевская система T. Функциональная интерпретация. Характеризация доказуемо тотальных вычислимых функций в арифметике PA как функций, представимых в системе T.

Регистрационная форма участников

Объявления

21.03. В следующей части курса будет рассказано об интуиционистской арифметике, функционалах конечных типов и гёделевской системе T. Очередная лекция будет записана 23.03 и должна появиться в сети на следующий день. Тема лекции: интуиционистская логика предикатов и интуиционистская арифметика. Лектор: Л.Д. Беклемишев.

Прошедшие лекции

26.03. Лекция 16: Негативный перевод (Гёделя--Генцена) классической логики в интуиционистскую.

04.04 Лекция 17: Примитивно рекурсивная арифметика.

11.04. Лекция 18: Интуиционистская арифметика.

Аннотация: теория НА, принцип наименьшего числа влечет закон исключенного третьего, негативная интерпретация PA в HA, перевод Фридмана-Драгалина, замкнутость HA относительно рекурсивного правила Маркова и правила независимости посылок, консервативность PA над HA для $\forall\exists$-формул, штрих Акцеля, дизъюнктивное и экзистенциальное свойства НА.

21.04 Лекция 19: Гёделевская система Т. Функциональная интерпретация интуиционистской арифметики в Т, часть 1.

Аннотация: Функционалы конечных типов. Язык системы Т. Рекурсор. Аксиоматика системы Т. D-перевод формул арифметики Гейтинга HA в T. Формулировка теоремы Гёделя о функциональной интерпретации. Начало её доказательства: эквивалентная аксиоматизация исчисления высказываний, интерпретация правил modus ponens и силлогизма, аксиома $\phi\to\phi\land\phi$.

28.04 Лекция 20: Функциональная интерпретация интуиционистской арифметики в Т, часть 2.

Аннотация: Завершение доаказательства теоремы Гёделя об интерпретации арифметики HA в системе T. Правило индукции. Следствия об относительной непротиворечивости, консервативности и представимости доказуемо рекурсивных функций PA в системе T.

12.05 Лекция 21. Применения функциональной интерпретации. Интерпретация отсутствием контрпримера. Модели системы Т.

Программа осеннего семестра

Программа весеннего семестра

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

Лекторы
Беклемишев Лев Дмитриевич
Кузнецов Степан Львович

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