## 1. The Essence of Constructive and Intuitionistic Set Theory




Constructive and intuitionistic Zermelo-Fraenkel set theories are
based on intuitionistic rather than classical logic, and 
represent a natural environment within which to codify and study 
mathematics based on intuitionistic logic. 
For constructive ZF, the main focus has been 
to represent the mathematical
practice of Bishop (Bishop 1967, Bishop and Bridges
1985).




For the basic concepts and the driving ideas of intuitionistic logic,
constructive mathematics and intuitionism, the reader may wish to
consult the following entries:


* intuitionistic logic,
* the development of intuitionistic logic,
* constructive mathematics,
* intuitionism in the philosophy of mathematics,
* Luitzen Egbertus Jan Brouwer.




For classical set theory, see the entry on
 set theory.




Constructive and intuitionistic ZF are based on the same first-order
language as classical ZF set theory,
which has only the binary predicate symbol \(\in\) (membership) as
non-logical symbol. That is, they are formulated on the basis of
intuitionistic first-order logic with equality, plus the binary
predicate symbol \(\in\). We can thus take advantage of the simplicity
of the set-theoretic language and of our familiarity with it (Myhill
1975). As with Bishop-style constructive mathematics, Constructive and
intuitionistic ZF are *compatible* with the classical
tradition, in the sense that all of their theorems are *classically
true*. In fact, the two formal systems that we shall consider,
Constructive Zermelo-Fraenkel (CZF) and Intuitionistic
Zermelo-Fraenkel (IZF), give rise to full classical ZF by the simple
addition of the principle of the excluded middle.


### 1.1 Axiomatic freedom




Classical Zermelo-Fraenkel set theory is based on classical
first-order predicate logic with equality. On top of the logical
principles are axioms and schemata which describe the notion of set
the theory codifies. These principles can be classified into three
kinds. First, there are principles that enable us to form new sets
from given ones. For example, the axiom of pair allows us to form a
set which is the pair of two given sets. Secondly, there are
principles that establish properties of the set theoretic
structure. For example, the axiom of extensionality identifies all
sets having the same elements. Third, and finally, there are axioms
asserting the existence of specific sets. Thus the axiom of infinity
states that there is an infinite set. These principles all together
are usually called the set-theoretic principles.




When introducing versions of ZF based on intuitionistic logic, the
first step is to eliminate from the logic the principle of the
excluded middle (EM). The next step is to choose a good stock of
set-theoretic principles which faithfully represent the desired notion
of constructive set. These tasks turn out to be more challenging than
one at first might have expected. In fact, as is well known, systems
based on a "weaker" logic have the ability to distinguish
between statements which are equivalent from the point of view of a
"stronger" logic. In the case of set theory, some of the
ZF axioms or schemata are often presented by one of many classically
equivalent formulations. Classically it is only a matter of
convenience which one to use at a specific time. When working on the
basis of intuitionistic logic, however, various formulations of a
classical axiom may turn out to be distinct (non-equivalent). In fact,
one can envisage new statements which are classically equivalent to a
ZF axiom but intuitionistically separate from it (for example CZF's
subset collection axiom (Aczel 1978)).




As to the first step, consisting in eliminating the principle of
excluded middle from the logic, it turns out that simply evicting this
principle from the underlying logic is insufficient; that is, it is
not enough to take the intuitionistic rather than the classical
predicate calculus as our basis. We also need to ensure that the set
theoretic axioms do not bring undesirable forms of excluded middle
back into our theory. For example, as noted by Myhill (1973), we need
extra care in choosing an appropriate statement for the axiom of
foundation. Foundation is introduced in set theory to rule out sets
which are members of themselves and thus \(\in\)-chains of sets. The
usual formulation of foundation asserts that each inhabited set (a set
with at least one element) has a least element with respect to the
membership relation. This statement, however, can be shown to yield
constructively unacceptable instances of excluded middle on the basis
of modest set-theoretic assumptions. Therefore the usual formulation
of foundation has to be omitted from a set theory based on
intuitionistic logic. For a proof, see the supplementary document:



> Set-theoretic principles incompatible with intuitionistic logic.


The typical move in formulating set theories based on
intuitionistic logic is then to replace foundation with the
classically equivalent schema of set induction, which does not have
the same "side effects" but has similar
 consequences.[1]


As to the second step, related to the selection of a good stock of 
set-theoretic principles, the schemata of replacement and
separation, and the axiom of power set have attracted most attention. For
the exact formulation of these principles see the supplementary
document:



> Axioms of CZF and IZF.




Here the following is a typical scenario. Given what are classically two variants
of a single set-theoretic principle, their classical proof of equivalence requires 
at some point an instance of the excluded middle. However, in general this
proof of equivalence will not carry through to an
intuitionistic context, and thus what are classically two forms of one principle
may result into two distinct principles when working intuitionistically. 
Choosing one rather than
the other of them may therefore influence the notion of set we thus define. 
In the context of *constructive* set theories like CZF, power set and 
separation are 
replaced by intuitionistically weaker principles. One reason for this is that 
the full strenght of power set and full separation are seen as unnecessary, 
since their weaker substitutes seem to 
suffice for carrying out constructive mathematics. Another reason is that they 
are seen as philosophically problematic, since they may introduce forms of
impredicativity within the set theory (see the section on
 Predicativity in constructive set theory).
The case of replacement versus collection is somehow more complex (see,
for example, the articles (Friedman and Scedrov 1985), (Rathjen 2005)
and (Rathjen 2012)). It is worth stressing that while adopting the
usual formulation of foundation goes against the very assumption of
intuitionistic logic as background logic, the principles of separation
and power set have no incompatibility with intuitionistic logic at
all, so much so that they are integral part of the intuitionistic
theory of sets IZF (Friedman 1973a).





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.


### 1.2 Constructive versus intuitionistic set theory




Although there are many systems of sets based on
intuitionistic logic, we can distinguish two main trends within the
literature. According to the first one, we take all of what is
available in classical ZF set theory and only modify those principles,
such as foundation, which have a clear incompatibility with
intuitionistic logic. This gives rise to set theories such as
Intuitionistic Zermelo-Fraenkel,
 IZF,
