Set Theory: Constructive and Intuitionistic ZF

First published Fri Feb 20, 2009; substantive revision Thu Feb 22, 2024

Constructive and intuitionistic Zermelo-Fraenkel set theories areaxiomatic theories of sets in the style ofZermelo-Fraenkel set theory (ZF) which are based onintuitionistic logic. They were introduced in the 1970’s and they represent a formalcontext within which to codify mathematics based on intuitionisticlogic (see the entry onconstructive mathematics). They are formulated on the standard first order language ofZermelo-Fraenkel set theory and make no direct use of inherentlyconstructive ideas. In working in constructive and intuitionistic ZFwe can thus to some extent rely on our familiarity with ZF and itsheuristics.

Notwithstanding the similarities with classical set theory, theconcepts of set defined byconstructive andintuitionistic set theories differ considerably from that ofthe classical tradition; they also differ from each other. Thetechniques utilised to work within them, as well as to obtainmetamathematical results about them, also diverge in some respectsfrom the classical tradition because of their commitment tointuitionistic logic. In fact, as is common in intuitionisticsettings, a plethora of semantic and proof-theoretic methods areavailable for the study of constructive and intuitionistic settheories.

This entry introduces the main features of constructive andintuitionistic set theories. As the field is expanding at a fast pace,we can only briefly recall some key aspects of results and availabletechniques. We focus more on constructive set theory to highlightimportant foundational issues that arise within it. Note that we omita conspicuous part of the literature on constructive andintuitionistic ZF which relates to their categorical interpretations.This area has seen major developments over the years, so much so thatan adequate treatment of that progress would require a substantialextension of this entry. The interested reader might wish to consultthe entry oncategory theory and its references (see also its supplementprogrammatic reading guide).

1. The Essence of Constructive and Intuitionistic Set Theory

Constructive and intuitionistic Zermelo-Fraenkel set theories arebased on intuitionistic rather than classical logic, and represent anatural environment within which to codify and study mathematics basedon intuitionistic logic. For constructive ZF, the main focus has beento represent the mathematical practice of Bishop (Bishop 1967, Bishopand Bridges 1985).

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

For classical set theory, see the entry onset theory.

Constructive and intuitionistic ZF are based on the same first-orderlanguage asclassical ZF set theory, which has only the binary predicate symbol \(\in\) (membership) asnon-logical symbol. That is, they are formulated on the basis ofintuitionistic first-order logic with equality, plus the binarypredicate symbol \(\in\). We can thus take advantage of the simplicityof the set-theoretic language and of our familiarity with it (Myhill1975). As with Bishop-style constructive mathematics, Constructive andintuitionistic ZF arecompatible with the classicaltradition, in the sense that all of their theorems areclassicallytrue. In fact, the two formal systems that we shall consider,Constructive Zermelo-Fraenkel (CZF) and IntuitionisticZermelo-Fraenkel (IZF), give rise to full classical ZF by the simpleaddition of the principle of the excluded middle.

1.1 Axiomatic freedom

Classical Zermelo-Fraenkel set theory is based on classicalfirst-order predicate logic with equality. On top of the logicalprinciples are axioms and schemata which describe the notion of setthe theory codifies. These principles can be classified into threekinds. First, there are principles that enable us to form new setsfrom given ones. For example, the axiom of pair allows us to form aset which is the pair of two given sets. Secondly, there areprinciples that establish properties of the set theoretic structure.For example, the axiom of extensionality identifies all sets havingthe same elements. Third, and finally, there are axioms asserting theexistence of specific sets. Thus the axiom of infinity states thatthere is an infinite set. These principles all together are usuallycalled the set-theoretic principles.

When introducing versions of ZF based on intuitionistic logic, thefirst step is to eliminate from the logic the principle of theexcluded middle (EM). The next step is to choose a good stock ofset-theoretic principles which faithfully represent the desired notionof constructive set. These tasks turn out to be more challenging thanone at first might have expected. In fact, as is well known, systemsbased on a “weaker” logic have the ability to distinguishbetween statements which are equivalent from the point of view of a“stronger” logic. In the case of set theory, some of theZF axioms or schemata are often presented by one of many classicallyequivalent formulations. Classically it is only a matter ofconvenience which one to use at a specific time. When working on thebasis of intuitionistic logic, however, various formulations of aclassical axiom may turn out to be distinct (non-equivalent). In fact,one can envisage new statements which are classically equivalent to aZF axiom but intuitionistically separate from it (for exampleCZF’s subset collection axiom (Aczel 1978)).

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

Set-theoretic principles incompatible with intuitionistic logic.

The typical move in formulating set theories based on intuitionisticlogic is then to replace foundation with the classically equivalentschema of set induction, which does not have the same “sideeffects” but has similar consequences.^[1]

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

Axioms of CZF and IZF.

Here the following is a typical scenario. Given what are classicallytwo variants of a single set-theoretic principle, their classicalproof of equivalence requires at some point an instance of theexcluded middle. However, in general this proof of equivalence willnot carry through to an intuitionistic context, and thus what areclassically two forms of one principle may result into two distinctprinciples when working intuitionistically. Choosing one rather thanthe other of them may therefore influence the notion of set we thusdefine. In the context ofconstructive set theories like CZF,power set and separation are replaced by intuitionistically weakerprinciples. One reason for this is that the full strength of power setand full separation are seen as unnecessary, since their weakersubstitutes 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 settheory (see the section onPredicativity in constructive set theory). The case of replacement versus collection is somehow more complex(see, for example, the articles (Friedman and Scedrov 1985), (Rathjen2005) and (Rathjen 2012)). It is worth stressing that while adoptingthe usual formulation of foundation goes against the very assumptionof intuitionistic logic as background logic, the principles ofseparation and power set have no incompatibility with intuitionisticlogic at all, so much so that they are integral part of theintuitionistic theory of sets IZF (Friedman 1973a).

To summarise, in formulating a set theory based on intuitionisticlogic, the first task is to expel the principle of excluded middle,including those instances of it which might be hidden in familiarformulations of set-theoretic axioms. The next task is to choose oneversion of each classical principle which best characterises thedesired notion of set. This opens up a range of choices one can make,as a plurality of intuitionistic principles may correspond to oneclassical principle. It should be stressed that from a constructivepoint of view this plurality of options (and thus systems), ratherthan causing uneasiness, is a highly desirable situation, as itconstitutes a form of “axiomatic freedom”. For example, itallows us to differentiate between a number of mathematical notions,thus better capturing our intuitions of them as distinct. It alsogives us the freedom to choose the notions and theories which bestsuit a given context. In addition, by adopting intuitionistic logic wecan include within our theories principles which are classically verystrong, without having to commit to their classical strength. Forexample, one can add a notion of inaccessible set to a weakconstructive set theory and obtain a predicative theory, while thesame notion embedded in a classical context becomes extremely strong(see the sections onPredicativity in constructive set theory andLarge sets in constructive and intuitionistic ZF). Finally, a rich area of (meta-theoretical) study of the relationsbetween the resulting distinct set-theoretic systems naturally arises.As one could expect, this freedom also has a price, as a highlytechnical study of the axiomatic theories might be necessary todistinguish their principles as well as to unveil some of theirsubtleties. This again can be seen as an advantage, since it forces usto a deeper and clearer analysis of the mathematical notions involvedand 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 tothe first one, we take all of what is available in classical ZF settheory and only modify those principles, such as foundation, whichhave a clear incompatibility with intuitionistic logic. This givesrise 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 onIZF.) The rationale behind these theories appears to be that ofgranting the mathematician the most powerful tools possible, as longas compatibility with intuitionistic logic is preserved. According tothe second approach, in addition to the adherence to intuitionisticlogic we also introduce restrictions on the set-theoretic principlesadmitted, as far as the resulting system complies with theconstructive mathematical practice. Theories of this second kind canthus be seen as the outcome of a double process of restriction withrespect to classical ZF. First there is a restriction tointuitionistic logic, then a restriction is imposed on theset-theoretic constructions allowed. The latter is motivated by (1)the observation that weaker principles appear to suffice for theconstructive mathematical practice and (2) the desire to adhere to aform of predicativity (see the next section for a clarification ofthis notion of predicativity). Paradigmatic examples of the latterkind of systems are Myhill’s Constructive Set Theory (Myhill1975), Friedman’s system B (Friedman 1977) and Aczel’sConstructive Zermelo-Fraenkel set theoryCZF (Aczel 1978; 1982; 1986, Aczel & Rathjen 2001; Aczel &Rathjen 2010, Other Internet Resources). We can also say that in thissecond approach the foundational motivation influences the practice toa higher degree.

