R. L. Goodstein, “Logic-free formalisations of recursive arithmetic”, Math. Scand., vol. 2, pp. 246–260, Dec. 1954, doi: 10.7146/math.scand.a-10412.