Abstract
We give a finitary normalisation proof for the restriction of system F where we quantify only over first-order type. As an application, the functions representable in this fragment are exactly the ones provably total in Peano Arithmetic. This is inspired by the reduction of π1 1-comprehension to inductive definitions presented in [Buch2] and this complements a result of [Leiv]. The argument uses a finitary model of a fragment of the system AF2 considered in Kriv,Leiv.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
W. Buchholz. The ωμ+1-rule. In Iterated Inductive Definitions and Subsystems of Analysis: Recent Proof-Theoretical Studies, volume 897 of Lecture Notes in Mathematics, pages 188–233. 1981.
W. Buchholz and K. Schütte. Proof theory of impredicative subsystems of analysis. Studies in Proof Theory. Monographs, 2. Bibliopolis, Naples, 1988.
M.D. Gladstone. A reduction of the recursion scheme. J. Symbolic Logic 32 1967 505–508.
J.L. Krivine. Lambda-calcul. Types et modèles. Masson, Paris, 1990.
D. Leivant. Peano’s Lambda Calculus: The Functional Abstraction Implicit in Arithmetic to be published in the Church Memorial Volume.
A. Troelstra. Metamathematical Investigations of Intuitionistic Arithmetic and Analysis. Lecture Notes in Mathematics 344, 1973.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Altenkirch, T., Coquand, T. (2001). A Finitary Subsystem of the Polymorphic λ-Calculus. In: Abramsky, S. (eds) Typed Lambda Calculi and Applications. TLCA 2001. Lecture Notes in Computer Science, vol 2044. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45413-6_6
Download citation
DOI: https://doi.org/10.1007/3-540-45413-6_6
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-41960-0
Online ISBN: 978-3-540-45413-7
eBook Packages: Springer Book Archive