Hostname: page-component-cd9895bd7-mkpzs Total loading time: 0 Render date: 2024-12-25T09:11:51.888Z Has data issue: false hasContentIssue false
  • English
  • Français

Construction principle and transfinite induction up to ε0

Published online by Cambridge University Press:  09 April 2009

Mariko Yasugi
Mariko Yasugi
Affiliation:
The Institute of Information Science, University of Tsukuba, Sakuramura, Ibaraki, Japan 305
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

What we cail here the “construction principle” is a principle on the ground of which some functionals can be defined; the domain and the range of such a functional consist of some “computable” functionals of various finite types. The principle above is considered here as the basis of the functional interpretation of transfinite induction up to ε0. It is concretely repesented as the “term-forms”, where every term-form is shown to be “computable” in some sense.

Type
Research Article
Information
Journal of the Australian Mathematical Society , Volume 32 , Issue 1 , January 1982 , pp. 24 - 47
Copyright
Copyright © Australian Mathematical Society 1982

References

Diller, J. (1968), ‘Zur Berechenbarkeit primitive-rekursiver Funktionale endlicher Typen’, Contributions to mathematical logic, edited by Schmidt, H. A., Shütte, K., Thiele, H. J., pp. 109–120 (North-Holland Publ. Co., Amsterdam).Google Scholar
Feferman, S. (1970), ‘Formal theories for transfinite iterations of generalized inductive definitions and some subsystems of analysis’, Intuitionism and proof theory, Proceedings of the Summer Conference at Buffalo, N. Y., 1968, edited by Kino, A., Myhill, J., Vesley, R. E., pp. 303–326 (North-Holland Publ. Co., Amsterdam).Google Scholar
Gentzen, G. (1936), ‘Die Widerspruchsfreiheit der reinen Zahlentheorie’, Math. Ann. 112, 493–565.CrossRefGoogle Scholar
Gentzen, G. (1943), ‘Beweisbarkeit und Unbeweisbarkeit von Anfangsfälen der transfiniten Induktion in der reinen Zahlentheorie’, Math. Ann. 119, 140–161.CrossRefGoogle Scholar
Girard, J.-Y. (1971), ‘Une extension de l'interpretation de Gödel a l'analyse et son application a l'elimination des coupures dans l'analyse et la théries des types’, Proceedings of the Second Scandinavian Logic Symposium, edited by Fenstad, J. E., pp. 63–92 (North-Holland Publ. Co., Amsterdam).CrossRefGoogle Scholar
Gödel, K. (1958), ‘Über eine bisher noch nicht benützte Erweiterung des finiten Standpunktes’, Dialectica 12, 280–287.CrossRefGoogle Scholar
Hanatani, Y. (1977), Interpretation Functionnelle de ID1, (Thesis, Université Paris).Google Scholar
Hinata, S. (1967), ‘Calculability of primitive recursive functionals of finitetypes’, Sci. Rep. Tokyo Kyoiku Daigaku Sect. A 9, 218–235.Google Scholar
Hindley, J. R., Lercher, B. and Seldin, J. P. (1972), Introduction to combinatory logic, London Mathematical Lecture Notes Series 7 (C. U. P.).Google Scholar
Kreisel, G. (1959), ‘Interpretation of analysis by means of constructive functionals of finite types’, Constructivity in mathematics, edited by Heyting, A., pp. 101–128 (North-Holland Publ. Co., Amsterdam).Google Scholar
Kreisel, G. (1968), ‘A survey of proof theory’, J. Symbolic Logic 33, 321–388.CrossRefGoogle Scholar
Szabo, M. E. (1969), editor, The collected papers of Gerhard Gentzen (North-Holland Publ. Co., Amsterdam).Google Scholar
Tait, W. W. (1967), ‘Intensional interpretation of functionals of finite type I’, J. Symbolic Logic 32, 198–212.CrossRefGoogle Scholar
Takeuti, G. (1975), Proof theory (North-Holland Publ. Co., Amsterdam).Google Scholar
Yasugi, M. (1963), ‘Intuitionistic analysis and Gödel's interpretation’, J. Math. Soc. Japan 15, 101–112.CrossRefGoogle Scholar
Yasugi, M. (1980), ‘Gentzen reduction revisited’, Publ. Res. Inst. Math. Sci. 16, 1–33.CrossRefGoogle Scholar