Abstract
The presentations of type theory based on a comprehension scheme, a skolemized comprehension scheme and λ-calculus are equivalent, both in the sense that each one is a conservative extension of the previous and that each one can be coded in the previous preserving provability. A similar result holds for set theory.
Preview
Unable to display preview. Download preview PDF.
References
P.B. Andrews, General models, descriptions and choice in type theory, The Journal of Symbolic Logic, 37, 2 (1972) pp. 385–394.
P.B. Andrews, An introduction to mathematical logic and type theory: to truth through proof, Academic Press, Orlando (1986).
A. Church, A formulation of the simple theory of types, The Journal of Symbolic Logic, 5 (1940), pp. 56–68.
H. Curry, An analysis of logical substitution, American Journal of Mathematics, 51 (1929), pp. 363–384.
G. Dowek, Lambda-calculus, combinators and the comprehension scheme, manuscript (1994).
G. Dowek, Collections, types and sets, manuscript (1994).
J.Y. Girard, Y. Lafont, P. Taylor, Types and proofs, Cambridge University Press (1989).
L. Henkin, Banishing the rule of substitution for functional variables, The Journal of Symbolic Logic, 18, 3 (1953), pp. 201–208.
R.J.M. Hughes, Super-combinators, a new implementation method for applicative languages, Proceedings of Lisp and Functional Programming (1982).
D.A. Miller, Proofs in higher order logic, PhD Thesis, Carnegie Mellon University (1983).
D.A. Miller, A compact representation of proofs, Studia Logica, 46, 4 (1987).
T. Skolem, Über die mathematische logik, Norsk Matematisk Tidsskrift, 10 (1928), pp. 125–142.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1995 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Dowek, G. (1995). Lambda-calculus, combinators and the comprehension scheme. In: Dezani-Ciancaglini, M., Plotkin, G. (eds) Typed Lambda Calculi and Applications. TLCA 1995. Lecture Notes in Computer Science, vol 902. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0014051
Download citation
DOI: https://doi.org/10.1007/BFb0014051
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-59048-4
Online ISBN: 978-3-540-49178-1
eBook Packages: Springer Book Archive