Лев Дмитриевич Беклемишев
Доказуемо рекурсивные функции
Л. Д. Беклемишев планирует провести 4 занятия.
Доступны 4 видеозаписи курса.
Вычислимая функция f = N --> N называется доказуемо рекурсивной в данной формальной теории T, если существует алгоритм её вычисления такой, что в T можно доказать утверждение "для любого x существует y такой, что f(x)=y". В математической логике такие функции изучаются по двум причинам. Во-первых, для данной программы нас часто интересует доказательство её корректности, в частности вопрос о том, завершает ли она работу при любых исходных данных. С другой стороны, варьируя функцию f мы можем ставить для теории T сколь угодно сложные (вплоть до невыполнимости) задачи на доказательство. Тем самым, доказуемо рекурсивные функции могут быть использованы для изучения и сравнения между собой различных формальных теорий. Такой подход приводит к построению функций, имеющих катастрофически большой рост, и к наиболее впечатляющим на сегодняшний день примерам недоказуемых комбинаторных утверждений.
Мы начнем с понятия машины Тьюринга и вычислимой функции. Затем мы разберемся в том, как формальная арифметика может говорить о вычислениях, и убедимся, что она фактически имеет свой "внутренний" язык программирования. Затем мы поймем, что для любых разумных систем аксиом T их запас доказуемо рекурсивных функций никак не может исчерпывать все вычислимые всюду определенные функции. Отсюда мы выведем первую теорему Гёделя о неполноте.
Дальнейший рассказ пойдет о том, что можно сказать о классах доказуемо рекурсивных функций для конкретных теорий и о связанных с этим открытых проблемах в математической логике. На этом пути мы встретим различные фрагменты арифметики Пеано, иерархию Гжегорчика быстрорастущих функций, а также теоремы Париха и Парсонса-Минца, описывающие классы доказуемо рекурсивных функций для теорий, получающихся ограничением аксиомы индукции в арифметике.
Материалы
E-mail оргкомитета:
dubna@mccme.ru