a variant of which was introduced as early as in (Friedman
1973a). (See Beeson 1985, Chapters 8 and 9 and Scedrov 1985 for two
surveys on IZF.) The rationale behind these theories appears to be
that of granting the mathematician the most powerful tools possible,
as long as compatibility with intuitionistic logic is
preserved. According to the second approach, in addition to the
adherence to intuitionistic logic we also introduce restrictions on
the set-theoretic principles admitted, as far as the resulting system
complies with the constructive mathematical practice. Theories of
this second kind can thus be seen as the outcome of a double process
of restriction with respect to classical ZF. First there is a
restriction to intuitionistic logic, then a restriction is imposed on
the set-theoretic constructions allowed. The latter is motivated by
(1) the observation that weaker principles appear to suffice for the
constructive mathematical practice and (2) the desire to adhere to a
form of predicativity (see the next section for a clarification of
this notion of predicativity). Paradigmatic examples of the latter
kind of systems are Myhill's Constructive Set Theory (Myhill 1975),
Friedman's system B (Friedman 1977) and Aczel's Constructive
Zermelo-Fraenkel set theory
 CZF
 (Aczel 1978; 1982; 1986, Aczel & Rathjen
2001; Aczel & Rathjen 2010, Other Internet Resources). We can also say that in this second approach the foundational
motivation influences the practice to a higher degree.




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-Lof type theory
(Martin-Lof 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).


### 1.3 Predicativity in constructive set theory




Predicativism has its origins in the writings of Poincare and
Russell, who responded to the paradoxes that were discovered in
Cantor's and Frege's set theories in the early 20th
century. Subsequently Weyl made fundamental contributions to the study
of predicative mathematics (Weyl 1918, see also Feferman 1988).
According to one notion, a definition is *impredicative* if it
defines an object by reference to a totality which includes the object
to be defined. With his Vicious Circle Principle (VCP), Russell
intended to eliminate the circularity in mathematics that arises from
such impredicative definitions. Russell gave various formulations of the VCP, one of which is:



> 
>  Whatever contains an apparent variable must not be a possible value
>  of that variable (Russell 1908, in van Heijenoort 1967, 163).
> 




Poincare, Russell and Weyl's foundational analysis of
predicativity has paved the way for a variety of logical analyses of
the notion. The most commonly accepted analysis is due to Feferman and
Schutte (independently) following lines indicated by Kreisel
(Kreisel 1958, Feferman 1964 and Schutte 1965; 1965a). Here
proof theory has played a pivotal role. In very rough terms, the idea
was to single out a collection of theories (a transfinite progression
of systems of ramified second order arithmetic indexed by ordinals) by
means of which to characterise a certain notion of predicative
ordinal. Feferman and Schutte's proof theoretic analysis of these
theories has identified an ordinal, usually referred to as
\(\Gamma\_0\), which is the least non-predicative ordinal
according to this notion. A formal system is considered 
*predicatively justifiable* if it is proof-theoretically reducible to a
system of ramified second order arthmetic indexed by an ordinal less
then \(\Gamma\_0\). Therefore in proof theory
\(\Gamma\_0\) is usually considered as representing the limit of
predicativity. (See Feferman 2005 for a more accurate informal
account of this notion of predicativity and for further
references. See also Crosilla 2017. The reader may also consult the section on
 predicativism
 in the entry on philosophy of mathematics and the entry on
 paradoxes and contemporary
logic).




For *constructive* foundational theories a more
"liberal" approach to predicativism has been suggested,
starting from work in the late 1950's of Lorenzen, Myhill and Wang
(see *e.g.* Lorenzen and Myhill 1959). The driving idea is that
so-called *inductive definitions* ought to be allowed in the
realm of constructive mathematics. The intuitive justification of
inductive definitions is related to the fact that they can be
expressed by means of finite rules, in a "bottom-up" way.
The proof-theoretic strength of theories of inductive definitions goes
well beyond Feferman and Schutte's bound (Buchholz, Feferman,
Pohlers and Sieg 1981). Thus relatively strong theories are considered
predicative in today's foundations of constructive mathematics. This
more liberal notion of predicativity has often been
termed *generalised predicativity*. In this entry we 
simply write *predicativity* for generalised predicativity and call 
*predicativity given the natural numbers* the better known form of predicativity which arises in the classical context and was analysed by Kreisel, Feferman and Schutte.


An example of a predicative theory in this sense is the
constructive set theory CZF, as its proof-theoretic strength is the
same as that of a theory of one inductive definition known as
ID\(\_1\). The system IZF, instead, is impredicative, as its
proof-theoretic strength equates that of the whole of classical ZF
(Friedman 1973a).




In set theories based on intuitionistic logic, predicativity is usually
achieved by restricting the principles of separation and power set, as
these appear to be the main sources of impredicativity (when the
infinity axiom is assumed). 


#### 1.3.1 Impredicativity of Separation




The schema of separation allows us to form a subset of a given set
whose elements satisfy a given property (expressed by a formula in the
language of set theory). Given a set \(B\) and a formula \(\phi(X)\),
separation allows us to construct a new set, the set of those elements
\(X\) of \(B\) for which \(\phi\) holds. This is usually informally
represented as: \(\{X \in B : \phi(X)\}\). Separation may lead to
impredicativity in case the formula \(\phi\) contains unbounded
quantifiers ranging over the whole universe of sets; in fact, in
defining the new set by separation we may thus refer to this very set,
contradicting Russell's VCP. For example, if we define a set
\(C\) by separation as \(\{X\in B : \forall Y \psi(X,Y)\}\), then
\(C\) is among the \(Y\)'s that need to be checked for the
property \(\psi\). This form of impredicativity is avoided in
constructive set theory by restricting the separation schema: by
requiring that all quantifiers occurring in the formula \(\phi\) range
only over "previously constructed" sets. Syntactically,
this means that given a set \(B\), we can form a new set \(\{X \in B :
\phi(X)\}\) by separation only if all quantifiers in \(\phi\) are
bounded; that is, only if all quantifiers in \(\phi\) are of the form
\(\forall X (X\in Y \rightarrow \ldots)\) or \(\exists X(X\in Y \wedge
\ldots)\), for some set \(Y\).



