# Set Theory: Constructive and Intuitionistic ZF

*First published Fri Feb 20, 2009*

Constructive and intuitionistic Zermelo-Fraenkel set theories are axiomatic theories of sets in the style of Zermelo-Fraenkel set theory (ZF) which are based on intuitionistic logic. They were introduced in the 1970's and constitute a foundation for mathematics based on intuitionistic logic (see the entry on constructive mathematics). They are formulated on the standard first order language of Zermelo-Fraenkel set theory and make no direct use of inherently constructive ideas. In working in constructive and intuitionistic ZF we can thus to some extent rely on our familiarity with ZF and its heuristics.

Notwithstanding the similarities with classical set theory, the
concepts of set defined by *constructive* and
*intuitionistic* set theories differ considerably from that of
the classical tradition; they also differ from each other. The
techniques utilised to work within them, as well as to obtain
metamathematical results about them, also diverge in some respects
from the classical tradition because of their commitment to
intuitionistic logic. In fact, as is common in intuitionistic
settings, a plethora of semantic and proof-theoretic methods are
available for the study of constructive and intuitionistic set
theories.

In the following we introduce the main features of intuitionistic and constructive set theories and explain how they differ. As the field has grown considerably in recent years, we can discuss only some of the known results and available techniques. We shall focus on constructive set theory as we should like to highlight important foundational issues that arise within it.

- 1. The Essence of Constructive and Intuitionistic Set Theory
- 2. Origins of Constructive and Intuitionistic Set Theories
- 3. The Axioms Systems CZF and IZF
- 4. Constructive Choice Principles
- 5. Proof Theory and Semantics of Constructive and Intuitionistic ZF
- 6. Variants of Constructive and Intuitionistic Set Theories: Set Theories with Urelements and Non-extensional Set Theories
- Bibliography
- Other Internet Resources
- Related Entries

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

Constructive and intuitionistic Zermelo-Fraenkel set theories are based on intuitionistic rather than classical logic. They arise as a foundation for 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, the entry on set theory.

Constructive and intuitionistic ZF are based on the same first-order language as classical ZF set theory, thus taking advantage of the simplicity of the set-theoretic language and of our familiarity with it. As with Bishop-style constructive mathematics, they 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 sets. 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 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. The next step is to choose a good stock of set-theoretic principles which faithfully represent the desired notion of constructive set. This task turns out to be far 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 principles which are equivalent from the point of view of a stronger logic. In the case of set theory, some of the ZF principles 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). One can even envisage new statements which are classically equivalent to the axiom but intuitionistically separate from it. In the case of versions of ZF based on intuitionistic logic, the principles of replacement, separation, powerset and foundation have attracted most attention. For the exact formulation of these principles see the supplementary document:

Axioms of CZF and IZF.

The following is a typical scenario. The classical proof of equivalence of two forms of a single set-theoretic principle requires, at some point, an instance of the excluded middle. Therefore, this proof of equivalence will not be valid when working within an intuitionistic context. Consequently, these two forms of one principle may result in two distinct principles, and choosing one rather than the other of them may influence the notion of set we thus define.

In the specific case of the axiom of foundation, however, the situation is more complex. We need extra care in choosing an appropriate statement for foundation because its standard formulation yields instances of the excluded middle (on the basis of minimal set-theoretic assumptions). Foundation is introduced to rule out sets which are members of themselves and thus ∈-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 can be shown to yield instances of excluded middle and thus 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 then is to replace foundation with the classically
equivalent schema of set induction, which does not have the same
“side effects” but has similar
consequences.^{[1]}

Unlike foundation, principles such as powerset and separation present no incompatibility with intuitionistic logic, but different formulations of them may affect the strength of the whole theory in different ways. These principles may in fact 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) and (Rathjen 2005)).

To conclude, 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 set-theoretic axioms. The next task is to choose one version of each classical principle which best characterises the desired notion of set. 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”. We can also say that it allows one to choose the notions and theory which best suit a given context. As one could expect, this freedom 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 mathematical notions and prompts us to develop new sophisticated tools.

### 1.2 Constructive versus intuitionistic set theory

Although there are many possible 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. In the second approach, we also introduce restrictions on the set-theoretic principles admitted, as far as the resulting system complies with 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 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 and Rathjen 2001). We can also say that in this second approach the foundational predisposition influences the practice to a higher degree.

