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

Вычислимая функция $f\colon N\to N$ называется доказуемо рекурсивной в данной формальной теории $T$, если существует алгоритм её вычисления такой, что в $T$ можно доказать утверждение «для любого $x$ существует $y$ такой, что $f(x)=y$». В математической логике такие функции изучаются по двум причинам. Во-первых, для данной программы нас часто интересует доказательство её корректности, в частности вопрос о том, завершает ли она работу при любых исходных данных. Разработка методов верификации программ — важный раздел Computer Science. С другой стороны, мы можем использовать доказуемо рекурсивные функции для изучения и сравнения между собой различных формальных теорий. Такой подход приводит к изучению функций, имеющих катастрофически большой рост и наиболее впечатляющим на сегодняшний день примерам недоказуемых комбинаторных утверждений.