We can see that constraining separation in this way avoids impredicativity, by 
observing that the
proof theoretic strength of CZF, which has only restricted separation,
is within the range of predicativity. However, by adding full
separation to CZF one obtains an impredicative theory, in fact, one
with the same proof-theoretic strength as full second order arithmetic
(Lubarsky 2006). See also Section 5 for a discussion of the role of proof theory
in analysing constructive and intuitionistic set theories. 


#### 1.3.2 Impredicativity of Powerset




The power set axiom allows us to form a *set* of all subsets of
a given set. An example of impredicative use of power set is given by
the definition of a subset of the natural numbers, \(N\), as follows:
\(B := \{n \in N : \forall C \subseteq N \phi(n, C)\}\), where
\(\phi\) can be taken to be a bounded formula. A form of circularity
arises here as \(B\) itself is among the subsets of \(N\) which need
to be checked for \(\phi\). As emphasized by Myhill (1975, 354), power
set is hard to justify from a constructive point of view: it gathers
together all the subsets of a given set, but does not prescribe a rule
that "constructs" the set out of previously given sets, as
predicativity would seem to require.



Myhill writes:



> Power set seems especially nonconstructive and
> impredicative compared with the other axioms: it does not involve, as
> the others do, putting together or taking apart sets that one has
> already constructed but rather selecting out of the totality of all
> sets those that stand in the relation of inclusion to a given
> set. (Myhill 1975, 351).



Power set seems particularly problematic in the case of infinite sets, 
as "we have no idea of what an arbitrary subset of an infinite set is; there is no way of generating them all and so we have no way to form the set of all of them" (Myhill 1975, 354).
As a consequence, there seems to be no way of giving constructive sense to the set of all subsets of an infinite set. 



Myhill crucially observes that power set is not needed for constructive 
mathematics Bishop-style, as it can be replaced by one of its
consequences. This is often called Myhill's *exponentiation
axiom* and states that we can form a *set* of all functions
from one given set to another. This axiom is clearly
equivalent to power set in a classical context, where subsets of a
given set may be represented by characteristic functions. In the
absence of the principle of excluded middle, however, power set and
exponentiation are not equivalent.
Myhill's fundamental observation is that exponentiation suffices to carry out 
the mathematics of (Bishop 1967); for example, it allows for 
the construction of the (Cauchy) real numbers within constructive set theory. 
Myhill claims that exponentiation is constructively meaningful because a function is a rule, 
a finite object which can actually be given.



He also writes that the case of power set is different from that of
exponentiation as:



> even in the case of infinite sets \(A\) and \(B\) we do
> have an idea of an arbitrary mapping from \(A\) into \(B\). An
> arbitrary mapping from \(\mathbf{Z}\) into \(\mathbf{Z}\) is a partial
> recursive function together with a proof that the computation always
> terminates; a similar account can be given of an arbitrary real
> function. There is no corresponding explanation of
> "arbitrary *subset*". (Myhill 1975,
> 354).




Myhill's exponentiation axiom is now part of all major systems of
constructive set theory. In the case of CZF, in fact, one has a
strengthening of exponentiation, known as subset collection, which is
also a weakening of power set. A generalisation of exponentiation can
also be found in constructive type theory.



In the case of CZF, the claim that adding the power set axiom 
induces a form of impredicativity can
be substantiated by a technical result. Rathjen (2012b) shows that CZF
augmented by the power set axiom exceeds the strength of classical Zermelo set theory,
and thus the addition of the power set axiom to CZF 
brings us to a fully impredicative theory. This also shows that the
implication from power set to subset collection can not be reversed,
as CZF's proof-theoretic strength is way below that of Zermleo
set-theory. In other terms, the power set axiom is much stronger than 
both exponentiation and subset collection. 


#### 1.3.3 The constructive universe of sets




Having introduced appropriate constraints to power set and separation,
we could now face a substantial objection. Constructive and
intuitionistic set theories can be seen as modifications of classical
ZF set theory that are obtained by: (1) replacing classical with
intuitionistic logic, and (2) accurately choosing, among various
classically equivalent principles, those which seem more appropriate
for given purposes. For example, we might choose principles which
suffice to represent a certain mathematical practice, like, for
example, Bishop style mathematics. The resulting notion of set,
however, might become obscure and the choice of the set-theoretic
principles might appear to a certain degree as arbitrary. In the case
of intuitionistic ZF, one can justify the choice of the set-theoretic
principles by examining its semantical interpretations, as Heyting
semantics, or by looking at its categorical models. In the case of
constructive set theory, to hinder this kind of objection, Aczel has
given an interpretation of CZF in a version of Martin-Lof type
theory (Aczel 1978). The claim is that a clear constructive meaning is
thus assigned to CZF's notion of set by looking at its meaning in
Martin-Lof type theory, since the latter is usually considered as
representing an accurate and fully motivated formulation of a
constructive notion of set. Aczel's interpretation of CZF in
constructive type theory is given by interpeting sets
as *trees* in type theory. That is, in constructive type theory 
the universe of sets of CZF is represented by a type, V, of iterative sets built over the
universe, U, of small types (Aczel 1978;
Martin-Lof 1984). This interpretation clearly highlights the
(generalised) predicativity of CZF, whose sets can be seen as trees built up inductively, and whose set theoretic universe also has a clear inductive
structure.



