RUS  ENG
Полная версия
ВИДЕОТЕКА

Летняя школа «Современная математика» имени Виталия Арнольда, 2018
21 июля 2018 г. 17:15, г. Дубна, Московская область, г. Дубна, дом отдыха «Ратмино»


Доказуемо рекурсивные функции, занятие 1

Л. Д. Беклемишев



Аннотация: Вычислимая функция $f: \mathbb{N}\rightarrow \mathbb{N}$ называется доказуемо рекурсивной в данной формальной теории $T$, если существует алгоритм её вычисления такой, что в $T$ можно доказать утверждение «для любого $x$ существует $y$ такой, что $f(x)=y$». В математической логике такие функции изучаются по двум причинам. Во-первых, для данной программы нас часто интересует доказательство её корректности, в частности вопрос о том, завершает ли она работу при любых исходных данных. С другой стороны, варьируя функцию $f$ мы можем ставить для теории $T$ сколь угодно сложные (вплоть до невыполнимости) задачи на доказательство. Тем самым, доказуемо рекурсивные функции могут быть использованы для изучения и сравнения между собой различных формальных теорий. Такой подход приводит к построению функций, имеющих катастрофически большой рост, и к наиболее впечатляющим на сегодняшний день примерам недоказуемых комбинаторных утверждений. Мы начнем с понятия машины Тьюринга и вычислимой функции. Затем мы разберемся в том, как формальная арифметика может говорить о вычислениях, и убедимся, что она фактически имеет свой «внутренний» язык программирования. Затем мы поймем, что для любых разумных систем аксиом $T$ их запас доказуемо рекурсивных функций никак не может исчерпывать все вычислимые всюду определенные функции. Отсюда мы выведем первую теорему Гёделя о неполноте. Дальнейший рассказ пойдет о том, что можно сказать о классах доказуемо рекурсивных функций для конкретных теорий и о связанных с этим открытых проблемах в математической логике. На этом пути мы встретим различные фрагменты арифметики Пеано, иерархию Гжегорчика быстрорастущих функций, а также теоремы Париха и Парсонса–Минца, описывающие классы доказуемо рекурсивных функций для теорий, получающихся ограничением аксиомы индукции в арифметике.

Website: https://www.mccme.ru/dubna/2018/courses/beklemishev.html
Цикл лекций


© МИАН, 2024