Aczel's V and the notion of set
When philosophers discuss the relation between set theory and type theory, they will usually have in mind simple type theory and, in particular, a hierarchy of function types built over one or two ground types. The type structure of Martin-Löf type theory differs significantly from that of simple type theory. There is, for instance, an indefinite range of ground types, each of which, moreover, is inductively generated (under a suitably general notion of inductive generation). Much light was shed on the relation between set theory and Martin-Löf type theory by Peter Aczel's construction of a model — often called V — of the constructive set theory CZF inside the latter. The construction also has more general significance for the philosophy of set theory — or so it will be argued in this talk. I will first attempt to explain the model construction in a way that is accessible also to those who are unfamiliar with Martin-Löf type theory. Thereafter I will draw some philosophical consequences pertaining to the notion of set and its relation to the notion of type. Intensionality will turn out to play a significant role in this comparison.
The talk will be hybrid in Oslo and on Zoom.
Contact Laura.Crosilla @ ifikk.uio.no for a Zoom-invite.