Probably recursive functions

A computable function $f\colon N\to N$ is called provably recursive in a formal theory $T$ if there is an algorithm computing $f$ such that the statement "for all $x$ there is a $y$ such that $f(x)=y$" is provable in $T$. Such functions are studied in mathematical logic for two main reasons. Firstly, given a program we are often interested in proving its correctness, in particular, that its computation terminates on any input. The development of program verification methods is an important topic in Computer Science. On the other hand, we can use provably recursive functions to study and compare various formal theories. This approach leads to the study of functions of exorbitant growth rates and to the most impressive examples, as of today, of unprovable combinatorial statements.