In the following we shall make use of the convention 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. It should be noted, however, that this convention is often not in place in the literature. In fact, the adjective “constructive” has also been used to denote impredicative theories, and “intuitionistic” often refers 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).

### 1.3 Predicativity in constructive set theory

In this entry we shall not address the subject of predicativity in detail, for which the reader may wish to consult (Feferman 2005). Other references include, for example, the section on predicativism in the entry on philosophy of mathematics and the entry on paradoxes and contemporary logic. We need however to explain what we mean by predicativity in the present context.

Predicativism has its origins in the writings of Poincaré and
Russell, who responded to the paradoxes that were discovered in
Cantor's and Frege's set theories in the early 20th century. Weyl also
made fundamental contributions to the study of predicativism.
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. We recall here one of the
formulations of the VCP:

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

Poincaré, 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 Schütte (independently) following lines indicated by
Kreisel (Kreisel 1958, Feferman 1964 and Schütte 1965, 1965a).
Here proof theory has played a pivotal role. 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 Schütte's proof theoretic analysis of these theories has identified an ordinal (usually referred to as Γ_{0}) which is the least non-predicative ordinal according to this notion.
Then a formal system is considered as predicatively justifiable if it is proof-theoretically reducible to a system of ramified second order arthmetic indexed by an ordinal less then Γ_{0}. (See Feferman 2005 for a more accurate informal account of this notion of predicativity and for further references).

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 Schütte'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*. We shall reserve the term *predicative*
for generalised predicativity, and call *strictly predicative*
a theory conforming with Feferman and Schütte's
criteria.^{[2]}

#### 1.3.1 The universe of sets

The shift from classical to intuitionistic logic, as well as the requirement of predicativity, reflects a conflict between the classical and the constructive view of the universe of sets. This also relates to the time-honoured distinction between actual and potential infinity. According to one view often associated to classical set theory, our mathematical activity can be seen as a gradual disclosure of properties of the universe of sets, whose existence is independent of us. This tenet is bound up with the assumed validity of classical logic on that universe. Brouwer abandoned classical logic and embarked on an ambitious programme to renovate the whole mathematical landscape. He denounced that classical logic had wrongly been extrapolated from the mathematics of finite sets, had been made independent from mathematics, and illicitly applied to infinite totalities.

In a constructive context, where the rejection of classical logic
meets the requirement of predicativity, the universe is an open
concept, a universe “in fieri”. This coheres with the
constructive rejection of actual infinity (Dummett 2000, Fletcher 2007).
Intuitionism
stressed the dependency of mathematical objects on the thinking
subject. Following this line of thought, predicativity appears as a natural
and fundamental component of the constructive view.
If we *construct* mathematical objects, then
resorting to impredicative definitions would produce an undesirable
form of circularity. We can thus view the universe of constructive
sets as built up in stages by our own mathematical activity and
thus open-ended.

In set theories based on intuitionistic logic, predicativity is usually expressed by restricting the axioms of separation and powerset, as these appear to be the main sources of impredicativity (when the infinity axiom is assumed). We also notice that two related components of predicativity come into play in the restrictions on separation and powerset. On the one side there is an attempt to avoid the circularity implied by defining an object by reference to itself (Russell's VCP); on the other side there is our supposed inability to survey the whole universe of sets.

#### 1.3.2 Restrictions on Powerset

The powerset axiom allows us to form a *set* of all subsets
of a given set. A typical example of impredicative use of powerset is
given by the definition of a new set *Y* as the intersection of
all subsets of a given set, say *B*, which satisfy a certain
property. That is, one uses powerset in conjunction with separation to
form a set *Y* = ∩{*D* ∈ Pow(*B*) :
φ(*D*)}. A form of impredicativity may arise here if
*Y* itself satisfies the formula φ and is thus among the
sets which are needed to define it.

A fundamental objection to powerset has been raised by Myhill in (Myhill 1975). From a constructive point of view, powerset is seen as problematic because “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). Myhill also 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).

Myhill's crucial observation was that powerset 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 powerset 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, powerset and
exponentiation are not equivalent. Myhill justifies exponentiation
by noting that a function is a rule, a finite object which can actually
be given (contrary to infinite sets).
He also writes that the case of powerset is different from
that of exponentiation as:

