Although such properties seem quite natural and are fairly easy to establish for arithmetical theories, they turn out to pose considerable technical challenges in the case of set theories, due to their transfinite hierarchies of sets and the extensionality axiom. In fact, prominent constructive and intuitionistic set theories turn out  not to possess the existence property, as discussed in the next section. 