R. L. Goodstein, “On non-constructive theorems of analysis and the decision problem”, Math. Scand., vol. 3, pp. 261–263, Dec. 1955, doi: 10.7146/math.scand.a-10444.