even in the case of infinite setsAandBwe do have an idea of an arbitrary mapping fromAintoB. An arbitrary mapping fromZintoZis 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 axplanation of “arbitrarysubset”. (Myhill 1975, 354).

Myhill's exponentiation axiom (in fact, a strengthening of it in the case of CZF) is now part of all major systems of constructive set theory. A form of exponentiation can also be found in constructive type theory.

#### 1.3.3 Restrictions on 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 φ(*X*), separation allows us to construct a new set
informally represented as: {*X* ∈ *B* : φ(*X*)}. This
schema may lead to impredicativity in case the formula φ contains
unbounded quantifiers ranging over the whole universe of
sets. Unrestricted separation seems in this case to require our ability to
survey the whole universe of sets and check if a given property holds
of each set. Another way to look at the impredicativity of separation is to note that
in defining a new set we may need to refer to this very set, contradicting Russell's VCP. For example, if we define a set *C* by separation
as {*X*∈*B* : ∀*Y*
ψ(*X*,*Y*)}, then *C* is among
the *Y*'s that need to be checked for the property ψ.
The
impredicativity of the separation schema is dealt with by requiring
that quantifiers in the formula range only over previously constructed
sets. Syntactically, this means that all quantifiers in the formula
are bounded (that is, they occur only in contexts ∀*X*
(*X*∈*Y* → ...) and ∃*X*(*X*∈*Y* ∧ ...)).

Having introduced appropriate constraints to powerset 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, then (2) accurately choosing, among various classically equivalent principles, those which seem more appropriate to represent a certain mathematical practice. The resulting notion of set, however, might become obscure and the choice of the set-theoretic principles might appear 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-Löf type theory (Aczel 1978). The claim is then that a clear constructive meaning is thus assigned to CZF's notion of set by looking at its meaning in Martin-Löf type theory, whose constructiveness is presupposed.

## 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). One could thus say that the first appearance of systems of intuitionistic set theory is rather technical in nature. These first papers already clarify a key feature of intuitionistic set theory, mainly that it is amenable to non-classical semantic interpretations and enjoys properties which are typical of the constructive approach.

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 Gödel's system T (see also (Bishop 1970) for a similar attempt). Myhill came though to 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 concpet 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.

Myhill appears to have been the first to notice that the full strength of powerset is not needed for the actual development of the mathematics in Bishop's book. 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 has been 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). System B is there shown to be expressive enough to represent the constructive mathematical practice of Bishop 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 strict predicativity). 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). Aczel also gave an interpretation of CZF in Martin-Löf type theory with the aim of corroborating the constructive nature of the set theory. He also strengthened some principles (namely, collection and exponentiation) of Myhill's system on the ground that the stronger versions are practically useful and are validated by the interpretation in type theory.

It should be mentioned that 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-Löf 1975; 1984).
Constructive type theory is usually considered the
most satisfactory foundation for constructive mathematics Bishop-style.
Both formalisms can be seen as making more explicit the computational
content of constructive mathematics.

The aim of recovering the computational content of mathematics, lost
by the widespread application of classical logic to infinite domains,
drives Bishop and his followers. Constructive and intuitionistic set
theories share this objective, but they display their computational
content only indirectly through their semantic interpretations
(see *e.g.* (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 ∈ (membership) as an additional non-logical binary predicate symbol. Their set-theoretic axioms are as follows.

IZFCZF

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. For 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

One usually considers ZFC (the axiom system ZF plus the axiom of
choice) as a foundation for mathematics (see the entry on
set theory). The axiom of choice (AC)
has been often considered the most controversial principle of set
theory. In constructive contexts one witnesses a peculiar
phenomenon. The usual form of the axiom of choice is validated by
intensional theories of types such as Martin-Löf type theory,
where the Curry-Howard correspondence
holds.^{[3]} 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
constructive and intuitionistic ZF. (For the proof, see the
supplementary document
on Set-theoretic principles incompatible with intuitionistic logic.)

The incompatibility of AC with extensional set theories based on intuitionistic logic seems to have been first noticed by Diaconescu in the context of categorical models of intuitionistic set theory (Diaconescu 1975). Goodman and Myhill give an argument for set theories based on intuitionistic logic (Goodman and Myhill 1978). (The reader may also wish to see the discussion on choice principles in the entry on constructive mathematics.)

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), which are often
employed in the constructive mathematical practice. (For their exact
formulation see the supplementary document on
Axioms of CZF and IZF.)

Aczel also considered a choice principle called the *Presentation
Axiom* (Aczel 1978). This principle 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*. In other terms presentation states that for each set *A* we can
find another set *B* which is a base and such that each element
of *A* can be “represented” by an element of *B*. Intuitively, a base should represent the concept of a
“well presented set”, one for which membership of an
element in the set is witnessed by a proof. In this context, countable choice can be
seen as saying that the natural numbers form a base.

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

A final remark: although constructive and intuitionistic set theories
are compatible with the principles of choice just mentioned, the set
theories are usually defined without any choice principle. 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). We wish also to mention here
Richman's recent 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