In the following, we make use of a convention which is often in placetoday, 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 thisconvention is not always followed in the literature. In fact, theadjective “constructive” has also been used to denoteimpredicative theories, and “intuitionistic” to refer topredicative foundational theories such as Martin-Löf type theory(Martin-Löf 1975; 1984). It is also worth noting that the presentconvention on the use of the words “constructive” and“intuitionistic” differs from that made in the context ofconstructive mathematics (see, for example, the entry onconstructive mathematics and also Bridges and Richman 1987).

1.3 Predicativity in constructive set theory

Predicativism has its origins in the writings of Poincaré andRussell, who responded to the paradoxes that were discovered inCantor’s and Frege’s set theories in the early 20thcentury. Subsequently Weyl made fundamental contributions to the studyof predicative mathematics (Weyl 1918, see also Feferman 1988).According to one notion, a definition isimpredicative if itdefines an object by reference to a totality which includes the objectto be defined. With his Vicious Circle Principle (VCP), Russellintended to eliminate the circularity in mathematics that arises fromsuch impredicative definitions. Russell gave various formulations ofthe VCP, one of which is:

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

Poincaré, Russell and Weyl’s foundational analysis ofpredicativity has paved the way for a variety of logical analyses ofthe notion. The most commonly accepted analysis is due to Feferman andSchütte (independently) following lines indicated by Kreisel(Kreisel 1958, Feferman 1964 and Schütte 1965; 1965a). Here prooftheory has played a pivotal role. In very rough terms, the idea was tosingle out a collection of theories (a transfinite progression ofsystems of ramified second order arithmetic indexed by ordinals) bymeans of which to characterise a certain notion of predicativeordinal. Feferman and Schütte’s proof theoretic analysis ofthese theories has identified an ordinal, usually referred to as\(\Gamma_0\), which is the least non-predicative ordinal according tothis notion. A formal system is consideredpredicativelyjustifiable if it is proof-theoretically reducible to a system oframified second order arthmetic indexed by an ordinal less then\(\Gamma_0\). Therefore in proof theory \(\Gamma_0\) is usuallyconsidered as representing the limit of predicativity. (See Feferman2005 for a more accurate informal account of this notion ofpredicativity and for further references. See also Crosilla 2017. Thereader may also consult the section onpredicativism in the entry on philosophy of mathematics and the entry onparadoxes and contemporary logic).

Forconstructive foundational theories a more“liberal” approach to predicativism has been suggested,starting from work in the late 1950’s of Lorenzen, Myhill andWang (seee.g. Lorenzen and Myhill 1959). The driving idea isthat so-calledinductive definitions ought to be allowed inthe realm of constructive mathematics. The intuitive justification ofinductive definitions is related to the fact that they can beexpressed by means of finite rules, in a “bottom-up” way.The proof-theoretic strength of theories of inductive definitions goeswell beyond Feferman and Schütte’s bound (Buchholz,Feferman, Pohlers and Sieg 1981). Thus relatively strong theories areconsidered predicative in today’s foundations of constructivemathematics. This more liberal notion of predicativity has often beentermedgeneralised predicativity. (See Crosilla 2022 fordiscussion). In this entry we simply writepredicativity forgeneralised predicativity and callpredicativity given the naturalnumbers the better known form of predicativity which arises inthe classical context and was analysed by Kreisel, Feferman andSchütte.

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

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

1.3.1 Impredicativity of Separation

The schema of separation allows us to form a subset of a given setwhose elements satisfy a given property (expressed by a formula in thelanguage 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 informallyrepresented as: \(\{X \in B : \phi(X)\}\). Separation may lead toimpredicativity in case the formula \(\phi\) contains unboundedquantifiers ranging over the whole universe of sets; in fact, indefining 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 theproperty \(\psi\). This form of impredicativity is avoided inconstructive set theory by restricting the separation schema: byrequiring that all quantifiers occurring in the formula \(\phi\) rangeonly 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\) arebounded; 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 confirm that constraining separation in this way avoidsimpredicativity, by observing that the proof theoretic strength ofCZF, which has only restricted separation, is within the range ofpredicativity. However, by adding full separation to CZF one obtainsan impredicative theory, in fact, one with the same proof-theoreticstrength as full second order arithmetic (Lubarsky 2006). See alsoSection 5 for a discussion of the role of proof theory in analysingconstructive and intuitionistic set theories.

1.3.2 Impredicativity of Powerset

The power set axiom allows us to form aset of all subsets ofa given set. An example of impredicative use of power set is given bythe 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 circularityarises here as \(B\) itself is among the subsets of \(N\) which needto be checked for \(\phi\). As emphasized by Myhill (1975, 354), powerset is hard to justify from a constructive point of view: it gatherstogether all the subsets of a given set, but does not prescribe a rulethat "constructs" the set out of previously given sets, aspredicativity would seem to require.

Myhill writes:

Power set seems especially nonconstructive and impredicative comparedwith the other axioms: it does not involve, as the others do, puttingtogether or taking apart sets that one has already constructed butrather selecting out of the totality of all sets those that stand inthe 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 formthe set of all of them" (Myhill 1975, 354). As a consequence, thereseems to be no way of giving constructive sense to the set of allsubsets of an infinite set.

Myhill crucially observes that power set is not needed forconstructive mathematics Bishop-style, as it can be replaced by one ofits consequences. This is often called Myhill’sexponentiation axiom and states that we can form aset of all functions from one given set to another. Thisaxiom is clearly equivalent to power set in a classical context, wheresubsets of a given set may be represented by characteristic functions.In the absence of the principle of excluded middle, however, power setand exponentiation are not equivalent. Myhill’s fundamentalobservation is that exponentiation suffices to carry out themathematics of (Bishop 1967); for example, it allows for theconstruction of the (Cauchy) real numbers within constructive settheory. Myhill claims that exponentiation is constructively meaningfulbecause a function is a rule, a finite object which can actually begiven.

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

even in the case of infinite sets \(A\) and \(B\) we do have an ideaof an arbitrary mapping from \(A\) into \(B\). An arbitrary mappingfrom \(\mathbf{Z}\) into \(\mathbf{Z}\) is a partial recursivefunction together with a proof that the computation always terminates;a similar account can be given of an arbitrary real function. There isno corresponding explanation of “arbitrarysubset”. (Myhill 1975, 354).

Myhill’s exponentiation axiom is now part of all major systemsof constructive set theory. In the case of CZF, in fact, one has astrengthening of exponentiation, known as subset collection, which isalso a weakening of power set. A generalisation of exponentiation canalso be found in constructive type theory.

In the case of CZF, the claim that adding the power set axiom inducesimpredicativity can be substantiated by a technical result. Rathjen(2012b) shows that CZF augmented by the power set axiom exceeds thestrength of classical Zermelo set theory, and thus the addition of thepower set axiom to CZF brings us to a fully impredicative theory. Thisalso shows that the implication from power set to subset collectioncan not be reversed, as CZF’s proof-theoretic strength is waybelow that of Zermleo set-theory. In other terms, the power set axiomis 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 andintuitionistic set theories can be seen as modifications of classicalZF set theory that are obtained by: (1) replacing classical withintuitionistic logic, and (2) accurately choosing, among variousclassically equivalent principles, those which seem more appropriatefor given purposes. For example, we might choose principles whichsuffice to represent a certain mathematical practice, like, forexample, Bishop style mathematics. The resulting notion of set,however, might become obscure and the choice of the set-theoreticprinciples might appear to a certain degree as arbitrary. In the caseof intuitionistic ZF, one can justify the choice of the set-theoreticprinciples by examining its semantical interpretations, as Heytingsemantics, or by looking at its categorical models. In the case ofconstructive set theory, to hinder this kind of objection, Aczel hasgiven an interpretation of CZF in a version of Martin-Löf typetheory (Aczel 1978). The claim is that a clear constructive meaning isthus assigned to CZF’s notion of set by looking at its meaningin Martin-Löf type theory, since the latter is usually consideredas representing an accurate and fully motivated formulation of aconstructive notion of set. Aczel’s interpretation of CZF inconstructive type theory is given by interpeting sets astrees in type theory. That is, in constructive type theorythe universe of sets of CZF is represented by a type, V, of iterativesets built over the universe, U, of small types (Aczel 1978;Martin-Löf 1984). This interpretation clearly highlights the(generalised) predicativity of CZF, whose sets can be seen as treesbuilt up inductively, and whose set theoretic universe also has aclear inductive structure.

