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