The predicativity of CZF and related systems is consonant with
philosophical positions which are often associated with the use of
intuitionistic logic. In particular, it would seem that if
we *construct* the mathematical objects, for example, if the
mathematical objects are mental constructions of some kind, then
resorting to impredicative definitions would produce an undesirable
form of circularity. This clearly contrasts with a view often
associated to classical set theory, for which our mathematical
activity can be seen as a gradual disclosure of properties of the
universe of sets, whose existence is independent from us. Such a view is
usually bound up with the use of classical logic and impredicativity
in studying the set-theoretic universe. Predicativity is also often
seen as related to the time-honoured distinction between actual and
potential infinity. Predicative (and thus, in particular,
constructive) theories are often seen as avoiding reference to actual
infinity, and only committing to potential infinity (Dummett 2000,
Fletcher 2007). This again seems particularly in harmony with those
philosophical positions which highlight the human dimension of our
mathematical activity, by seeing, for example, the mathematical
objects and the truth of statements about them as dependent on
us. Another related aspect is often seen as pertaining to
predicativity: if the universe of sets is built up in stages by our
own mathematical activity, then it would be natural also to see it
as *open ended*. For this reason, in a constructive context,
where the rejection of classical logic meets the requirement of
predicativity, the universe of sets is often described as an open
concept, a universe "in fieri". This idea is especially
well exemplified within constructive type theory, where the notion of
type-theoretic universe has been deliberately left open by Per
Martin-Lof (by not postulating specific elimination rules for
it). The open ended nature of the universe of sets has paved the way
for extensions of it by reflection principles. These have been
investigated both within type theory and constructive set theory. See
(Rathjen 2005a) for a survey of results and a foundational discussion,
and also section 5.2. 
For a formal analysis of the constructive universe of sets and a comparison with the Von Neumann hierarchy, see (Ziegler 2014). 


## 2. Origins of Constructive and Intuitionistic Set Theories




Intuitionistic versions of Zermelo-Fraenkel set theories were
introduced in the early 1970s by Friedman and Myhill. In (Friedman
1973) the author presents a study of formal properties of various
intuitionistic systems and introduces for them an extension of
Kleene's realisability method. The realisability technique is applied
in (Myhill 1973) to show the existence property for a version of
intuitionistic Zermelo-Fraenkel set theory (with replacement in place
of collection). In another fundamental contribution Friedman extends
the double negation translation of intuitonistic logic to relate
classical and intuitionistic set theories (Friedman 1973a). These
first papers already address the relation between some major
intuitionistic set theories and classical ZF. They also clarify a key
feature of set theory based on intuitionistic logic, mainly that it is
amenable to powerful constructive semantic interpretations, like
realizability. These techniques are applied to the study of crucial
metatheoretical properties which are typical of the constructive
approach and which are enjoyed by some constructive set theories (see
the section on
 Semantic techniques). 
This groundbreaking work has been fully exploited and substantially
extended in work by Beeson and McCarty (see Beeson 1985; McCarty
1984).




Constructive set theory from the very start has a more distinctive
foundational vocation and it is bound up with Bishop's mathematics. In
fact, in 1967 Bishop published the book "Foundations of
constructive analysis" (Bishop 1967), which opened up a new era
for mathematics based on intuitionistic logic (see the entry on
 constructive mathematics).
The monograph stimulated fresh attempts in the logical community to
clarify and formally represent the principles which were used by
Bishop, though only at an informal level. First attempts by Goodman
and Myhill (Goodman and Myhill 1972) made use of versions of
Godel's system T (see also (Bishop 1970) for a similar
attempt). Myhill, however, reached the conclusion that the resulting
formalisation was too complex and artificial (Myhill 1975,
347). Myhill proposed instead a system which is closer to the informal
notion of set originally utilised by Bishop and also closer to the
set-theoretic tradition. Myhill writes (1975, 347):



> We refuse to believe that things have to be this complicated -
> the argumentation of (Bishop 1967) looks very smooth and seems to 
> fall directly from a certain concept of what sets, functions, etc. are, and
> we wish to discover a formalism which isolates the principles underlying 
> this conception in the same way that Zermelo-Fraenkel set theory
> isolates the principles underlying classical (nonconstructive)
> mathematics. We want these principles to be such as to make the
> process of formalization completely trivial, as it is in the classical
> case.




We observe here that Myhill's constructive set theory had
distinguished notions of function, natural number and set; it thus
closely represented a constructive tradition in which functions and
natural numbers are conceptually independent from sets. Another
fundamental step in the development of constructive set theory was
Friedman's "Set-theoretical foundations for constructive
analysis" (Friedman 1977). Here, among other systems, a system
called B is defined which has further restrictions on the
set-theoretic principles compared with Myhill's (in particular, it has
no set induction). It also has a restricted form of the axiom of
dependent choice. System B is there shown to be expressive enough to
represent the constructive analysis of Bishop (1967) whilst being at
the same time proof-theoretically very weak (due to the absence of set
induction). System B is in fact a conservative extension of
arithmetic (thus it is well below the limit of predicativity given the natural numbers
briefly recalled in section
 1.3).
 Myhill and Friedman's systems were
subsequently modified by Aczel, to obtain a system, CZF (Constructive
Zermelo-Fraenkel), that is fully compatible with the ZF language
(Aczel 1978, 1982, 1986; Aczel and Rathjen 2001; 2010). CZF also
included no choice principles. Aczel gave an interpretation of CZF in
Martin-Lof type theory with the aim of corroborating the
constructive nature of the set theory. He also strengthened some of
the principles of Myhill's system (namely, collection and
exponentiation) on the ground that the stronger versions are still
validated by the interpretation in type theory.




Other foundational systems for
Bishop-style constructive mathematics were introduced in the early
1970's. For example: *explicit mathematics* by S. Feferman
(Feferman 1975), and the already mentioned *Intuitionistic Type
Theory* (Martin-Lof 1975; 1984). 
Constructive type theory is usually considered the 
most satisfactory foundation for constructive mathematics Bishop-style. 
Both type theory and explicit mathematics can be seen as expressing 
more directly the computational 
content of constructive mathematics. Type theory, in particular, 
can be read as a very general and expressive programming language. 
Constructive and intuitionistic set
theories display their computational
content only indirectly through their semantic interpretations
(see *e.g.* (Aczel 1977), (Lipton 1995) and the section on
 Semantic techniques).


## 3. The Axioms Systems CZF and IZF




For a reader who is already familiar with ZF set theory, we now
briefly recall the axioms of the systems CZF and IZF. For a full list
and an explanation of their axioms we refer instead to the
supplementary document:



> Axioms of CZF and IZF.




CZF and IZF are formulated on the basis of
 intuitionistic first-order logic
with equality, having only \(\in\) (membership) as an additional
non-logical binary predicate symbol. Their set-theoretic axioms are as
follows.