The predicativity of CZF and related systems is consonant withphilosophical positions which are often associated with the use ofintuitionistic logic. For example, it would seem that if weconstruct the mathematical objects, resorting toimpredicative definitions would produce an undesirable form ofcircularity (see, e.g., (Gödel 1944)). This clearly contrasts witha view often associated with classical set theory, for which ourmathematical activity can be seen as a gradual disclosure ofproperties of the universe of sets, whose existence is independentfrom us. Such a view is usually bound up with the use of classicallogic and impredicativity in studying the set-theoretic universe.Predicativity is also often seen as related to the time-honoureddistinction between actual and potential infinity. Predicative (andthus, in particular, constructive) theories are often seen as avoidingreference to actual infinity, and only committing to potentialinfinity (Dummett 2000, Fletcher 2007, Feferman 1964). This againseems particularly in harmony with those philosophical positions whichhighlight the human dimension of our mathematical activity, by seeing,for example, the mathematical objects and the truth of statementsabout them as dependent on us. Another related aspect is often seen aspertaining to predicativity: if the universe of sets is built up instages by our own mathematical activity, then it would be natural alsoto see it asopen ended. For this reason, in a constructivecontext, where the rejection of classical logic meets the requirementof predicativity, the universe of sets is often described as an openconcept, a universe “in fieri”. This idea is especiallywell exemplified within constructive type theory, where the notion oftype-theoretic universe has been deliberately left open by PerMartin-Löf (by not postulating specific elimination rules forit). The open ended nature of the universe of sets has paved the wayfor extensions of it by reflection principles. These have beeninvestigated both within type theory and constructive set theory. See(Rathjen 2005a) for a survey of results and a foundational discussion,and alsosection 5.2. For a formal analysis of the constructive universe of sets and acomparison with the Von Neumann hierarchy, see (Ziegler 2014).

2. Origins of Constructive and Intuitionistic Set Theories

Intuitionistic versions of Zermelo-Fraenkel set theories wereintroduced in the early 1970s by Friedman and Myhill. In (Friedman1973) the author presents a study of formal properties of variousintuitionistic systems and introduces for them an extension ofKleene’s realisability method. The realisability technique isapplied in (Myhill 1973) to show the existence property for a versionof intuitionistic Zermelo-Fraenkel set theory (with replacement inplace of collection). In another fundamental contribution Friedmanextends the double negation translation of intuitonistic logic torelate classical and intuitionistic set theories (Friedman 1973a).These first papers already address the relation between some majorintuitionistic set theories and classical ZF. They also clarify a keyfeature of set theory based on intuitionistic logic, mainly that it isamenable to powerful constructive semantic interpretations, likerealizability. These techniques are applied to the study of crucialmetatheoretical properties which are typical of the constructiveapproach and which are enjoyed by some constructive and intuitionisticset theories (see the section onSemantic techniques). This groundbreaking work has been fully exploited and substantiallyextended in work by, among others, Beeson, McCarty and Rathjen (see,e.g., Beeson 1985; McCarty 1984, Rathjen 2005, 2005b, 2006b, 2012).

Constructive set theory from the very start has a more distinctivefoundational vocation and it is bound up with Bishop’smathematics. In fact, in 1967 Bishop published the book“Foundations of constructive analysis” (Bishop 1967),which opened up a new era for mathematics based on intuitionisticlogic (see the entry onconstructive mathematics). The monograph stimulated fresh attempts in the logical community toclarify and formally represent the principles which were used byBishop, though only at an informal level. First attempts by Goodmanand Myhill (Goodman and Myhill 1972) made use of versions ofGödel’s system T (see also (Bishop 1970) for a similarattempt). Myhill, however, reached the conclusion that the resultingformalisation was too complex and artificial (Myhill 1975, 347).Myhill proposed instead a system which is closer to the informalnotion of set originally utilised by Bishop and also closer to theset-theoretic tradition. Myhill writes (1975, 347):

We refuse to believe that things have to be this complicated - theargumentation of (Bishop 1967) looks very smooth and seems to falldirectly from a certain concept of what sets, functions, etc. are, andwe wish to discover a formalism which isolates the principlesunderlying this conception in the same way that Zermelo-Fraenkel settheory isolates the principles underlying classical (nonconstructive)mathematics. We want these principles to be such as to make theprocess of formalization completely trivial, as it is in the classicalcase.

We observe here that Myhill’s constructive set theory haddistinguished notions of function, natural number and set; it thusclosely represented a constructive tradition in which functions andnatural numbers are conceptually independent from sets. Anotherfundamental step in the development of constructive set theory wasFriedman’s “Set-theoretical foundations for constructiveanalysis” (Friedman 1977). Here, among other systems, a systemcalled B is defined which has further restrictions on theset-theoretic principles compared with Myhill’s (in particular,it has no set induction). It also has a restricted form of the axiomof dependent choice. System B is there shown to be expressive enoughto represent the constructive analysis of Bishop (1967) whilst beingat the same time proof-theoretically very weak (due to the absence ofset induction). System B is in fact a conservative extension ofarithmetic (thus it is well below the limit of predicativity given thenatural numbers briefly recalled in section1.3). Myhill and Friedman’s systems were subsequently modified byAczel, to obtain a system, CZF (Constructive Zermelo-Fraenkel), thatis 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-Löf type theorywith the aim of corroborating the constructive nature of the settheory. He also strengthened some of the principles of Myhill’ssystem (namely, collection and exponentiation) on the ground that thestronger versions are still validated by the interpretation in typetheory.

Other foundational systems for Bishop-style constructive mathematicswere introduced in the early 1970’s. For example:explicitmathematics by S. Feferman (Feferman 1975), and the alreadymentionedIntuitionistic Type Theory (Martin-Löf 1975;1984). Constructive type theory is usually considered the mostsatisfactory foundation for constructive mathematics Bishop-style.Both type theory and explicit mathematics can be seen as expressingmore directly the computational content of constructive mathematics.Type theory, in particular, can be read as a very general andexpressive programming language. Constructive and intuitionistic settheories display their computational content only indirectly throughtheir semantic interpretations (seee.g. (Aczel 1977),(Lipton 1995) and the section onSemantic techniques).

3. The Axioms Systems CZF and IZF

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

Axioms of CZF and IZF.

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

\(\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 exponentiationaxiom, thus substituting for ZF’s Powerset.

4. Constructive Choice Principles

When discussing the role of classical set theory as a foundation formathematics, one usually considers the theory ZFC, that is, the axiomsystem ZF plus the axiom of choice (AC). One might therefore wonderwhat is the status of the axiom of choice in intuitionistic settings.The question is particularly significant because at its firstappearance the axiom of choice was often seen as controversial andhighly non-constructive. In constructive contexts, however, onewitnesses a peculiar phenomenon. The usual form of the axiom of choiceis validated by theories of types such as Martin-Löf type theory,where the Curry-Howard correspondence holds (See Section 3.4 of the entry onconstructive mathematics). On the other hand, the assumption of the axiom of choice gives riseto instances of the excluded middle inextensional contexts,where a form of separation is also available. This is the case, forexample, of constructive and intuitionistic ZF. (For the proof, seethe supplementary document onSet-theoretic Principles Incompatible with Intuitionistic Logic.) A proof of the incompatibility of AC with extensional set theoriesbased on intuitionistic logic seems to have first appeared in(Diaconescu 1975) in a categorical context. Goodman and Myhill give anargument for set theories based on intuitionistic logic (Goodman andMyhill 1978).

Although the axiom of choice is incompatible with both constructiveand intuitionistic ZF, other choice principles may be added to thebasic systems without producing the same undesirable results. Forexample one could add the principle ofcountable choice(AC\(_0)\) or that ofdependent choice (DC). In fact, bothhave been often employed in the constructive mathematical practice.(For their exact formulation see the supplementary document onAxioms of CZF and IZF.)

In (Aczel 1978) the author also considered a choice principle calledthePresentation Axiom, which asserts that every set is thesurjective image of a so-calledbase. A base is a set, say\(B\), such that every relation with domain \(B\) extends a functionwith domain \(B\).

The compatibility of all these forms of choice with constructive settheory has been proved by Aczel by extending his interpretation of CZFin Martin-Löf type theory (Aczel 1982). Rathjen (2006) has alsoconsidered various constructive choice principles and their mutualrelations.

A final remark: although constructive and intuitionistic set theoriesare compatible with the principles of choice just mentioned, the settheories are often defined without any choice principles. This has theaim of allowing for a “pluralistic” foundational approach.In particular, one would like to obtain a foundational theorycompatible with those contexts (e.g. categorical models ofset theory) in which even these weaker principles of choice may not bevalidated. For similar ideas in the context of constructive typetheory, see (Maietti and Sambin 2005, Maietti 2009). We wish also tomention here Richman’s appeal for a constructive mathematicswhich 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 tocodify it) from a philosophical perspective, we need to clarify withthe greatest possible precision the assumptions which are made withinit as well as the consequences which arise from those assumptions.This is particularly true when working with theories which are basedon a weaker logic than the classical one, for which a deeper, moreprecise insight is mandatory. Many technical tools are available whichcan help us clarify those aspects. Among the available instruments,there are proof-theoretic techniques, such as proof-theoreticinterpretations, as well as semantic techniques, such asrealisability, Kripke models, Heyting-valued semantics. In fact, inthe literature one often witnesses the interplay of proof-theoreticand semantic techniques. We here give a cursory look into some ofthese topics and suggest further reading.

