On an extension of finitary mathematics which has not yet been used (1972)
Kurt Gudel, Solomon Feferman, John W Dawson, Stephen Cole Kleene, Gregory Martin Moore, Robert M Solovay, Jean van HEIJENOORT · 2001
Abstract P. Bernays has pointed out that, even in order to prove only the consistency of classical number theory, it is necessary to extend Hilbert’s finitary standpoint. He suggested admitting certain abstract concepts in addition to the combinatorial concepts referring to symbols. The abstract concepts that so far have been used for this purpose are those of the constructive theory of ordinals and those of intuitionistic logic. It is shown that a certain concept of computable function of finite simple type over the natural numbers can be used instead, where no other procedures of constructing such functions are necessary except primitive recursion by a number variable and definition of a function by an equality with a term containing only variables and/or previously introduced functions beginning with the function +.