|  |  |
| --- | --- |
| \(\mathbf{IZF}\) | \(\mathbf{CZF}\) |
| Extensionality | *(same)* |
| Pair | *(same)* |
| Union | *(same)* |
| Infinity | *(same)* |
| Separation | Restricted Separation |
| Collection | Strong Collection |
| Powerset | Subset Collection |
| Set Induction | *(same)* |



Note that in IZF the schema of separation is unrestricted.
In CZF, Collection is strengthened to compensate for restricted separation.
Subset collection is a strengthening of Myhill's exponentiation axiom,
thus substituting for ZF's Powerset. 


## 4. Constructive Choice Principles




When discussing the role of classical set theory as a foundation for
mathematics, one usually considers the theory ZFC, that is, the axiom
system ZF plus the axiom of choice (AC). One might therefore wonder
what is the status of the axiom of choice in intuitionistic
settings. The question is particularly significant because at its
first appearance the axiom of choice was often seen as controversial
and highly non-constructive. In constructive contexts, however, one
witnesses a peculiar phenomenon. The usual form of the axiom of choice
is validated by theories of types such as Martin-Lof type theory,
where the Curry-Howard correspondence holds
(See Section 3.4
 of the entry on
 Constructive mathematics). 
On the other hand, the assumption of the axiom of
choice gives rise to instances of the excluded middle
in *extensional* contexts, where a form of separation is also
available. This is the case, for example, of constructive and
intuitionistic ZF. (For the proof, see the supplementary document
on Set-theoretic Principles Incompatible with Intuitionistic Logic.) 
A proof of the
incompatibility of AC with extensional set theories based on
intuitionistic logic seems to have first appeared in (Diaconescu 1975)
in a categorical context. Goodman and Myhill give an argument for set
theories based on intuitionistic logic (Goodman and Myhill 1978). 




Although the axiom of choice is incompatible with both constructive
and intuitionistic ZF, other choice principles may be added to the
basic systems without producing the same undesirable results. For
example one could add the principle of *countable choice*
(AC\(\_0)\) or that of *dependent choice* (DC). In fact, 
both have been often
employed in the constructive mathematical practice. 
(For their exact formulation see the supplementary document on 
Axioms of CZF and IZF.)



In (Aczel 1978) the author also considered a choice principle called the *Presentation
Axiom*, which asserts that every set is the
surjective image of a so-called *base*. A base is a set,
say \(B\), such that every relation with domain \(B\)
extends a function with domain \(B\).



The compatibility of all these forms of choice with constructive set
theory has been proved by Aczel by extending his
interpretation of CZF in Martin-Lof type theory (Aczel
1982). Rathjen (2006) has also considered various constructive choice
principles and their mutual relations.




A final remark: although constructive and intuitionistic set theories
are compatible with the principles of choice just mentioned, the set
theories are often defined without any choice principles. This has
the aim of allowing for a "pluralistic" foundational
approach. In particular, one would like to obtain a foundational
theory compatible with those contexts (*e.g.* categorical models
of set theory) in which even these weaker principles of choice may not be
validated. For similar ideas in the context of constructive type
theory, see (Maietti and Sambin 2005, Maietti 2009). We wish also to mention here
Richman's appeal for a constructive mathematics which makes no
use of choice principles (Richman 2000; 2001).


## 5. Proof Theory and Semantics of Constructive and Intuitionistic ZF




In considering a certain mathematical practice (or a theory used to
codify it) from a philosophical perspective, we need to clarify
with the greatest possible precision the assumptions which are made
within it as well as the consequences which arise from those
assumptions. This is particularly true when working with theories
which are based on a weaker logic than the classical one, for which a
deeper, more precise insight is mandatory. Many technical tools are
available which can help us clarify those aspects. Among the available
instruments, there are proof-theoretic techniques, such as
proof-theoretic interpretations, as well as semantic techniques, such
as realisability, Kripke models, Heyting-valued semantics. In fact, in
the literature one often witnesses the interplay of proof-theoretic
and semantic techniques. We here give a cursory look into some of
these topics and suggest further reading.


### 5.1 Proof-theoretic strength



A fundamental theme in proof theory (in particular in the branch of
this discipline known as ordinal analysis) is the classification of
theories by means of transfinite ordinals which measure their
"consistency strength" and "computational power". These ordinals give
an indication of how strong a theory is, and therefore offer a way of
comparing different theories. For example, the ordinal
\(\varepsilon\_0\) is the proof-theoretic ordinal of Peano Arithmetic,
and is much smaller than the ordinal \(\Gamma\_0\), usually referred to
as "the limit of predicativity" 
 (see section 1.3 above). 
 This is indicative that there are predicatively acceptable theories
which are much stronger than Peano Arithmetic. 



As discussed in section 1, the step
from classical ZF to its intuitionistic variants requires us to choose
a suitable formulation for each set-theoretic axiom: one classical 
axiom may have a number of intuitionistic variants which turn out to be 
non-equivalent to each other. This is sometimes reflected by the proof-theoretic
strength of the resulting theories, which may vary depending on which principles we choose. 
For example, we already noted that 
in CZF we do not have full separation and power set, which are 
replaced by the predicatively acceptable principles of bounded separation and 
subset collection, respectively. However, if
we add to CZF either of these principles, we obtain impredicative
theories. The impredicativity of the resulting theories is witnessed 
by the fact that their proof-theoretic strenght far exceeds that of CZF.



It is not surprising that investigations on the proof-theoretic
strength of constructive and intutionistic set theories have been a
crucial meta-theoretical tool for understanding these theories and
their relations with each other. Investigations on the
proof-theoretic strength of a theory are rich and informative. In
particular, Feferman (1993) has argued that a proof-theoretic analysis
may help us establish whether a certain theory complies with a given
philosophical framework: for example, the analysis may reveal that a
theory is predicative or finitistic etc. Furthermore, as a by-product
of the proof-theoretic analysis we sometimes obtain simple
independence proofs. In fact, we can show that a theory cannot prove a
specific principle because adding it to the theory would increase the
theory's proof-theoretic strength. For example, CZF does not prove the
powerset axiom, as the addition of powerset to CZF gives rise to a
much stronger theory. Proof-theoretic interpretations have also been
employed to compare constructive and intuitionistic ZF set theories
among each others, as well as with their classical counterparts, and
also with other foundational systems for constructive mathematics,
such as constructive type theory and explicit mathematics (see
e.g., Griffor and Rathjen 1994, Tupailo 2003). For a definition
of the notion of proof-theoretic strength and for surveys on proof
theory see, for example, (Rathjen 1999, 2006b). 




