Goodstein, R. L. (1954) “Logic-free formalisations of recursive arithmetic”, MATHEMATICA SCANDINAVICA, 2, pp. 246–260. doi: 10.7146/math.scand.a-10412.