Abstract
A system of untyped λ-calculus with a restriction on function abstraction using relative typing analogous to the restriction on set comprehension found in Quine's set theory “New Foundations” is discussed. The author has shown elsewhere that this system is equiconsistent with Jensen's NFU (“New Foundations” with urelements)+Infinity, which is in turn equiconsistent with the simple theory of types with infinity. The definition of the system is given and the construction of a model is described. A semantic motivation for the stratification criterion for function abstraction is given, based on an abstract model of computation. The same line of semantic argument is used to motivate an analogy between the notion of “strongly Cantorian set” found in “New Foundations” and the notion of “data type”; an implementation of absolute types as domains of retractions with strongly Cantorian ranges is described. The implementation of these concepts in a theorem prover developed by the author is sketched.
Supported by the U. S. Army Research Office, grant no. DAAH04-94-G-0247
Preview
Unable to display preview. Download preview PDF.
References
Boffa, M. “ZFJ and the consistency problem for NF”, in Jahrbuch der Kurt Gödel Gesellschaft, 1988, pp. 102–6.
Crabbé, M. On NFU. Notre Dame Journal of Formal Logic, vol. 33 (1992), pp. 112–119.
Forster, T. E. “A semantic characterization of the well-typed formulae of λ-calculus”. Theoretical Computer Science, vol. 110 (1993), pp. 405–418.
Forster, T. E. Set theory with a universal set, Oxford logic guides no. 20. Clarendon Press, Oxford, 1992.
Hailperin, T. “A set of axioms for logic”. Journal of Symbolic Logic, vol. 9 (1944), pp. 1–19.
Holmes, M. R. “Systems of combinatory logic related to Quine's ‘New Foundations'”, Ph.D. thesis, State University of New York at Binghamton, 1990.
Holmes, M. R. “Systems of combinatory logic related to Quine's ‘New Foundations'”. Annals of Pure and Applied Logic, vol. 53 (1991), pp. 103–133.
Holmes, M. R. “Systems of combinatory logic related to predicative and ‘mildly impredicative’ fragments of Quine's ‘New Foundations'”. Annals of Pure and Applied Logic, vol. 59 (1993), pp. 45–53.
Holmes, M. R. “The set-theoretical program of Quine succeeded, but nobody noticed”. Modern Logic, vol. 4, no. 1 (1994), pp. 1–47.
Holmes, M. R. “Strong axioms of infinity in NFU”, preprint.
Jensen, R. B. “On the consistency of a slight (?) modification of Quine's NF”. Synthese, vol. 19 (1969), pp. 250–63.
Rosser, J. B. Logic for Mathematicians. McGraw-Hill, reprinted (with appendices) by Chelsea, New York, 1978.
Scott, Dana. “Continuous lattices”, in Springer Lecture Notes in Mathematics, no. 274, pp. 97–136.
Wang, H. “Negative types”. Mind, vol. 61 (1952), pp. 366–8.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1995 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Holmes, M.R. (1995). Untyped λ-calculus with relative typing. 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/BFb0014056
Download citation
DOI: https://doi.org/10.1007/BFb0014056
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