Although CZF and IZF are the most widely studied systems, numerous
other systems for constructive and intuitionistic set theory have been
considered in the literature so far. The proof-theoretic strength of a
number of constructive and intuitionistic set theories has been
established by a variety of tools, like, for example, an extension to
set theory of the double negation interpretation (originated in
(Friedman 1973a)), and a variety of other proof-theoretic
interpretations, often resulting from a careful combination of
semantic and proof theoretic techniques. In many cases the proof
theoretic strength of a system has been determined by a chain of
interpretations between constructive and classical systems, and by
using a variety of tools, from relisability to more "traditional"
proof theoretic techniques, as ordinal analysis (see, for example,
Beeson 1985; Griffor and Rathjen 1994; Rathjen 2012b). In particular,
realisability has turned out to be very useful, due to its
flexibility. As to the outcomes of these investigations, some of the
systems analysed turn out to be as weak as arithmetic, as, for example,
Friedman's system B (Friedman 1977); other systems are as strong as
full classical ZF, as IZF (Friedman 1973a). There are also systems of
intermediate strength, as CZF. The strength of the latter theory, in
fact, equals that of a theory of one inductive definition known as
ID\(\_1\). The fact that CZF has the same strength as
ID\(\_1\) is taken to confirm the (generalised) predicativity of the set
theory, and to prove that it exceeds the limit of predicativity given 
the natural numbers, since ID\(\_1\)'s proof theoretic ordinal is well above 
\(\Gamma\_0\).




As a final remark: while the strength of CZF is well below that of 
second-order arithmetic, the simple addition of excluded middle to CZF
gives us (full) ZF. This should be contrasted with IZF, which already
has the strength of ZF (Friedman 1973a). The limited 
proof theoretic strength of CZF compared with IZF has often been considered one of 
the main advantages of constructive over intuitionistic set
theory. In a sense, it would seem that CZF makes the most of 
its use of intuitionistic logic, as it characterises a notion of 
(generalised) predicative set which is sufficiently strong for 
the development of much of constructive mathematics but also 
weak enough to avoid impredicativity.
Interestingly, when some large set axioms have been added to
constructive set theory, a similar pattern has emerged, as the
strength of the resulting theory is well below that of the
corresponding classical theory.


### 5.2 Large sets in constructive and intuitionistic ZF




A prominent area of research in classical set theory is that of large
cardinals (see the entry on
 set theory). In constructive contexts, the ordinals are not linearly
ordered. (For the notion of constructive ordinal and a brief
discussion of its properties, see the supplementary document on: 
Set-theoretic Principles Incompatible with Intuitionistic Logic.) 
 As a consequence, cardinal numbers do not play the same role as in the classical
 setting.




One can nonetheless study the impact of "reflection
principles" of the form of *large set axioms*.
For example, one can add to constructive and intuitionistic set theories 
an axiom asserting the existence of inaccessible 
sets.[2] 
 The addition of large set axioms to intuitionistic ZF was first proposed
by Friedman and Scedrov (Friedman and Scedrov 1984). One of their
aim was to shed light on the corresponding classical
notions; another was to study the impact of these principles on
metatheoretical properties of the original set theories. Friedman and
Scedrov have shown, for example, that the addition of large set axioms
does not compromise the validity of the disjunction and numerical
existence properties for IZF.




In the context of constructive set theory, large sets have been
introduced by Aczel in the form of so-called *regular sets* to
allow inductive definitions of sets (Aczel 1986). Rathjen and Crosilla
have considered inaccessible sets (Rathjen al. 1998; Crosilla and
Rathjen 2001) and Mahlo sets (Rathjen 2003a). Nevertheless, an
objection could be raised to extensions of constructive set theory by
large set axioms. In classical set theory, large cardinals can be seen
as an incarnation of higher infinity. How do we justify these
principles constructively? The constructive justification of these
notions relies again on the type theoretic interpretation. The
addition of these principles corresponds in fact to that of universes
and \(W\)-types within constructive type theory. The
justification of extensions by large sets is thus bound up with the
question of the limits of Martin-Lof type theory (Rathjen
2005). We also note that the addition of inacessible set axioms
 to a weak subsystem of CZF
(with no set induction) produces a theory of strength
\(\Gamma\_0\), the ordinal singled out by Feferman and
Schutte as the limit of predicativity given the natural numbers (Crosilla and
Rathjen 2001; see also section 1.3). This is 
witness to the fact that by working in a constructive, predicative
context, we can tame traditionally strong set-theoretic notions.



Crosilla and Rathjen's set theory with inaccessible sets (but no set
induction) is proof theoretically rather weak, but mathematically
quite expressive. For example, it has been used to verify that the
addition of Voevodsky's Univalence Axiom to Martin-Lof type
theory does not engender impredicativity (Rathjen 2017). The axiom of
Univalence was introduced by Voevodsky as part of his Univalent
Foundations programme (Voevodsky 2015). (For Univalent Foundations,
see the entries on 
 type theory 
and on
 intuitionistic type theory). 
Voevodsky gave a model of constructive type theory with
the Univalence Axiom which is based on Kan simplicial sets (see
Kapulkin & Lumsdaine 2012, Other Internet Resources). The
simplicial model of constructive type theory with univalence developed
in the above article is carried out within an extension of ZFC with
inaccessible cardinals. This prompted the question whether one could
give a more constructive model of this type theory, and, in
particular, whether the type theory is predicative. Bezem, Coquand and
Huber (2014) have recently proposed a model of this type theory in
cubical sets which is computational and "can be expressed in a
constructive metalogic". Rathjen (2017) has verified that this new
model can be codified in a suitable extension of CZF by inaccessible
sets which is much weaker than classical set theory with inaccessible
cardinals. In fact, it turns out that if we take as starting point a
relatively weak type theory, i.e. one without W-types, and extend it
by the Univalence Axiom, the resulting theory has proof theoretic
strength \(\Gamma\_0\), the ordinal usually taken to represent the
limit of predicativity given the natural numbers (Rathjen 2017). To
show this, one proves that the cubical model by Bezem, Coquand and
Huber can be carried out in an extension of the system introduced in
Crosilla and Rathjen (2001) by (bounded) Relativized Dependent
Choice. It follows from (Crosilla and Rathjen 2001) and (Rathjen 2003)
that the latter has proof theoretic ordinal \(\Gamma\_0\). 


