  To summarise, in formulating a set theory based on intuitionistic logic, the first task is to expel the principle of excluded middle, including those instances of it which might be hidden in familiar formulations of set-theoretic axioms. The next task is to choose one version of each classical principle which best characterises the desired notion of set. This opens up a range of choices one can make, as a plurality of intuitionistic principles may correspond to one classical principle. It should be stressed that from a constructive point of view this plurality of options (and thus systems), rather than causing uneasiness, is a highly desirable situation, as it constitutes a form of “axiomatic freedom”. For example, it allows us to differentiate between a number of mathematical notions, thus better capturing our intuitions of them as distinct. It also gives us the freedom to choose the notions and theories which best suit a given context. In addition, by adopting intuitionistic logic we can include within our theories principles which are classically very strong, without having to commit to their classical strength. For example, one can add a notion of inaccessible set to a weak constructive set theory and obtain a predicative theory, while the same notion embedded in a classical context becomes extremely strong (see the sections on  Predicativity in constructive set theory and  Large sets in constructive and intuitionistic ZF). Finally, a rich area of (meta-theoretical) study of the relations between the resulting distinct set-theoretic systems naturally arises. As one could expect, this freedom also has a price, as a highly technical study of the axiomatic theories might be necessary to distinguish their principles as well as to unveil some of their subtleties. This again can be seen as an advantage, since it forces us to a deeper and clearer analysis of the mathematical notions involved and prompts us to develop new sophisticated tools.