5.1 Proof-theoretic strength

A fundamental theme in proof theory (in particular in the branch ofthis discipline known as ordinal analysis) is the classification oftheories by means of transfinite ordinals which measure their"consistency strength" and "computational power". These ordinals givean indication of how strong a theory is, and therefore offer a way ofcomparing 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 toas "the limit of predicativity" (seesection 1.3 above). This is indicative that there are predicatively acceptabletheories which are much stronger than Peano Arithmetic.

As discussed insection 1, the step from classical ZF to its intuitionistic variants requires usto choose a suitable formulation for each set-theoretic axiom: oneclassical axiom may have a number of intuitionistic variants whichturn out to be non-equivalent to each other. This is sometimesreflected 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 powerset, which are replaced by the predicatively acceptable principles ofbounded separation and subset collection, respectively. However, if weadd to CZF either of these principles, we obtain impredicativetheories. The impredicativity of the resulting theories is witnessedby the fact that their proof-theoretic strenght far exceeds that ofCZF.

It is not surprising that investigations on the proof-theoreticstrength of constructive and intutionistic set theories have been acrucial meta-theoretical tool for understanding these theories andtheir relations with each other. Investigations on the proof-theoreticstrength of a theory are rich and informative. In particular, Feferman(1993) has argued that a proof-theoretic analysis may help usestablish whether a certain theory complies with a given philosophicalframework: for example, the analysis may reveal that a theory ispredicative or finitistic etc. Furthermore, as a by-product of theproof-theoretic analysis we sometimes obtain simple independenceproofs. In fact, we can show that a theory cannot prove a specificprinciple because adding it to the theory would increase thetheory’s proof-theoretic strength. For example, CZF does notprove the powerset axiom, as the addition of powerset to CZF givesrise to a much stronger theory. Proof-theoretic interpretations havealso been employed to compare constructive and intuitionistic ZF settheories among each others, as well as with their classicalcounterparts, and also with other foundational systems forconstructive mathematics, such as constructive type theory andexplicit mathematics (see e.g., Griffor and Rathjen 1994, Tupailo2003). For a definition of the notion of proof-theoretic strength andfor surveys on proof theory see, for example, (Rathjen 1999, 2006b).

Although CZF and IZF are the most widely studied systems, numerousother systems for constructive and intuitionistic set theory have beenconsidered in the literature so far. The proof-theoretic strength of anumber of constructive and intuitionistic set theories has beenestablished by a variety of tools, like, for example, an extension toset theory of the double negation interpretation (originated in(Friedman 1973a)), and a variety of other proof-theoreticinterpretations, often resulting from a careful combination ofsemantic and proof theoretic techniques. In many cases the prooftheoretic strength of a system has been determined by a chain ofinterpretations between constructive and classical systems, and byusing 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 itsflexibility. As to the outcomes of these investigations, some of thesystems analysed turn out to be as weak as arithmetic, as, forexample, Friedman’s system B (Friedman 1977); other systems areas strong as full classical ZF, as IZF (Friedman 1973a). There arealso systems of intermediate strength, as CZF. The strength of thelatter theory, in fact, equals that of a theory of one inductivedefinition known as ID\(_1\). The fact that CZF has the same strengthas ID\(_1\) is taken to confirm the (generalised) predicativity of theset theory, and to prove that it exceeds the limit of predicativitygiven the natural numbers, since ID\(_1\)’s proof theoreticordinal is well above \(\Gamma_0\).

As a final remark: while the strength of CZF is well below that ofsecond-order arithmetic, the simple addition of excluded middle to CZFgives us (full) ZF. This should be contrasted with IZF, which alreadyhas the strength of ZF (Friedman 1973a). The limited proof theoreticstrength of CZF compared with IZF has often been considered one of themain advantages of constructive over intuitionistic set theory. In asense, it would seem that CZF makes the most of its use ofintuitionistic logic, as it characterises a notion of (generalised)predicative set which is sufficiently strong for the development ofmuch of constructive mathematics but also weak enough to avoidimpredicativity. Interestingly, when some large set axioms have beenadded to constructive set theory, a similar pattern has emerged, asthe strength of the resulting theory is well below that of thecorresponding classical theory.

5.2 Large sets in constructive and intuitionistic ZF

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

One can nonetheless study the impact oflarge set axioms overintuitionistic and constructive set theories. For example, one can addto constructive and intuitionistic set theories an axiom asserting theexistence of inaccessible sets, which classically correspond tostrongly inaccessible levels of the von Neumann hierarchy.^[2] The addition of large set axioms to intuitionistic ZF was firstproposed by Friedman and Scedrov (Friedman and Scedrov 1984). Theyintroduced inaccessible sets, Mahlo sets, and elementary embedding toexpress supercompactness, hugeness, and Reinhardt’s axiom over IZF.One of their aim was to shed light on the corresponding classicalnotions; another was to study the impact of these principles onmetatheoretical properties of the original set theories. Friedman andScedrov have shown, for example, that the addition of large set axiomsdoes not compromise the validity of the disjunction and numericalexistence properties for IZF.

In the context of constructive set theory, large sets have beenintroduced by Aczel in the form of so-calledregular sets toexpress inductive definitions of sets (Aczel 1986). Rathjen andcollaborators have determined the proof-theoretic strength of a numberof extensions of CZF by large set axioms, expressing largeness notions corresponding to inaccessibility, Mahloness and weak compactness (see, e.g., Rathjen et al. 1998; Rathjen 1998; Rathjen 1999, Rathjen 2003a). The study of large setsin the context of constructive set theories has been further expandedby Ziegler and Matthews in their Ph.D. theses (Ziegler 2014a, Matthews 2021). Ziegler 2014a is an investigation into large sets and large set axioms in the context of CZF. Amongother things, Ziegler uses a new modified cumulative hierarchy tocharacterise large sets’ arrangement in the set theoreticuniverse. He develops a constructive theory of clubs, presents acharacterisation theorem for Mahlo sets (connecting classical andconstructive approaches to Mahloness) and presents a characterisationtheorem for 2-strong sets. He then studies elementary embeddings ofthe set theoretic universe into a transitive class model of CZF.Matthews (2021) studies elementary embeddings in the context of bothclassical and intuitionistic theories without powerset. Jeon andMatthews ms. [Other Internet Resources] further this study byconsidering large set axioms on the basis of constructive settheories, including CZF. While the proof-theoretic strength of theextensions of CZF by small large sets is weaker than that ofSecond-order Peano Arithmetic, they show that the proof-theoreticstrength of large large sets (large set notions defined in terms ofelementary embeddings) vastly exceeds that of ZFC.