### 5.3 Metamathematical properties of constructive and intuitionistic ZF and semantic techniques




A variety of interpretations for
intuitionistic logic have been
extended to intuitionistic and constructive set theories, such as
realisability, Kripke models and Heyting-valued semantics. All these
techniques have been applied to obtain metamathematical results about
the set theories.


#### 5.3.1 Disjunction and existence properties of constructive and intuitionistic ZF




Some intuitionistic set theories satisfy certain
"hallmark" metamathematical properties, such as
the *disjunction* and the *existence properties*. They
can also be shown to be consistent with the addition of principles
which go beyond what we most typically consider constructive. Among
these are, for example, *Church Thesis* and *Markov's
principle*. For a description of these principles in the context
of intuitionistic logic, the reader may wish to consult sections 4.2
and 5.2 of the entry on
intuitionistic logic or
Troelstra and van Dalen's book *Constructivism in Mathematics*
(Troelstra and van Dalen 1988).




Here we recall the disjunction and existence properties, formulated for
a set theory \(T\). The informal motivation for the disjunction and 
the existence properties is based on our understanding of
the constructive proofs of disjunctive and existential statements (respectively). 
In fact, it seems reasonable to expect that if we constructively prove 
a disjunction \(\phi \vee \psi\), 
then we should also be able to prove \(\phi\) or prove \(\psi\). 
Similarly, if we prove an existential statement, then we should be 
able to prove that a witness to that statement is definable within our theory.


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. 




Let \(T\) be a theory whose language, \(L(T)\), encompasses the
language of set theory. Moreover, for simplicity, we shall assume that
\(L(T)\) has a constant \(\omega\) denoting the set of von Neumann
natural numbers and for each \(n\) a constant \(c\_n\) denoting the
\(n\)-th element of \(\omega\).




A theory \(T\) has the ***disjunction property***
(DP) if whenever \(T\) proves \((\phi \vee \psi)\) for sentences
\(\phi\) and \(\psi\) of \(L(T)\), then \(T\) proves \(\phi\) or
\(T\) proves \(\psi\).




The ***existence property*** has two distinct
versions in the context of set theory: the ***numerical
existence property*** (NEP) and the ***existence
property*** (EP). Let \(\theta(x)\) be a formula with
at most \(x\) free. We say that:



> (1) \(T\) has the NEP if whenever \(T\) proves
> \(\exists x \in \omega \theta(x)\), then, for some natural
> number \(n, T\) proves \(\theta(c\_n)\).
> 
> 
> 
> (2) \(T\) has the EP if whenever \(T\) proves
> \(\exists x\theta\)(x), then there is a formula \(\phi(x)\)
> with exactly \(x\) free, so that \(T\) proves
> \(\exists !x(\phi(x) \wedge \theta(x))\).
> 
> 
> 




As realisability techniques have proved crucial in investigations on
the existence and disjunction properties for constructive and
intuitionistic set theories, we discuss the outcomes of these studies
in the next section.


#### 5.3.2 Realisability




Realisability has been one of the first and principal tools in the
research surrounding set theories based on intuitionistic logic,
starting from the early contributions by Friedman and Myhill (Friedman
1973, Myhill 1973). Realisability semantics for intuitionistic
arithmetic were first proposed by Kleene (Kleene 1945) and extended to
higher order Heyting arithmetic by Kreisel and Troelstra (Kreisel and
Troelstra 1970). For the definition of realisability for arithmetic
see section 5.2 of the entry
on intuitionistic logic. A
realisability similar to Kreisel and Troelstra was applied to systems
of higher order arithmetic by Friedman (Friedman 1973). Myhill
introduced a variant of this realisability which resembles Kleene's
slash (Myhill 1973; Kleene 1962, 1963). He thus proved that a version
of IZF with replacement in place of collection (called
IZF\(\_{Rep})\) has the DP, the NEP and the EP. These results were
further extended in (Myhill 1975; Friedman and Scedrov 1983). While
Friedman and Myhill gave realisability models for extensional set
theories, Beeson developed a notion of realisability for
non-extensional set theories. He then studied metatheoretical
properties of the extensional set theories via an interpretation in
their non-extensional counterparts. He thus proved that IZF (with
collection) has the DP and NEP (Beeson 1985). Subsequently McCarty
introduced realisability for IZF directly for extensional set theory
(McCarty 1984; 1986). Realisability semantics for variants of CZF have
been considered, for example, in (Crosilla and Rathjen 2001; Rathjen
2006a). The realisability in the latter article is inspired by
McCarty's and has the important feature that, as McCarty's for IZF, it
is a self-validating semantics for CZF (that is, this notion of
realisability can be formalised in CZF and each theorem of CZF is
realised provably in CZF). Rathjen has made use of this notion of
realisability to show that CZF (and a number of extensions of it) have
the DP and the NEP (Rathjen 2005b).



Another kind of realisability that has proved very useful is Lifschitz
realisability. Lifschitz (1979) introduced a modification of Kleene's
realizability for Heyting arithmetic which has the peculiarity of
validating a weak form of Church's Thesis (CT) with a uniqueness
condition, but not CT itself. Lifschitz realisability was extended to
second order arithmetic by van Oosten (1990). It was subsequently
extended to full IZF by Cheng and Rathjen, who employed it to obtain a
number of independence results, as well as validating the so called
Lesser Limited Principle of Omniscience (LLPO) (for LLPO see the entry
on 
 constructive mathematics).


The question of which set theories satisfy the existence property turned out to be particularly difficult to solve. (Friedman and
Scedrov 1985) used Kripke models to show that IZF (that is, the system
with collection) does not have the EP, while as mentioned above, the
system IZF\(\_{Rep}\) (which has replacement in place of
collection) does have the EP. This prompted Beeson to pose the
question [Beeson 1985, IX]:



