Goodstein RL. Logic-free formalisations of recursive arithmetic. Math. Scand. 1954;2:246-260. doi:10.7146/math.scand.a-10412