Another notion that has played a crucial role in classical set theory,also in relation with large cardinal assumptions, is that of theconstructible hierarchy, L. Lubarsky (1993) first studied theconstructible hierarchy in the context of IZF. Matthews and Rathjen(2024) further study the constructible hierarchy to clarify itsstructure and role within constructive set theories. For example, theyinvestigate whether L can be thought of as an inner model in the usualsense and show that the constructive case is importantly differentfrom the classical one. For example, they prove that it is possiblefor there to be an ordinal which is not in the constructibleuniverse.

From a foundational perspective, an objection could be raised toextensions of constructive set theory by large set axioms. Inclassical set theory, large cardinals can be seen as an incarnation ofhigher infinity. How do we justify these principles constructively? Itmay be thought that the constructive justification of these notionsshould rely again on the type theoretic interpretation. In the case ofset theories extended with so-called “small” large setprinciples, there are, in fact, corresponding extensions ofconstructive type theory by universes and so-called \(W\)-types. Fromthis perspective, the justification of extensions by large sets isthus bound up with the question of the limits of Martin-Löf typetheory (Rathjen 2005). We also note that the addition of inacessibleset axioms to a weak subsystem of CZF (with no set induction) producesa theory of strength \(\Gamma_0\), the ordinal singled out by Fefermanand Schütte as the limit of predicativity given the naturalnumbers (Crosilla and Rathjen 2001; see also section1.3). This is witness to the fact that by working in a constructive,predicative context, we can tame important traditionally strongset-theoretic notions. For stronger large set assumptions, otherjustifications would seem to be required. See, e.g., Ziegler 2014 fordiscussion.

Crosilla and Rathjen’s set theory with inaccessible sets (but noset induction) is proof theoretically rather weak, but mathematicallyquite expressive. For example, it has been used to verify that theaddition of Voevodsky’s Univalence Axiom to Martin-Löf typetheory does not engender impredicativity (Rathjen 2017). The axiom ofUnivalence was introduced by Voevodsky as part of his UnivalentFoundations programme (Voevodsky 2015). (For Univalent Foundations,see the entries ontype theory and onintuitionistic type theory). Voevodsky gave a model of constructive type theory with theUnivalence Axiom which is based on Kan simplicial sets (see Kapulkin& Lumsdaine 2012). The simplicial model of constructive typetheory with univalence developed in the above article is carried outwithin an extension of ZFC with inaccessible cardinals. This promptedthe question whether one could give a more constructive model of thistype theory, and, in particular, whether the type theory ispredicative. Bezem, Coquand and Huber (2014) have proposed a model ofthis type theory in cubical sets which is computational and “canbe expressed in a constructive metalogic”. Rathjen (2017) hasverified that this new model can be codified in a suitable extensionof CZF by inaccessible sets which is much weaker than classical settheory with inaccessible cardinals. In fact, it turns out that if wetake as starting point a relatively weak type theory, i.e., one withoutW-types, and extend it by the Univalence Axiom, the resulting theoryhas proof theoretic strength \(\Gamma_0\) (Rathjen 2017). To showthis, one proves that the cubical model by Bezem, Coquand and Hubercan be carried out in an extension of the system introduced inCrosilla and Rathjen (2001) by (bounded) Relativized Dependent Choice.It follows from (Crosilla and Rathjen 2001) and (Rathjen 2003) thatthe latter has proof theoretic ordinal \(\Gamma_0\).

5.3 Metamathematical properties of constructive and intuitionistic ZF and semantic techniques

A variety of interpretations forintuitionistic logic have been extended to intuitionistic and constructive set theories,such as realisability, Kripke models and Heyting-valued semantics. Allthese techniques have been applied to obtain metamathematical resultsabout 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 thedisjunction and theexistence properties. They canalso be shown to be consistent with the addition of principles whichgo beyond what we most typically consider constructive. Among theseare, for example,Church Thesis andMarkov’sprinciple. For a description of these principles in the contextof intuitionistic logic, the reader may wish to consult sections 4.2and 5.2 of the entry onintuitionistic logic or Troelstra and van Dalen’s bookConstructivism inMathematics (Troelstra and van Dalen 1988).

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

Although such properties seem quite natural and are fairly easy toestablish for arithmetical theories, they turn out to poseconsiderable technical challenges in the case of set theories, due totheir transfinite hierarchies of sets and the extensionality axiom. Infact, prominent constructive and intuitionistic set theories turn outnot to possess the existence property, as discussed in the nextsection.

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

A theory \(T\) has thedisjunction 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\).