When considering a certain mathematical practice (or a theory used to codify it) from a philosophical perspective, we should like 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 simplified look into some of these topics and suggest further reading.

### 5.1 Proof-theoretic strength

When moving from classical ZF to its intuitionistic variants, the
choice of the set-theoretic axioms can considerably affect the
proof-theoretic strength of the resulting theory. For the notion of
proof-theoretic strength and for recent surveys on proof theory see for
example (Rathjen 1999, 2006b). We here only note that investigations
on the proof-theoretic strength of a theory are rich and
informative. For example, a proof-theoretic analysis may contribute
to establish if a certain theory complies with a given
mathematical framework (*e.g.*, predicativity, finitism, etc.).
Further, 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. Proof-theoretic interpretations have also
been employed to compare constructive set theory with other
foundational systems for constructive mathematics, such as
constructive type theory and explicit mathematics (see *e.g.*
Tupailo 2003).

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. Their proof-theoretic
strength has been established by various tools, *e.g.*, an
extension to set theory of the double negation interpretation (Friedman 1973a)
and a series of proof-theoretic interpretations between
theories (Griffor and Rathjen 1994). Some of the systems analysed
are 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} (Buchholz, Feferman, Pohlers and Sieg 1981). The fact
that CZF has the same strength as ID_{1} confirms the
generalised predicativity of the set theory, while it shows that it
exceeds the limit of strict predicativity.

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. 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*. The
addition of large set axioms to intuitionistic ZF was first proposed
by Friedman and Scedrov (Friedman and Scedrov 1984). One of the aims
of this program is to shed light on the corresponding classical
notions; another is 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 in constructive type theory. The justification of
extensions by large sets is thus bound up with the question of the
limits of foundational systems for constructive mathematics
(*e.g.* Rathjen 2005). We also note that in the case of
inaccessible set axioms, their addition to a subsystem of CZF with no set induction
produces a theory of strength Γ_{0}, the ordinal singled
out by Feferman and Schütte as the limit of strict predicativity
(Crosilla and Rathjen 2001; see also section
1.3).
Thus by working in a
constructive, predicative context, traditionally strong set-theoretic
notions might become predicatively justifiable.

### 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 Metamathematical properties of constructive and intuitionistic ZF

Some intuitionistic set theories satisfy certain
“hallmark” metamathematical features, such as
the *disjunction* and the *existence properties*. They
can also be shown to be consistent with principles which go beyond our
usual perception of constructiveness. 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 *Constructivism in Mathematics*
(Troelstra and van Dalen 1988).

We here recall the disjunction and existence property, formulated for
a set theory *T*. In the following ω denotes the set of
von Neumann natural numbers (for simplicity we do not distinguish each
natural number *n* from the *n*-th element of
ω).

A theory *T* has the * disjunction
property* (DP) if whenever

*T*proves (φ ∨ ψ) for sentences φ and ψ of

*T*, then

*T*proves φ or

*T*proves ψ.

The * existence property* has two distinct
versions in the context of set theory: the

**(NEP) and the**

*numerical existence property**(EP). Let θ(*

**existence property***x*) be a formula with at most

*x*free. We say that:

(1)Thas the NEP if wheneverTproves ∃x ∈ ω θ(x), then, for some natural numbern,Tproves θ(n).(2)

Thas the EP if wheneverTproves ∃xθ(x), then there is a formula φ(x) with exactlyxfree, so thatTproves ∃!x(φ(x) ∧ θ(x)).

