In various places I have read that the normally considered non-primitive recursive Ackermann function is primitive recursive in higher-order logic. It's claimed to be due to "Reynolds, 1985", as far as I can tell this refers to "THREE APPROACHES TO TYPE STRUCTURE". But quoting from this paper: "However, our ability to define numerical functions is not limited to the scheme of primitive recursion." before defining Ackermann function using a scheme from this paper. I assume that when people say Ackermann function is definable via primitive recursion they mean this scheme.

I have tracked down this claim to HOL documentation footnote (p. 40, 50 in the pdf)

It's kind of hard to track down the meaning of this, but maybe someone knows. Are there definitions of primitive recursion (sic!) relative to the underlying logical system we operate in or is this treating whatever Foetus can prove terminating as primitive recursive?

  • 5
    $\begingroup$ I think that "higher-order primitive recursion" is a suggestive way of calling the recursion scheme of Gödel's system T (which is indeed enough to define the Ackermann function), because it looks exactly like we would expect a higher-order version of usual, first-order primitive recursion to look like. I don't think that there's a general underlying definition of "primitive recursion relative to a theory". But maybe I'm wrong. $\endgroup$ Oct 6, 2023 at 10:43


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.