Abstract
P. Bernays has pointed out that, in order to prove the consistency of classical number theory, it is necessary to extend Hilbert's finitary standpoint by 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 the concept of a computable function of finite simple type over the integers can be used instead, where no other procedures of constructing such functions are necessary except simple recursion by an integral variable and substitution of functions in each other (starting with trivial functions).
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
A bibliography of work resulting from Gödel's paper
Michael Beeson [1978], ‘A type-free Gödel interpretation’, J. Symbolic Logic 43, 213–227.
Justus Diller [1968], ‘Zur Berechenbarkeit primitiv-rekursiver Funktionale endlicher Typen’, in: Contributions to Mathematical Logic, H. A. Schmidt and K. Schütte (eds.), North-Holland, Amsterdam, pp. 109–120.
Justus Diller [1978], ‘Functional interpretations of Heyting's arithmetic in all finite types’.
Justus Diller and W. Nahm [1974], ‘Eine Variante zur Dialectica-Interpretation der Heyting-Arithmetik endlicher Typen’, Arch. Math. Logik Grundlagenforsch. 16, 49–66.
Justus Diller and Kurt Schütte [1971], ‘Simultane Rekursionen in der Theorie der Funktionale endlicher Typen’, Arch. Math. Logik Grundlagenforsch. 14, 69–74.
Justus Diller and H. Vogel [1975], ‘Intensionale Funktionalinterpretation der Analysis’, in: Proof Theory Symposion Kiel 1974. J. Diller and G. H. Müller (eds.), Lecture Notes in Mathematics 500, Springer-Verlag, Berlin, pp. 56–72.
A. G. Dragalin [1968], ‘The computation of primitive recursive terms of finite type, and primitive recursive realization,’ Zap. Naučn. Sem. Leningrad. Otdel. Mat. Inst. Steklov (LOMI) 8, 32–45.
J. Y. Girard [1971], ‘Une extension de l'interprétation de Gödel à l'analyse, et son application à l'élimination des coupures dans l'analyse et la théorie des types’, in: Proceedings of the Second Scandinavian Logic Symposium, J. E. Fenstad (ed.), North-Holland, Amsterdam, pp. 63–92.
J. Y. Girard [1972], ‘Interprétation fonctionnelle et élimination des coupures de l'arithmétique d'ordre supérieur’, Thèse de doctorat d'état, Université Paris VII.
Kurt Gödel [1958], ‘Über eine bisher noch nicht benützte Erweiterung des finiten Standpunktes’, Dialectica 12, 280–287.
Nicolas D. Goodman [1976], ‘The theory of the Gödel functionals’, J. Symbolic Logic 41, 574–582.
A. Grzegorczyk [1964], ‘Recursive objects in all finite types’, Fund. Math. 54, 73–93.
Y. Hanatani [1966], ‘Démonstration de l'ω-non-contradiction de l'arithmétique’, Ann. Japan Assoc. Philos. Sci. 3, 105–114.
Y. Hanatani [1975], ‘Calculatability of the primitive recursive functionals of finite type over the natural numbers’, in: Proof Theory Symposion Kiel 1974, J. Diller and G. H. Müller (eds.), Lecture Notes in Mathematics 500, Springer-Verlag, Berlin, pp. 152–163.
S. Hinata [1967], ‘Calculability of primitive recursive functionals of finite type’, Sci. Rep. Tokyo Kyoiku Daigaku Sect. A, 9, 218–235.
J. R. Hindley, B. Lercher, and J. P. Seldin [1972], ‘Introduction to Combinatory Logic’, London Math. Soc. Lecture Note Series 7, Cambridge U.P.
W. A. Howard [1968], ‘Functional interpretation of bar induction by bar recursion’, Compositio Math. 20, 107–124.
W. A. Howard [1970], ‘Assignment of ordinals to terms for primitive recursive functionals of finite type’, in: Intuitionism and Proof Theory, Proceedings of the Summer Conference at Buffalo, 1968, A. Kino, J. Myhill and R. E. Vesley (eds.), North-Holland, Amsterdam, pp. 443–458.
Georg Kreisel [1959], ‘Interpretation of analysis by means of constructive functionals of finite type’, in: Constructivity in Mathematics, A. Heyting (ed.), North-Holland, Amsterdam, pp. 101–128.
Georg Kreisel [1965], ‘Mathematical Logic’, in: Lectures on Modern Mathematics III, T. L. Saaty (ed.), John Wiley, New York, pp. 95–195.
Georg Kreisel [1968], ‘A survey of proof theory’, J. Symbolic Logic 33, 321–388.
Georg Kreisel [1971], ‘A survey of proof theory II’, in: Proceedings of the Second Scandinavian Logic Symposium, J. E. Fenstad (ed.), North-Holland, Amsterdam, pp. 109–170.
H. Luckhardt [1973], ‘Extensional Gödel functional interpretation. A consistency proof of classical analysis’, Lecture Notes in Mathematics 306, Springer, Berlin.
P. Rath [1978], ‘Eine verallgemeinerte Funktionalinterpretation der Heyting-Arithmetik endlicher Typen’, Dissertation, Münster.
L. E. Sanchis [1967], ‘Functionals defined by recursion, Notre Dame J. Formal Logic 8, 161–174.
Joseph R. Shoenfield [1967], ‘Mathematical Logic’, Addison-Wesley, Reading Mass.
Clifford Spector [1962], ‘Provably recursive functionals of analysis: a consistency proof of analysis by an extension of principles formulated in current intuitionistic mathematics’, in: Recursive Function Theory, J. C. E. Dekker (ed.), Proc. Symp. Pure Math. V, Amer. Math. Soc., Providence RI, pp. 1–27.
M. Stein [1977], ‘Interpretations of Heyting's Arithmetic — an analysis by means of a language with set symbols.
S. Stenlund [1972], Combinators, λ-terms, and proof theory, D. Reidel, Dordrecht.
W. W. Tait [1965], ‘Infinitely long terms of transfinite type, in: Formal Systems and Recursive Functions, J. N. Crossley and M. A. E. Dummett (eds.), North-Holland, Amsterdam, pp. 176–185.
W. W. Tait [1967], ‘Intensional interpretations of functionals of finite type I’, J. Symbolic Logic 32, 198–212.
W. W. Tait [1971], ‘Normal form theorem for barrecursive functions of finite type’, in: Proceedings of the Second Scandinavian Logic Symposium, J. E. Fenstad (ed.), North-Holland, Amsterdam, pp. 353–367.
A. S. Troelstra [1973], ‘Realizability and functional interpretations’, in: Metamathematical Investigation of Intuitionistic Arithmetic and Analysis, A. S. Troelstra (ed.), Lecture Notes in Mathematics 344, Springer, Berlin, pp. 175–274.
M. Yasugi [1963], ‘Intuitionistic analysis and Gödel's interpretation’, J. Math. Soc. Japan 15, 101–112.
Author information
Authors and Affiliations
Rights and permissions
About this article
Cite this article
Gödel, K. On a hitherto unexploited extension of the finitary standpoint. J Philos Logic 9, 133–142 (1980). https://doi.org/10.1007/BF00247744
Issue Date:
DOI: https://doi.org/10.1007/BF00247744