In the case of constructive and intuitionistic ZF, the study of the disjunction and existence properties has required advanced tools. For a survey on results in intuitionistic set theory see (Beeson 1985, Chapter IX). For the corresponding developments in CZF, see (Rathjen 2005b).

#### 5.3.2 Realisability

Realisability has been the main tool 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 also
section
5.2 of the entry on intuitionistic logic. The main task in
extending realisability to set theory is to give a good definition of
the atomic cases and to
appropriately specify the quantifier clauses. Different routes have
been taken. Concerning the quantifier clauses, the approach most
followed appears to be that by Kreisel and Troelstra, where the
realizing numbers “go through” the quantifiers (Beeson
1985; Rathjen 2005b). A realisability similar to Kreisel and Troelstra
was applied to intuitionistic set theory 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 (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 obtained metatheoretical results
for the extensional set theories via an interpretation in their
non-extensional counterparts. He thus proved that IZF (with
collection) has the DP and NEP (see 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 (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).

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

Kripke models for intuitionistic set theories (Friedman and Scedrov
1985) have been used to show that IZF does not have the EP (combining
this with the results in (Myhill 1973) shows that IZF_{Rep}
does not prove IZF). Kripke models have more recently been applied by
Lubarsky to show that Myhill's exponentiation does not imply Aczel's
subset collection (Lubarsky 2005).

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 found application to independence results (Scedrov 1981; 1982). A constructive treatment has been recently given (Gambino 2006).

#### 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. For the most recent developments that relate more
specifically to constructive set theories, see *e.g.* (Simpson
2005) and S. Awodey's page on
algebraic set theory.

## 6. 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. It is certainly in agreement with ideas expressed by Bishop (Bishop 1967) (among others). In Bishop's monograph the natural numbers are taken as a fundamental concept in terms of which all the other mathematical concepts should be expressed. 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 (Cantini and Crosilla 2008).

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 relevant, 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 has, however, been not computational
but technical in nature. Extensionality, in fact, sometimes complicates matters
for metatheoretical investigations of intuitionistic systems. To get around this difficulty, Friedman and Beeson
have interpreted set theory *with* extensionality in a theory
*without* it, and then carried out the work in the latter
(see Beeson 1985).

## Bibliography

- Aczel, P., 1978, “The Type Theoretic Interpretation of
Constructive Set Theory”, in
*Logic Colloquium ‘77*, A. MacIntyre, L. Pacholski, J. Paris (eds.), Amsterdam and New York: North-Holland, pp. 55–66. - –––, 1982, “The type theoretic
interpretation of constructive set theory: choice principles”, in
*The L.E.J. Brouwer Centenary Symposium*, A. S. Troelstra and D. van Dalen (eds.), Amsterdam and New York: North-Holland, pp. 1–40. - –––, 1986, “The type theoretic
interpretation of constructive set theory: inductive
definitions”, in
*Logic, Methodology, and Philosophy of Science VII*, R.B. Marcus, G.J. Dorn, and G.J.W. Dorn (eds.), Amsterdam and New York: North-Holland, pp. 17–49. - –––, 1988,
*Non-wellfounded Sets*(CSLI Lecture Notes 14), Stanford: CSLI. - Aczel, P., and Rathjen, M., 2001, “Notes on Constructive Set Theory”, Institut Mittag-Leffler, Preprint 40. [Available online]
- Aczel, P., and Gambino, N., 2002, “Collection principles in
dependent type theory”, in
*Types for Proofs and Programs*(Lecture Notes in Computer Science 2277), P. Callaghan, Z. Luo, J. McKinna, and R. Pollack (eds.), Berlin: Springer, 1–23. - Barwise, J., and Moss, L., 1996,
*Vicious Circles*(CSLI Lecture Notes 60), Stanford: CSLI. - Beeson, M., 1985,
*Foundations of Constructive Mathematics*, Berlin: Springer. - Bishop, E., 1967,
*Foundations of Constructive Analysis*, New York: McGraw-Hill. - –––, 1970, “Mathematics as a numerical
language”, in
*Intuitionism and Proof Theory*, A. Kino, J. Myhill, and R. E. Vesley (eds.), Amsterdam: North-Holland, pp. 53–71. - Bishop, E., and Bridges, D., 1985,
*Constructive Analysis*, Berlin and Heidelberg: Springer. - Bridges, D., and Richman, F., 1987,
*Varieties of Constructive Mathematics*, Cambridge: Cambridge University Press. - Buchholz, W., Feferman, S., Pohlers, W., and Sieg, W., 1981,
*Iterated Inductive Definitions and Subsystems of Analysis*, Berlin: Springer. - Cantini, A., and Crosilla, L., 2008, “Constructive set theory
with operations”, in A. Andretta, K. Kearnes, D. Zambella (eds.),
*Logic Colloquium 2004*(Lecture Notes in Logic 29), Cambridge: Cambridge University Press. - Crosilla, L., and Rathjen, M., “Inaccessible set axioms may
have little consistency strength”,
*Annals of Pure and Applied Logic*115: 33–70. - Diaconescu, R., 1975, “Axiom of choice and
complementation”,
*Proceedings of the American Mathematical Society*51: 176–178. - Dummett, M., 2000,
*Elements of Intuitionism*, second edition, (Oxford Logic Guides 39), New York: Oxford University Press. - Feferman, S., 1964, “Systems of predicative analysis”,
*Journal of Symbolic Logic*29: 1–30. - –––, 1975, “A language and axioms for
explicit mathematics”, in
*Algebra and Logic*(Lecture Notes in Mathematics 450), J. Crossley (ed.), Berlin: Springer, pp. 87–139. - –––, 2005, “Predicativity”, in
*Handbook of the Philosophy of Mathematics and Logic*, S. Shapiro (ed.), Oxford: Oxford University Press. - Fletcher, P., 2007, “Infinity”, in
*Handbook of the Philosophy of Logic*, D. Jacquette, (ed.), Amsterdam: Elsevier, pp. 523–585. - Fourman, M.P., 1980, “Sheaf models for set theory”,
*Journal of Pure Applied Algebra*, 19: 91–101. - Fourman, M.P., and Scott, D.S., 1980, “Sheaves and
logic”, in
*Applications of Sheaves*(Lecture Notes in Mathematics 753), M.P. Fourman, C.J. Mulvey and D.S. Scott (eds.), Berlin: Springer, pp. 302–401. - Friedman, H., 1973, “Some applications of Kleene's methods
for intuitionistic systems”, in
*Proceedings of the 1971 Cambridge Summer School in Mathematical Logic*(Lecture Notes in Mathematics 337), A.R.D. Mathias and H. Rogers (eds.), Berlin: Springer, pp. 113–170. - –––, 1973a, “The consistency of classical
set theory relative to a set theory with intuitionistic logic”,
*Journal of Symbolic Logic*38: 315–319. - –––, 1977, “Set-theoretical foundations for
constructive analysis”,
*Annals of Mathematics*105: 1–28. - Friedman, H., Scedrov, A., 1983, “Set existence property for
intuitionistic theories with dependent choice”,
*Annals of Pure and Applied Logic*25: 129–140. - –––, 1984, “Large sets in intuitionistic
set theory”,
*Annals of Pure and Applied Logic*27: 1–24. - –––, 1985, “The lack of definable witnesses
and provably recursive functions in intuitionistic set theory”,
*Advances in Mathematics*57: 1–13. - Gambino, N., 2006, “Heyting-valued interpretations for
constructive set theory”,
*Annals of Pure and Applied Logic*137: 164–188. - Goodman, N.D., and Myhill, J., 1972, “The formalization of
Bishop's constructive mathematics”, in
*Toposes, Algebraic Geometry and Logic*(Lecture Notes in Mathematics 274), F.W. Lawvere (ed.), Berlin: Springer, pp. 83–96. - Goodman, N.D., and Myhill, J., 1978, “Choice implies excluded
middle”,
*Zeitschrift für mathematische Logik und Grundlagen der Mathematik*24(5): 461. - Grayson, R.J., 1979, “Heyting-valued models for
intuitionistic set theory”, in
*Applications of Sheaves*(Lecture Notes in Mathematics 753), M.P. Fourman, C.J. Mulvey, and D.S. Scott (eds.), Berlin: Springer, pp. 402–414. - Griffor, E., and Rathjen, M., 1994, “The strength of some Martin-Löf type theories”,
*Archive Mathematical Logic*33: 347–385. - van Heijenoort, J., 1967,
*From Frege to Gödel. A Source Book in Mathematical Logic 1879–1931*, Cambridge: Harvard Univ. Press. - Kleene, S.C., 1945, “On the interpretation of intuitionistic
number theory”,
*Journal of Symbolic Logic*10: 109–124. - –––., 1962, “Disjunction and existence under
implication in elementary intuitionistic formalisms”,
*Journal of Symbolic Logic*27: 11–18. - –––., 1963, “An addendum”,
*Journal of Symbolic Logic*28: 154–156. - Kreisel, G., 1958, “Ordinal logics and the characterization
of informal concepts of proof”,
*Proceedings of the International Congress of Mathematicians*(14–21 August 1958), Paris: Gauthier-Villars, pp. 289–299. - Kreisel, G., and Troelstra, A., S., 1970, “Formal systems for
some branches of intuitionistic analysis”,
*Annals of Mathematical Logic*1: 229–387. - Lindström, I., 1989, “A construction of non-well-founded
sets within Martin-Löf type theory”,
*Journal of Symbolic Logic*, 54: 57–64. - Lipton, J., 1995, “Realizability, set theory and term
extraction”, in
*The Curry-Howard isomorphism*(Cahiers du Centre de Logique de l'Universite Catholique de Louvain 8), Louvain-la-Neuve: Academia, pp. 257–364. - Lorenzen, P., and Myhill, J., 1959, “Constructive definition
of certain analytic sets of numbers”,
*Journal of Symbolic Logic*24: 37–49. - Lubarsky, R., 2005, “Independence results around constructive
ZF”,
*Annals of Pure and Applied Logic*,: 209–225.*132* - Maietti, M.E., Sambin, G., 2005, “Toward a Minimalist
Foundation for Constructive Mathematics”, in
*From Sets and Types to Topology and Analysis: Towards Practicable Foundations for Constructive Mathematics*(Oxford Logic Guides 48), L. Crosilla, and P. Schuster (eds.), Oxford: Oxford University Press. - Martin-Löf, P., 1975, “An intuitionistic theory of
types: predicative part”, in H.E. Rose and J. Sheperdson (eds.),
*Logic Colloquium ‘73*, Amsterdam: North-Holland, pp. 73–118. - –––, 1984, “Intuitionistic Type Theory”, Naples: Bibliopolis.
- McCarty, D.C., 1984, “Realisability and Recursive
Mathematics”,
D.Phil. Dissertation,
*Philosophy*, Oxford University. - –––, 1986, “Realizability and recursive set
theory”,
*Annals of Pure and Applied Logic*32: 153–183. - Myhill, J., 1973, “Some properties of Intuitionistic
Zermelo-Fraenkel set theory”, in
*Proceedings of the 1971 Cambridge Summer School in Mathematical Logic*(Lecture Notes in Mathematics 337), A.R.D. Mathias, and H. Rogers(eds.), Berlin: Springer, pp. 206–231. - –––, 1975, “Constructive set theory”,
*Journal of Symbolic Logic*, 40: 347–382. - Powell, W., 1975, “Extending Gödel's negative interpretation to ZF”,
*Journal of Symbolic Logic*, 40: 221–229. - Rathjen, M., Griffor, E., and Palmgren, E., 1998,
“Inaccessibility in constructive set theory and type
theory”,
*Annals of Pure and Applied Logic*94: 181–200. - Rathjen, M., 1999, “The realm of ordinal analysis”, in
*Sets and Proofs*(London Mathematical Society Lecture Notes 258), Cambridge: Cambridge University Press, pp. 219–279. - –––, 2003, “The anti-foundation axiom in
constructive set theories”, in
*Games, logic, and constructive sets*(CSLI Lecture Notes 161), Stanford: CSLI, pp. 87–108. - –––, 2003a, “Realizing Mahlo set theory in
type theory”,
*Archive for Mathematical Logic*42: 89–101. - –––, 2004, “Predicativity, circularity, and
anti-foundation”, in
*One hundred years of Russell's paradox*(Logic and its Applications 6), G. Link (ed.), Berlin: de Gruyter, pp. 191–219. - –––, 2005, “Replacement versus Collection
and related topics in constructive Zermelo-Fraenkel Set Theory”,
*Annals of Pure and Applied Logic*136: 156–174. - –––, 2005a, “The constructive Hilbert
program and the limits of Martin-Löf type theory”,
*Synthese*147: 81–120. - –––, 2005b, “The disjunction and related
properties for constructive Zermelo-Fraenkel set theory”,
*Journal of Symbolic Logic*70(4): 1232–1254. - –––, 2006, “Choice principles in
constructive and classical set theories”,
*Logic Colloquium ‘02*(Lecture Notes in Logic 27), Z. Chatzidakis, P. Koepke, and W. Pohlers (eds.), Wellesley, Massachusetts: A.K. Peters, 299–326. - –––, 2006a, “Realizability for constructive
Zermelo-Fraenkel set theory”, in
*Logic Colloquium ‘03*(Lecture Notes in Logic 24), V. Stoltenberg-Hansen and J. Väänänen (eds.), Wellesley, Massachusets: A.K. Peters, pp. 282–314. - –––, 2006b, “Theories and ordinals in proof
theory”,
*Synthese*148(3): 719–743. - Richman, F., 2000, “The fundamental theorem of algebra: a
constructive development without choice”,
*Pacific Journal of Mathematics*196: 213–230. - –––, 2001, “Constructive mathematics
without choice”, in
*Reuniting the Antipodes: Constructive and Nonstandard Views of the Continuum*(Synthese Library 306), P. Schuster,*et al*. (eds.), Dordrecth: Kluwer, pp. 199–205. - Russell, B., 1908, “Mathematical logic as based on the theory
of types”,
*American Journal of Mathematics*30: 222–262. Reprinted in van Heijenoort (1967), 150–182. - Scedrov, A., 1981, “Consistency and independence results in
Intuitionistic set theory” in
*Constructive mathematics*(Lecture Notes in Mathematics 873), F. Richman (ed.), Berlin: Springer, pp. 54–86. - –––, 1982, “Independence of the fan theorem
in the presence of continuity principles” in
*The L.E.J. Brouwer Centenary Symposium*, A.S. Troelstra, and D. van Dalen (eds.), Amsterdam: North-Holland, pp. 435–442. - –––, 1985, “Intuitionistic set
theory” in
*Harvey Friedman's research on the foundations of mathematics*, L.A. Garrubgtib*et al*. (eds.), Amsterdam: Elsevier. - Schütte, K., 1965, “Predicative well-orderings”,
in
*Formal Systems and Recursive Functions*, J. Crossley and M. Dummett (eds.), Amsterdam: North-Holland, pp. 279–302. - –––, 1965a, “Eine Grenze für die
Beweisbarkeit der Transfiniten Induktion in der verzweigten
Typenlogik”,
*Archiv für mathematische Logik und Grundlagenforschung*7: 45–60. - Simpson, A., 2005, “Constructive set theories and their
category-theoretic models”, in
*From Sets and Types to Topology and Analysis: Towards Practicable Foundations for Constructive Mathematics*(Oxford Logic Guides 48), L. Crosilla and P. Schuster (eds.), Oxford: Oxford University Press. - Troelstra, A.S., and van Dalen, D., 1988,
*Constructivism in Mathematics*(two volumes), Amsterdam: North Holland. - Tupailo, S., 2003, “Realization of constructive set theory
into Explicit Mathematics: a lower bound for impredicative Mahlo
universe”,
*Annals of Pure and Applied Logic*120: 165–196.

## Other Internet Resources

- Algebraic Set theory, by S. Awodey (Carnegie Mellon).

[Please contact the author with further suggestions.]

## Related Entries

Brouwer, Luitzen Egbertus Jan | category theory | logic, history of: intuitionistic logic | logic: intuitionistic | mathematics, philosophy of | mathematics, philosophy of: intuitionism | mathematics: constructive | paradoxes: and contemporary logic | proof theory | set theory | set theory: alternative axiomatic theories | set theory: early development | set theory: non-wellfounded | type theory: constructive

### Acknowledgments

I thank Andrea Cantini, Michael Rathjen and Peter Schuster for valuable comments on an earlier version of this entry. My thanks also to the referee for helpful suggestions and to the editors for their useful comments and their kind assistance with the html files.