Untyped λ-Calculus with Relative Typing

A system of untyped λ-calculus with a restriction on function abstraction using relative typing analogous to the restriction on set comprehension found in Quine\u27s set theory “New Foundations” is discussed. The author has shown elsewhere that this system is equiconsistent with Jensen\u27s 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