Ackermann's Function Is Not Primitive Recursive

Lawrence C. Paulson 🌐

March 23, 2022

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

Abstract

Ackermann's function is defined in the usual way and a number of its elementary properties are proved. Then, the primitive recursive functions are defined inductively: as a predicate on the functions that map lists of numbers to numbers. It is shown that every primitive recursive function is strictly dominated by Ackermann's function. The formalisation follows an earlier one by Nora Szasz.
BSD License

Topics

Theories of Ackermanns_not_PR