> Does any reasonable set theory with collection have the existence property?


A first answer to Beeson's question came with (Rathjen 2012), where
the author introduced the notion of *weak* existence property:
the focus here is finding a provably definable
*set* of witnesses for every existential theorem. He then
introduced a form of realizability based on general set recursive
functions, where a realizer for an existential statement provides a
*set* of witnesses for the existential quantifier, rather than
a single witness. Rathjen combined this notion of realizability with
truth to yield that a number of theories with collection do enjoy the
weak existence property (while IZF does not). Among them, in
particular, the theory CZF without subset collection plus Myhill's
exponentiation axiom, CZF\(\_{Exp}\). In fact, Rathjen claimed that
by combining these results with further work he had carried out, he
could show that CZF\(\_{Exp}\) (and a number of other theories) do
have the existence property. A striking observation is that these theories are formulated with collection; consequently the failure
of the existence property in the case of IZF can not be attributed
only to collection, but to the interplay between this scheme and
unrestricted separation.


As to the prominent question of whether
CZF itself has the existence property, this has been solved in the
negative by Swan (2014). There the author made use of three well
devised realisability models and embeddings between them, to show that
even the weak existence property fails for CZF. In so doing he also
showed that CZF's subset collection schema is the culprit. As clearly
highlighted in (Swan 2014) the fact that CZF does not have EP does not
indicate some weakness in CZF as a constructive theory. Even if Swan
proved essentially that CZF asserts the existence of mathematical
objects that it does not know how to construct, still CZF does have
natural interpretations in which these objects can be constructed,
like, for example, Aczel's interpretation into type theory (Aczel
1978).



For a survey of results in intuitionistic set theory see (Beeson 1985,
Chapter IX). For the corresponding developments in CZF, see (Rathjen
2005b, 2006, 2012) and (Swan 2014).


#### 5.3.3 Kripke models and Heyting-valued semantics




Kripke models for intuitionistic set theories have been used 
in (Friedman and Scedrov 1985) to show that IZF does not have the EP (and
combining this with the results in (Myhill 1973) we have that
IZF\(\_{Rep}\) does not prove IZF). Kripke models have more
recently been applied to clarify the relation between the constructive
substitutes of the power set axiom: Myhill's exponentiation axiom and
Aczel's subset collection schema. It is clear that the power set axiom
implies both of these principles, and that subset collection implies
exponentiation. On the other hand, each of the latter two principles 
does not imply power set, as the theory CZF with power set in place of subset 
collection is much stronger 
than CZF and CZF\(\_{Exp}\) (Rathjen 2012b). In fact, CZF and
CZF\(\_{Exp}\) have the same proof theoretic strength (Griffor and
Rathjen 1994); therefore to investigate the relation between 
subset collection and exponentiation in constructive set theory 
one needed to develop tools other then proof theoretic methods. 
Lubarsky (2005) used Kripke models to
show that Myhill's exponentiation axiom does not imply Aczel's
subset collection (on the basis of CZF minus subset collection plus
full separtion). In (Lubarsky and Rathjen 2007) the authors applied the
technique of Kripke models to show that also the consequences of the
theories CZF and CZF\(\_{Exp}\) are different. Aczel and Rathjen
(2001) had shown that the class of Dedekind real numbers forms a set in CZF, 
by using subset collection. Lubarsky and Rathjen (2007) showed that
CZF\(\_{Exp}\) does not suffice to prove the same statement. For
further applications of Kripke models to separating crucial constructive 
notions, see e.g. (Diener and Lubarsky 2013).


 

Heyting-valued semantics for intuitionistic set theories were obtained
by Grayson (Grayson 1979) as a counterpart for Boolean models for
classical set theory. They have been generalized especially via
categorical semantics (for an introduction see MacLane and Moerdijk 1992). 
Heyting-valued semantics 
have found application to independence
results in (Scedrov 1981; 1982). A constructive treatment has been
given in (Gambino 2006). See also (Lubarsky 2009). 
See also Ziegler (2012) for a generalization of realisability and Heyting models for constructive set theory. 


#### 5.3.4 Categorical models of constructive and intuitionistic set theory




Categorical models of constructive and intuitionistic set theories
have flourished over the years. 
The notions of topos and sheaf play an 
essential role here (see *e.g.* Fourman 1980 and Fourman and
Scott 1980). For an overview of the main concepts, see the entry on
 category theory and the references
provided there (see in particular the supplement
 Programmatic Reading Guide). 
For recent developments that relate more
specifically to constructive set theories, see *e.g.* (Simpson
2005) and (Awodey 2008), as well as the web page:
 algebraic set theory.


### 5.4 Variants of Constructive and Intuitionistic Set Theories: Set Theories with Urelements and Non-extensional Set Theories




Sometimes systems of intuitionistic and constructive set theory have
been presented with the natural numbers as a separate sort of
urelements, that is, primitive objects with no elements (Friedman 1977; 
Myhill 1975; Beeson 1985). Constructively, this is a
natural choice which is in agreement with ideas expressed, for example, by
Bishop (1967) (among others). In Bishop's monograph the natural
numbers are taken as a fundamental concept on which all the
other mathematical concepts are based. From a technical
point of view, if the natural numbers are taken as primitive and
distinct from their set-theoretic representations, the axiom of
infinity then takes the form: "there is a set of natural numbers
(as urelements)". A more general form of urelements in
constructive set theories have been considered in (Cantini and Crosilla
2008). Here a variant of constructive set theory is proposed which combines 
an intensional and partial notion of operation with CZF's extensional notion of set 
(see also Cantini and Crosilla 2010).




The axiom of extensionality is a common feature of all the systems
discussed so far. However, in a context in which the computational
content of a statement is considered to be crucial, an intensional
theory might be more appropriate. For example, constructive type theory and
explicit mathematics both encapsulate some form of
intensionality. Intuitionistic set theories without extensionality
have been considered in the literature (Friedman 1973a, Beeson 1985). 
Their motivation, however, has been not computational
but technical in nature, due to the difficulties that extensionality 
brings about when studying metamathematical properties of intuitionistic set 
theories.