On the interpretation of non-finitist proofs–Part II

Since the Hilbert substitution method has been applied by Ackermann to the formalism Z of number theory in 3, we shall give the no-counter-example interpretation for extensions ( c ) of Z , e.g. Z μ . The work required on top of Ackermann's investigations to check conditions ( α ) and ( β ), consists only in a suitable definition of a class of recursive functional. The verification of ( γ ) and ( δ ) is much more difficult, and requires the ideas of paras. 32 and 33 in the preceding section.