Goodstein, R. L. “Logic-Free Formalisations of Recursive Arithmetic”. Mathematica Scandinavica, vol. 2, Dec. 1954, pp. 246-60, https://doi.org/10.7146/math.scand.a-10412.