Theexistence property has two distinctversions in the context of set theory: thenumericalexistence property (NEP) and theexistenceproperty (EP). Let \(\theta(x)\) be a formula with atmost \(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 onthe existence and disjunction properties for constructive andintuitionistic set theories, we discuss the outcomes of these studiesin the next section.

5.3.2 Realisability

Realisability has been one of the first and principal tools in theresearch surrounding set theories based on intuitionistic logic,starting from the early contributions by Friedman and Myhill (Friedman1973, Myhill 1973). Realisability semantics for intuitionisticarithmetic were first proposed by Kleene (Kleene 1945) and extended tohigher order Heyting arithmetic by Kreisel and Troelstra (Kreisel andTroelstra 1970). For the definition of realisability for arithmeticsee section 5.2 of the entry onintuitionistic logic. A realisability similar to Kreisel and Troelstra was applied tosystems of higher order arithmetic by Friedman (Friedman 1973). Myhillintroduced a variant of this realisability which resemblesKleene’s slash (Myhill 1973; Kleene 1962, 1963). He thus provedthat a version of IZF with replacement in place of collection (calledIZF\(_{Rep})\) has the DP, the NEP and the EP. These results werefurther extended in (Myhill 1975; Friedman and Scedrov 1983). WhileFriedman and Myhill gave realisability models for extensional settheories, Beeson developed a notion of realisability fornon-extensional set theories. He then studied metatheoreticalproperties of the extensional set theories via an interpretation intheir non-extensional counterparts. He thus proved that IZF (withcollection) has the DP and NEP (Beeson 1985). Subsequently McCartyintroduced realisability for IZF directly for extensional set theory(McCarty 1984; 1986). Realisability semantics for variants of CZF havebeen considered, for example, in (Crosilla and Rathjen 2001; Rathjen2006a). The realisability in the latter article is inspired byMcCarty’s and has the important feature that, as McCarty’sfor IZF, it is a self-validating semantics for CZF (that is, thisnotion of realisability can be formalised in CZF and each theorem ofCZF is realised provably in CZF). Rathjen has made use of this notionof 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 Lifschitzrealisability. Lifschitz (1979) introduced a modification ofKleene’s realizability for Heyting arithmetic which has thepeculiarity of validating a weak form of Church’s Thesis (CT)with a uniqueness condition, but not CT itself. Lifschitzrealisability 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 asvalidating the so called Lesser Limited Principle of Omniscience(LLPO) (for LLPO see the entry onconstructive mathematics).

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

Does any reasonable set theory with collection have the existenceproperty?

A first answer to Beeson’s question came with (Rathjen 2012),where the author introduced the notion ofweak existenceproperty: the focus here is finding a provably definablesetof witnesses for every existential theorem. He then introduced a formof realizability based on general set recursive functions, where arealizer for an existential statement provides aset ofwitnesses for the existential quantifier, rather than a singlewitness. Rathjen combined this notion of realizability with truth toyield that a number of theories with collection do enjoy the weakexistence property (while IZF does not). Among them, in particular,the theory CZF without subset collection plus Myhill’sexponentiation axiom, CZF\(_{Exp}\). In fact, Rathjen claimed that bycombining these results with further work he had carried out, he couldshow that CZF\(_{Exp}\) (and a number of other theories) do have theexistence property. A striking observation is that these theories areformulated with collection; consequently the failure of the existenceproperty in the case of IZF can not be attributed only to collection,but to the interplay between this scheme and unrestrictedseparation.

As to the prominent question of whether CZF itself has the existenceproperty, this has been solved in the negative by Swan (2014). Therethe author made use of three well devised realisability models andembeddings between them, to show that even the weak existence propertyfails for CZF. In so doing he also showed that CZF’s subsetcollection schema is the culprit. As clearly highlighted in (Swan2014) the fact that CZF does not have EP does not indicate someweakness in CZF as a constructive theory. Even if Swan provedessentially that CZF asserts the existence of mathematical objectsthat it does not know how to construct, still CZF does have naturalinterpretations in which these objects can be constructed, like, forexample, Aczel’s interpretation into type theory (Aczel1978).

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

5.3.3 Kripke models and Heyting-valued semantics

Kripke models for intuitionistic set theories have been used inFriedman and Scedrov 1985 to show that IZF does not have the EP (andcombining this with the results in Myhill 1973 we have thatIZF\(_{Rep}\) does not prove IZF). Kripke models have more recentlybeen applied to clarify the relation between the constructivesubstitutes of the power set axiom: Myhill’s exponentiationaxiom and Aczel’s subset collection schema. It is clear that thepower set axiom implies both of these principles, and that subsetcollection implies exponentiation. On the other hand, each of thelatter two principles does not imply power set, as the theory CZF withpower set in place of subset collection is much stronger than CZF andCZF\(_{Exp}\) (Rathjen 2012b). In fact, CZF and CZF\(_{Exp}\) have thesame proof theoretic strength (Griffor and Rathjen 1994); therefore toinvestigate the relation between subset collection and exponentiationin constructive set theory one needed to develop tools other thenproof theoretic methods. Lubarsky (2005) used Kripke models to showthat Myhill’s exponentiation axiom does not imply Aczel’ssubset collection (on the basis of CZF minus subset collection plusfull separtion). In Lubarsky and Rathjen 2007, the authors appliedthe technique of Kripke models to show that also the consequences ofthe theories CZF and CZF\(_{Exp}\) are different. Aczel and Rathjen(2001) had shown that the class of Dedekind real numbers forms a setin CZF, by using subset collection. Lubarsky and Rathjen (2007) showedthat CZF\(_{Exp}\) does not suffice to prove the same statement.

Kripke models have been applied also to separate varieties of the Fantheorem in Diener and Lubarsky 2013. Lubarsky (2023) presents anoverview of model-theoretic techniques, introducing bothHeyting-valued and Kripke models, and constructions that combine bothof those ideas. Kripke models for constructive set theory are employedin Iemhoff 2010, Iemhoff and Passmann 2021, and Iemhoff and Passmann2023. Iemhoff (2010) constructs Kripke models for subtheories ofconstructive set theory by using constructions from classical modeltheory such as constructible sets and generic extensions. She provesthat under the main construction all axioms except the collectionaxioms can be shown to hold in the constructed Kripke model. Iemhoffand Passmann (2021) investigate the logical structure of an importantsubsystem of CZF, intuitionistic Kripke-Platek set theory, IKP. Theyshow that the first-order logic of IKP is intuitionistic first-orderlogic.

Heyting-valued semantics for intuitionistic set theories were obtainedby Grayson (1979) as a counterpart for Boolean models forclassical set theory. They have been generalized especially viacategorical semantics (for an introduction see MacLane and Moerdijk1992). Heyting-valued semantics have found application to independenceresults in (Scedrov 1981; 1982). A constructive treatment has beengiven in Gambino 2006. (See also Lubarsky 2009.) See Ziegler 2012for a generalization of realisability and Heyting models forconstructive set theory.

5.3.4 Categorical models of constructive and intuitionistic set theory

Categorical models of constructive and intuitionistic set theorieshave flourished over the years. The notions of topos and sheaf play anessential role here (see, e.g., Fourman 1980 and Fourman andScott 1980). For an overview of the main concepts, see the entry oncategory theory and the references provided there (see in particular the supplementProgrammatic Reading Guide). For developments that relate more specifically to constructive settheories, seee.g. (Simpson 2005) and (Awodey 2008), as wellas 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 havebeen presented with the natural numbers as a separate sort ofurelements, that is, primitive objects with no elements (Friedman1977; Myhill 1975; Beeson 1985). Constructively, this is a naturalchoice which is in agreement with ideas expressed, for example, byBishop (1967), among others. In Bishop’s monograph the naturalnumbers are taken as a fundamental concept on which all the othermathematical concepts are based. From a technical point of view, ifthe natural numbers are taken as primitive and distinct from theirset-theoretic representations, the axiom of infinity then takes theform: “there is a set of natural numbers (as urelements)”.A more general form of urelements in constructive set theories havebeen considered in Cantini and Crosilla 2008. Here a variant ofconstructive set theory is proposed which combines an intensional andpartial 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 systemsdiscussed so far. However, in a context in which the computationalcontent of a statement is considered to be crucial, an intensionaltheory might be more appropriate. For example, constructive typetheory and explicit mathematics both encapsulate some form ofintensionality. Intuitionistic set theories without extensionalityhave been considered in the literature (Friedman 1973a, Beeson 1985).Their motivation, however, has been not computational but technical innature, due to the difficulties that extensionality brings about whenstudying metamathematical properties of intuitionistic set theories.

Bibliography

Aczel, P., 1978, “The Type Theoretic Interpretation ofConstructive Set Theory”, inLogic Colloquium‘77, A. MacIntyre, L. Pacholski, J. Paris (eds.), Amsterdamand New York: North-Holland, pp. 55–66.
–––, 1982, “The type theoreticinterpretation of constructive set theory: choice principles”,inThe L.E.J. Brouwer Centenary Symposium, A. S. Troelstraand D. van Dalen (eds.), Amsterdam and New York: North-Holland, pp.1–40.
–––, 1986, “The type theoreticinterpretation of constructive set theory: inductivedefinitions”, inLogic, Methodology, and Philosophy ofScience 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 (CSLILecture Notes 14), Stanford: CSLI.
Aczel, P., and M. Rathjen, 2001, “Notes on Constructive SetTheory”, Report No. 40, 2000/2001, Djursholm: InstitutMittag-Leffler, [available online]
Aczel, P., and N. Gambino, 2002, “Collection principles independent type theory”, inTypes for Proofs andPrograms (Lecture Notes in Computer Science 2277), P. Callaghan,Z. Luo, J. McKinna, and R. Pollack (eds.), Berlin: Springer, pp.1–23.
Awodey, S., 2008, “A Brief Introduction to Algebraic SetTheory”,The Bulletin of Symbolic, 14 (3):281–298.
Barwise, J., and L. Moss, 1996,Vicious Circles (CSLILecture Notes 60), Stanford: CSLI.
Beeson, M., 1985,Foundations of ConstructiveMathematics, Berlin: Springer.
Bezem, M., C. Thierry, and S. Huber, 2014, “A model of typetheory in cubical sets”, in 19th International Conference onTypes for Proofs and Programs (TYPES 2013), Matthes, R. and Schubert,A. (eds.), Dagstuhl: Schloss Dagstuhl–Leibniz-Zentrum fuerInformatik, pp. 107–128.
Bishop, E., 1967,Foundations of Constructive Analysis,New York: McGraw-Hill.
–––, 1970, “Mathematics as a numericallanguage”, inIntuitionism and Proof Theory, A. Kino,J. Myhill, and R. E. Vesley (eds.), Amsterdam: North-Holland, pp.53–71.
Bishop, E., and D. Bridges, 1985,Constructive Analysis,Berlin and Heidelberg: Springer.
Bridges, D., and F. Richman, 1987,Varieties of ConstructiveMathematics, Cambridge: Cambridge University Press.
Buchholz, W., S. Feferman, W. Pohlers, and W. Sieg, 1981,Iterated Inductive Definitions and Subsystems of Analysis,Berlin: Springer.
Cantini, A., and L. Crosilla, 2008, “Constructive settheory with operations”, in A. Andretta, K. Kearnes, D. Zambella(eds.),Logic Colloquium 2004 (Lecture Notes in Logic 29),Cambridge: Cambridge University Press, pp. 47–83.
–––, 2010, “Explicit operationalset theory”, in R. Schindler (ed.),Ways of ProofTheory, Frankfurt: Ontos, pp. 199–240.
Chen, R.-M. and M. Rathjen, 2012, “Lifschitz Realizabilityfor Intuitionistic Zermelo-Fraenkel Set Theory”,Archive forMathematical Logic, 51: 789–818.
Crosilla, L., 2017, “Predicativity and Feferman”, inG. Jäger and W. Sieg (eds.),Feferman on Foundations(Outstanding Contributions to Logic: Volume 13), Cham: Springer, pp.423–447.
–––, 2022, “Predicativity and ConstructiveMathematics”, in Oliveri, G., Ternullo, C. and Boscolo,S. (eds.),Objects, Structures, and Logics (Boston Studies in thePhilosophy and History of Science: Volume 339), Cham: Springer.
Crosilla, L., and M. Rathjen, 2001, “Inaccessible setaxioms may have little consistency strength”,Annals of Pureand Applied Logic, 115: 33–70.
Diaconescu, R., 1975, “Axiom of choice andcomplementation”,Proceedings of the American MathematicalSociety, 51: 176–178.
Diener, H., and R. Lubarsky, 2013, “Separating the FanTheorem and Its Weakenings”, in S. N. Artemov and A. Nerode(eds.),Proceedings of LFCS ‘13 (Lecture Notes inComputer Science 7734), Dordrecht: Springer, pp. 280–295.
Dummett, M., 2000,Elements of Intuitionism, secondedition, (Oxford Logic Guides 39), New York: Oxford UniversityPress.
Feferman, S., 1964, “Systems of predicative analysis”,Journal of Symbolic Logic, 29: 1–30.
–––, 1975, “A language and axioms forexplicit mathematics”, inAlgebra and Logic (LectureNotes in Mathematics 450), J. Crossley (ed.), Berlin: Springer, pp.87–139.
–––, 1988, “Weyl vindicated: Das Kontinuumseventy years later”, inTemi e prospettive della logica edella scienza contemporanee, C. Cellucci and G. Sambin (eds), pp.59–93.
–––, 1993, “What rests on what? Theproof-theoretic analysis of mathematics”, inPhilosophy ofMathematics, Part I, Proceedings of the 15th InternationalWittgenstein Symposium. Vienna: VerlagHölder-Pichler-Tempsky.
–––, 2005, “Predicativity”, inHandbook of the Philosophy of Mathematics and Logic, S.Shapiro (ed.), Oxford: Oxford University Press.
Fletcher, P., 2007, “Infinity”, inHandbook of thePhilosophy 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 D.S. Scott, 1980, “Sheaves andlogic”, inApplications of Sheaves (Lecture Notes inMathematics 753), M.P. Fourman, C.J. Mulvey and D.S. Scott (eds.),Berlin: Springer, pp. 302–401.
Friedman, H., 1973, “Some applications of Kleene’smethods for intuitionistic systems”, inProceedings of the1971 Cambridge Summer School in Mathematical Logic (Lecture Notesin Mathematics 337), A.R.D. Mathias and H. Rogers (eds.), Berlin:Springer, pp. 113–170.
–––, 1973a, “The consistency of classicalset theory relative to a set theory with intuitionistic logic”,Journal of Symbolic Logic, 38: 315–319.
–––, 1977, “Set-theoretical foundationsfor constructive analysis”,Annals of Mathematics, 105:1–28.
Friedman, H., and A. Scedrov, 1983, “Set existence property forintuitionistic theories with dependent choice”,Annals ofPure and Applied Logic, 25: 129–140.
–––, 1984, “Large sets in intuitionisticset theory”,Annals of Pure and Applied Logic, 27:1–24.
–––, 1985, “The lack of definablewitnesses and provably recursive functions in intuitionistic settheory”,Advances in Mathematics, 57: 1–13.
Gambino, N., 2006, “Heyting-valued interpretations forconstructive set theory”,Annals of Pure and AppliedLogic, 137: 164–188.
Gödel, 1944, “Russell’s mathematical logic”,The Philosophy of Bertrand Russell (Library of LivingPhilosophers), P. Schilpp (ed.), New York: Tudor, 1951,pp. 123–153.
Goodman, N.D., and J. Myhill, 1972, “The formalization ofBishop’s constructive mathematics”, inToposes,Algebraic Geometry and Logic (Lecture Notes in Mathematics 274),F.W. Lawvere (ed.), Berlin: Springer, pp. 83–96.
–––, 1978, “Choice implies excludedmiddle”,Zeitschrift für mathematische Logik undGrundlagen der Mathematik, 24(5): 461.
Grayson, R.J., 1979, “Heyting-valued models forintuitionistic set theory”, inApplications of Sheaves(Lecture Notes in Mathematics 753), M.P. Fourman, C.J. Mulvey, andD.S. Scott (eds.), Berlin: Springer, pp. 402–414.
Griffor, E., and M. Rathjen, 1994, “The strength of someMartin-Löf type theories”,Archive MathematicalLogic, 33: 347–385.
van Heijenoort, J., 1967,From Frege to Gödel. A SourceBook in Mathematical Logic 1879–1931, Cambridge: HarvardUniv. Press.
Ihemoff, R., 2010, “Kripke models for subtheories ofCZF”,Archive for Mathematical Logic, 49: 147–167.
Iemhoff, R., and R. Passmann, 2021, “Logics of intuitionisticKripke-Platek set theory”,Annals of Pure and AppliedLogic, 172: 103014.
–––, 2023, “Logics and admissible rules ofconstructive set theories”,Philosophical Transactions ofthe Royal Society A, 381 (2248). doi:10.1098/rsta.2022.0018
Kapulkin, C. and P.L. Lumsdaine, 2021, “The simplicialmodel of univalent foundations (after Voevodsky)”,Journalof the European Mathematical Society, 23(6): 2071–2126
Kleene, S.C., 1945, “On the interpretation of intuitionisticnumber theory”,Journal of Symbolic Logic, 10:109–124.
–––, 1962, “Disjunction and existenceunder 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 characterizationof informal concepts of proof”,Proceedings of theInternational Congress of Mathematicians (14–21 August1958), Paris: Gauthier-Villars, pp. 289–299.
Kreisel, G., and A. S. Troelstra, 1970, “Formal systemsfor some branches of intuitionistic analysis”,Annals ofMathematical Logic, 1: 229–387.
Lifschitz, V., 1979, “CT\(_0\) is stronger thanCT\(_0\)!”,Proceedings of the American MathematicalSociety, 73(1): 101–106.
Lindström, I., 1989, “A construction ofnon-well-founded sets within Martin-Löf type theory”,Journal of Symbolic Logic, 54: 57–64.
Lipton, J., 1995, “Realizability, set theory and termextraction”, inThe Curry-Howard isomorphism (Cahiersdu Centre de Logique de l’Universite Catholique de Louvain 8),Louvain-la-Neuve: Academia, pp. 257–364.
Lorenzen, P., and J. Myhill, 1959, “Constructive definitionof certain analytic sets of numbers”,Journal of SymbolicLogic, 24: 37–49.
Lubarsky, R., 1993, “Intuitionistic L”, inJ.N. Crossley, J.B. Remmel, R.A. Shore, and M.E. Sweedler(eds.),Logical Methods (Progress in Computer Science andApplied Logic: Volume 12), Birkhäuser, Boston, MA,555–571.
–––, 2005, “Independence results aroundconstructive ZF”,Annals of Pure and Applied Logic,132: 209–225.
–––, 2006, “CZF and second orderarithmetic”,Annals of Pure and Applied Logic,141: 29–34.
–––, 2009, “Topological Forcing Semanticswith Settling”, in S. N. Artemov and A. Nerode (eds.),Proceedings of LFCS ‘09 (Lecture Notes in ComputerScience 5407), Dordrecht: Springer, pp. 309–322.
–––, 2023, “Inner and Outer Models forConstructive Set Theories”, in D. Bridges, H. Ishihara,M. Rathjen, and H. Schwichtenberg (eds.),The Handbook ofConstructive Mathematics, Cambridge: Cambridge University Press,pp. 584–635.
Lubarsky, R., and M. Rathjen, 2007, “On the ConstructiveDedekind Reals”, in in S. N. Artemov and A. Nerode (eds.),Proceedings of LFCS 2007 (Lecture Notes in Computer Science4514), Dordrecht: Springer, pp. 349–362.
MacLane, S., and I. Moerdijk, 1992, “Sheaves in Geometryand Logic”, New York: Springer.
Maietti, M.E., 2009, “A minimalist two-level foundation forconstructive mathematics “,Annals of Pure and AppliedLogic, 160(3): 319–354.
Maietti, M.E., and G. Sambin, 2005, “Toward a MinimalistFoundation for Constructive Mathematics”, inFrom Sets andTypes to Topology and Analysis: Towards Practicable Foundations forConstructive Mathematics (Oxford Logic Guides 48), L. Crosilla,and P. Schuster (eds.), Oxford: Oxford University Press.
Martin-Löf, P., 1975, “An intuitionistic theory oftypes: predicative part”, in H.E. Rose and J. Sheperdson (eds.),Logic Colloquium ‘73, Amsterdam: North-Holland, pp.73–118.
–––, 1984, “Intuitionistic TypeTheory”, Naples: Bibliopolis.
Matthews, R. M. A., 2021, “Large Cardinals in WeakenedAxiomatic Theories”, Ph.D. Thesis, University of Leeds, [Matthews 2021 available online].
Matthews, R., and M. Rathjen, 2024, “Constructing theConstructible Universe Constructively”,Annals of Pureand Applied Logic, 175(3). doi:10.1016/j.apal.2023.103392
McCarty, D.C., 1984, “Realisability and RecursiveMathematics”, D.Phil. Dissertation,Philosophy, OxfordUniversity.
–––, 1986, “Realizability and recursiveset theory”,Annals of Pure and Applied Logic, 32:153–183.
Myhill, J., 1973, “Some properties of IntuitionisticZermelo-Fraenkel set theory”, inProceedings of the 1971Cambridge Summer School in Mathematical Logic (Lecture Notes inMathematics 337), A.R.D. Mathias, and H. Rogers(eds.), Berlin:Springer, pp. 206–231.
–––, 1975, “Constructive settheory”,Journal of Symbolic Logic, 40:347–382.
van Oosten, J., 1990, “Lifschitz’sRealizability”,The Journal of Symbolic Logic, 55:805–821.
Powell, W., 1975, “Extending Gödel’s negativeinterpretation to ZF”,Journal of Symbolic Logic, 40:221–229.
Rathjen, M., 1998, “The Higher Infinite in ProofTheory”, in J. Makowsky & E. Ravve (eds.),LogicColloquium ’95: Proceedings of the Annual European SummerMeeting of the Association of Symbolic Logic, in Haifa, Israel,August 1995, Cambridge: Cambridge University Press,pp. 275–304.
–––, 1999, “The realm of ordinalanalysis”, inSets and Proofs (London MathematicalSociety Lecture Notes 258), Cambridge: Cambridge University Press, pp.219–279.
–––, 2003, “The anti-foundation axiom inconstructive set theories”, inGames, logic, andconstructive sets (CSLI Lecture Notes 161), Stanford: CSLIPublication, pp. 87–108.
–––, 2003a, “Realizing Mahlo set theory intype theory”,Archive for Mathematical Logic, 42:89–101.
–––, 2004, “Predicativity, circularity,and anti-foundation”, inOne hundred years ofRussell’s paradox (Logic and its Applications 6), G. Link(ed.), Berlin: de Gruyter, pp. 191–219.
–––, 2005, “Replacement versus Collectionand related topics in constructive Zermelo-Fraenkel Set Theory”,Annals of Pure and Applied Logic, 136: 156–174.
–––, 2005a, “The constructive Hilbertprogram and the limits of Martin-Löf type theory”,Synthese, 147: 81–120.
–––, 2005b, “The disjunction and relatedproperties for constructive Zermelo-Fraenkel set theory”,Journal of Symbolic Logic, 70(4): 1232–1254.
–––, 2006, “Choice principles inconstructive 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 forconstructive Zermelo-Fraenkel set theory”, inLogicColloquium ‘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 inproof theory”,Synthese, 148(3): 719–743.
–––, 2008, “The natural numbers inconstructive set theory”,Mathematical Logic Quarterly,54: 287–312.
–––, 2012, “From the weak to the strongexistence property”,Annals of Pure and Applied Logic,163: 1400–1418.
–––, 2012b, “Constructive Zermelo-FraenkelSet Theory, Power Set, and the Calculus of Constructions”, in Epistemology versus Ontology: Essays on the Philosophy andFoundations of Mathematics in Honour of Per Martin-Löf,(Logic, Epistemology and the Unity of Science Series), P. Dybjer, S.Lindström, E. Palmgren and G. Sundhölm (eds.), New York andDordrecht: Springer Verlag.
–––, 2017, “Proof Theory of ConstructiveSystems: Inductive Types and Univalence”, in G. Jäger, andW. Sieg (eds.),Feferman on Foundations (OutstandingContributions to Logic: Volume 13), Cham: Springer, pp.385–419.
–––, 2023, “An Introduction toConstructive Set Theories: An Appetizer”, in D. Bridges,H. Ishihara, M. Rathjen, and H. Schwichtenberg (eds.),TheHandbook of Constructive Mathematics, Cambridge: CambridgeUniversity Press, pp. 20–60.
Rathjen, M., E. Griffor, and E. Palmgren, 1998,“Inaccessibility in constructive set theory and typetheory”,Annals of Pure and Applied Logic, 94:181–200.
Richman, F., 2000, “The fundamental theorem of algebra: aconstructive development without choice”,Pacific Journal ofMathematics, 196: 213–230.
–––, 2001, “Constructive mathematicswithout choice”, inReuniting the Antipodes: Constructiveand 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 thetheory of types”,American Journal of Mathematics, 30:222–262. Reprinted in van Heijenoort (1967), 150–182.
Scedrov, A., 1981, “Consistency and independence results inIntuitionistic set theory” inConstructive mathematics(Lecture Notes in Mathematics 873), F. Richman (ed.), Berlin:Springer, pp. 54–86.
–––, 1982, “Independence of the fantheorem in the presence of continuity principles” inTheL.E.J. Brouwer Centenary Symposium, A.S. Troelstra, and D. vanDalen (eds.), Amsterdam: North-Holland, pp. 435–442.
–––, 1985, “Intuitionistic settheory” inHarvey Friedman’s research on thefoundations of mathematics, L.A. Garrubgtibet al.(eds.), Amsterdam: Elsevier.
Schütte, K., 1965, “Predicative well-orderings”,inFormal Systems and Recursive Functions, J. Crossley and M.Dummett (eds.), Amsterdam: North-Holland, pp. 279–302.
–––, 1965a, “Eine Grenze für dieBeweisbarkeit der Transfiniten Induktion in der verzweigtenTypenlogik”,Archiv für mathematische Logik undGrundlagenforschung, 7: 45–60.
Simpson, A., 2005, “Constructive set theories and theircategory-theoretic models”, inFrom Sets and Types toTopology and Analysis: Towards Practicable Foundations forConstructive Mathematics (Oxford Logic Guides 48), L. Crosillaand P. Schuster (eds.), Oxford: Oxford University Press.
Swan, A.W., 2014, “CZF does not have the existenceproperty”,Annals of Pure and Applied Logic, 165:1115–1147.
Troelstra, A.S., and van Dalen, D., 1988,Constructivism inMathematics (two volumes), Amsterdam: North Holland.
Tupailo, S., 2003, “Realization of constructive set theoryinto Explicit Mathematics: a lower bound for impredicative Mahlouniverse”,Annals of Pure and Applied Logic, 120:165–196.
Voevodsky, V., 2015, “An experimental library of formalizedmathematics based on univalent foundations”,MathematicalStructures in Computer Science, 25: 1278–1294.
Weyl, H., 1918, “Das Kontinuum. Kritische Untersuchungenüber die Grundlagen der Analysis”, Veit, Leipzig.
Ziegler, Albert, 2012, “Generalizing realizability andHeyting models for constructive set theory”,Annals of Pureand Applied Logic, 163 (2): 175–184.
–––, 2014, “A cumulative hierarchy of setsfor constructive set theory”,Mathematical LogicQuarterly, 60 (1-2): 21–30.
–––, 2014a, “Large sets in constructiveset theory”, Ph.D. Thesis, University of Leeds, [available online]

Academic Tools

How to cite this entry.
Preview the PDF version of this entry at theFriends of the SEP Society.
Look up topics and thinkers related to this entry at the Internet Philosophy Ontology Project (InPhO).
Enhanced bibliography for this entryatPhilPapers, with links to its database.

Other Internet Resources

Awodey, S.,Algebraic Set theory, Carnegie Mellon.
Jeon, H., Matthews, R., m.s., “Very large set axioms over constructive set theories”, manuscript at arxiv.org.

[Please contact the author with further suggestions.]

Acknowledgments

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

Open access to the SEP is made possible by a world-wide funding initiative.
The Encyclopedia Now Needs Your Support
Please Read How You Can Help Keep the Encyclopedia Free

Browse

About

Support SEP

Mirror Sites

View this site from another server:

USA (Main Site)Philosophy, Stanford University

Info about mirror sites

Library of Congress Catalog Data: ISSN 1095-5054

Movatterモバイル変換