R. L. Goodstein, “Logic-free formalisations of recursive arithmetic”, Math. Scand., vol. 2, pp. 246–260, Dec. 1954.