  In the following we make use of a convention which is often in place today, according to which the adjective “intuitionistic” refers to those set theories, such as IZF, which are impredicative, while “constructive” refers to set theories, such as CZF, which comply with a form of predicativity. Note, however, that this convention is not always followed in the literature. In fact, the adjective “constructive” has also been used to denote impredicative theories, and “intuitionistic” to refer to predicative foundational theories such as Martin-Löf type theory (Martin-Löf 1975; 1984). It is also worth noting that the present convention on the use of the words “constructive” and “intuitionistic” differs from that made in the context of constructive mathematics (see, for example, the entry on constructive mathematics and also Bridges and Richman 1987).