 On the basis of your results one must now conclude, however, that that proof cannot be formalized within the system Z [of elementary number theory]; this must in fact hold true even if the system is restricted so that, of the recursive definitions, only those for addition and multiplication are retained. On the other hand, I don’t see at which place in Ackermann’s proof the formalization within Z should become impossible, …