Constructive λ-models

• Main Author: Knobel, Andreas
• Published: University of Edinburgh 1990
• Subjects: 510
• Online Access: http://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.653502

We study λ-models in a constructive setting. We present two novel ways of deriving λ-models. These two definitions make sense classically, but yield nothing of interest. The first extends the structure of a λ-model to its pace of singletons. These two models and all the models inbetween have the same equational theory. The second takes a full function space hierarchy and defines a λ-submodel whose universe consists of those points in the hierarchy that satisfy a logical relation. Call a model obtained in this way extension model. We prove that, given a 'classsical' λ-model, it is consistent with IZF that it be isomorphic to an extension model. Also, this extension model has the same equational theory as the full function space hierarchy from which it was obtained. We prove these claims by building a fairly simple model of IZF in which these statements hold. This set thoeretic model only depends on the cardinality of the original λ-model. We deduce that there is a model of IZF in which there exists a full function space hierarchy for every classical model such that the two have the same theory. We go on to explore the logic of the world where these λ-models exist.