Abstract

In this paper we analyze an extension of Martin-Löf s intensional set theory by means of a set contructor P such that the elements of P are the subsets of the set S. Since it seems natural to require some kind of extensionality on the equality among subsets, it turns out that such an extension cannot be constructive. In fact we will prove that this extension is classic, that is “ true holds for any proposition A