Constructive set theory

Constructive set theory is an approach to mathematical constructivism following the program of axiomatic set theory. The same first-order language with "$=$" and "$\in$" of classical set theory is usually used, so this is not to be confused with a constructive types approach. On the other hand, some constructive theories are indeed motivated by their interpretability in type theories.

Apart from rejecting the law of excluded middle, constructive set theories often require some logical quantifiers in their axioms to be bounded, motivated by results tied to impredicativity.

Introduction

Outlook

The logic of the theories discussed here is constructive in that it rejects ${\mathrm {LEM} }$, i.e. that the disjunction $\phi \lor \neg \phi$ automatically holds for all propositions. This requires rejection of strong choice principles and the rewording of some standard axioms. For example, the Axiom of Choice implies ${\mathrm {LEM} }$ for the formulas in ones adopted Separation schema, by Diaconescu's theorem. Similar results hold for the Axiom of Regularity in its standard form. In turn, constructive theories often do not permit classical proofs of properties that are e.g. provably computationally undecidable. Compared to the classical counterpart, one is also less likely to prove the existence of relations that cannot be realized. This then also affects the provability of statements about total orders such as that of all ordinal numbers, expressed by truth and negation of the terms in the order defining disjunction $(\alpha \in \beta )\lor (\alpha =\beta )\lor (\beta \in \alpha )$. And this in turn affects the proof theoretic strength defined in ordinal analysis. That said, theories without ${\mathrm {LEM} }$ tend to prove classically equivalent reformulations of classical theorems. For example, in Constructive analysis one cannot prove the intermediate value theorem in its textbook formulation, but one can prove theorems with algorithmic content that, as soon as ${\mathrm {LEM} }$ is assumed, are at once classically equivalent to the classical statement. The difference is that the constructive proofs are harder to find.

On models

Many theories studied in constructive set theory are mere restrictions, with respect to their axiom as well as their underlying logic, of Zermelo–Fraenkel set theory (${\mathsf {ZF}}$). Such theories can then also be interpreted in any model of ${\mathsf {ZF}}$. As far as constructive realizations go there is a realizability theory and Aczel's theory ${\mathsf {CZF}}$ has been interpreted in a Martin Löf type theories, as described below. In this way, set theory theorems provable in ${\mathsf {CZF}}$ and weaker theories are candidates for a computer realization. More recently, presheaf models for constructive set theories have been introduced. These are analogous to unpublished Presheaf models for intuitionistic set theory developed by Dana Scott in the 1980s.

Overview

The subject of constructive set theory begun by John Myhill's work on the ${\mathsf {CST}}$ set theory, a theory of several sorts and bounded quantification, aiming to provide a formal foundation for Errett Bishop's program of constructive mathematics. Below we list a sequence of theories in the same language as ${\mathsf {ZF}}$, leading up to Peter Aczel's well studied constructive Zermelo-Fraenkel, ${\mathsf {CZF}}$ and beyond. ${\mathsf {CZF}}$ is also characterized by the two features present also in Myhill's theory: On the one hand, it is using the Predicative Separation instead of the full, unbounded Separation schema. Boundedness can be handled as a syntactic property or, alternatively, the theories can be conservatively extended with a higher boundedness predicate and its axioms. Secondly, the impredicative Powerset axiom is discarded, generally in favor of related but weaker axioms. The strong form is very casually used in classical general topology. Constructive theories also come with stricter requirements for what sets constitutes a function. Adding ${\mathrm {LEM} }$ to a theory even weaker than ${\mathsf {CZF}}$ recovers ${\mathsf {ZF}}$, as detailed below. The system, which has come to be known as Intuitionistic Zermelo–Fraenkel set theory, ${\mathsf {IZF}}$, is a strong set theory without ${\mathrm {LEM} }$. It is similar to ${\mathsf {CZF}}$, but less conservative or predicative. The theory denoted ${\mathsf {IKP}}$ is the constructive version of ${\mathsf {KP}}$, the classical Kripke–Platek set theory where even the Axiom of Collection is bounded.

Subtheories of ZF

In this section we discuss common axiom candidates which make for frameworks in which all proofs are also proofs in ${\mathsf {ZF}}$.

Notation

Below we use the greek $\phi$ as a predicate variable in axiom schemas and use $P$ or $Q$ for particular predicates.

Quantifiers range over set and those are denoted by lower case letters. As is common in the study of set theory, one makes use set builder notation for classes, which, in most contexts, are not part of the object language but used for concise discussion. In particular, one may introduce notation declarations of the corresponding class via "$A=\{z\mid P(z)\}$", for the purpose of expressing $P(a)$ as $a\in A$. Logically equivalent predicates can be used to introduce the same class. One also writes $\{z\in B\mid P(z)\}$ as shorthand for $\{z\mid z\in B\land P(z)\}$.

As is common, we may abbreviate $\forall z.(z\in A\implies P(z))$ by $\forall (z\in A).P(z)$ and express the subclass claim $\forall (z\in A).z\in B$, i.e. $\forall z.(z\in A\implies z\in B)$, by $A\subset B$. For a property $P$, trivially $\forall z.{\big (}(z\in B\land P(z))\implies z\in B{\big )}$. And so follows that $\{z\in B\mid P(z)\}\subset B$.

Note that in a constructive interpretation, the elements of a subclass $A=\{z\in B\mid Q(z)\lor \neg Q(z)\}$ of $B$ may come equipped with more information than those of $B$. Also, as $Q$ may be not decidable for all elements in $B$, the two classes are a priori to be distinguished.

Common axioms

We start with ${\mathsf {ZF}}$ axioms that are virtually always deemed uncontroversial and part of all theories considered in this article.

Denote by $A\simeq B$ the statement expressing that two classes have exactly the same elements, i.e. $\forall z.(z\in A\iff z\in B)$, or equivalently $(A\subset B)\land (B\subset A)$.

The following axiom gives a means to prove equality "$=$" of two sets, so that through substitution, any predicate about $A$ translates to one of $B$.

Extensionality $\forall x.\forall y.\ \ x\simeq y\implies x=y$

By the logical properties of equality, the converse direction holds automatically.

Consider a property $P$ that provably holds for all elements of a set $y$, so that $\{z\in y\mid P(z)\}\simeq y$, and assume that the class on the left hand side is established to be a set. Note that, even if this set on the left informally also ties to proof-relevant information about the validity of $P$ for all the elements, the Extensionality axiom postulates that, in our set theory, the set on the left hand side is judged equal to the one on the right hand side.

Modern type theories may instead aim at defining the demanded equivalence "$\simeq$" in terms of functions, see e.g. type equivalence. The related concept of function extensionality is often not adopted in type theory. Other frameworks for constructive mathematics might instead demand a particular rule for equality or apartness come with each and every set.

Pairing $\forall x.\forall y.\ \ \exists p.\forall z.{\big (}(z=x\lor z=y)\implies z\in p{\big )}$

and

Union $\forall x.\ \ \exists u.\forall y.{\big (}(\exists z.y\in z\land z\in x)\implies y\in u{\big )}$

The two axioms may also be formulated stronger in terms of "$\iff$", e.g. in the context of ${\mathsf {BCST}}$ this is not necessary.

Together, these two axioms imply the existence of the binary union of two classes $a$ and $b$ when they have been established to be sets, and this is denoted $\bigcup \{a,b\}$ or $a\cup b$. Define class notation for finite elements via disjunctions (e.g. $c\in \{a,b\}$ says $(c=a)\lor (c=b)$) and define the successor set $Sx$ as $x\cup \{x\}$. A sort of blend between pairing and union, an axiom more readily related to the successor is the Axiom of adjunction. It is relevant for the standard modeling of individual Neumann ordinals. This axiom would also readily be accepted, but is not relevant in the context of stronger axioms below. Denote by $\langle x,y\rangle$ the standard ordered pair model $\{\{x\},\{x,y\}\}$.

The property that is false for any set corresponds to the empty class, denoted by $\{\}$ or $0$. That this is a set readily follows from other axioms, such as the Axiom of Infinity below. But if, e.g., one is explicitly interested in excluding infinite sets in ones study, one may at this point adopt the

Empty set $\exists x.\forall y.\,\neg (y\in x)$

BCST

In the following we will make use of axiom schemas, i.e. we postulate axioms for some collection of predicates. Note that some of the stated axiom schemas are often presented with set parameters $v$ as well, i.e. variants with extra universal closures $\forall v$ such that the $\phi$'s may depend on the parameters.

Basic constructive set theory ${\mathsf {BCST}}$ consists of several axioms also part of standard set theory, except the Separation axiom is weakened. Beyond the three axioms above, it adopts the

Axiom schema of predicative separation: For any bounded predicate $\phi$ with $y$ not free in it, $\forall y.\ \ \exists s.\forall x.{\Big (}x\in s\iff {\big (}x\in y\land \phi (x){\big )}{\Big )}$

also called Bounded Separation, i.e. the Separation for bounded quantifiers only. This amounts to postulating the existence of a set $s$ obtained by the intersection of any set $y$ and any predicatively described class $\{x\mid \phi (x)\}$. When the predicate is taken as $x\in z$ for $z$ proven to be a set, one obtains the binary intersection of sets and writes $s=y\cap z$. The restriction in the axiom is also gatekeeping impredicative definitions. For example, without the Axiom of power set, one should not expect a class $s$ defined as $\{x\in y\mid \forall (t\in {\mathcal {P}}y).Q(x,t)\}$ to be a set, where $Q$ denotes some 2-ary predicate. Note that if this subclass is provably a set, then the term $s$ thus defined is also in the scope of term variable $t$ used to define it.

While, in this way, predicative Separation leads to fewer given class definitions being sets, it must be emphasized that many class definitions that are classically equivalent are not so when restricting oneself to constructive logic. Thus, in this way, one gets a richer theory of sets constructively. Due to the potential undecidability of general predicates, the notion of subset is far more elaborate in constructive set theories than in classical ones, as we will see.

As noted, from Separation and the existence of any set (e.g. Infinity below) and the predicate that is false of any set will follow the existence of the empty set.

By virtue of the purely logical theorem $\forall x.{\big (}xRs\Leftrightarrow (xRy\land \neg xRx){\big )}\implies \neg sRy$, Russel's construction shows that Predicative Separation alone implies that $\{x\in y\mid x\notin x\}\notin y$. In particular, no universal set exists.

Next, we consider the

Axiom schema of Replacement: For any predicate $\phi$, $\forall d.\ \ \forall (x\in d).\exists !y.\phi (x,y)\implies \exists r.\forall y.{\big (}y\in r\iff \exists (x\in d).\phi (x,y){\big )}$

where $\exists !$ denotes unique existence. It is granting existence, as sets, of the range of function-like predicates, obtained via their domains.

With the Replacement schema, this theory proves that the equivalence classes or indexed sums are sets. In particular, the Cartesian product, holding all pairs of elements of two sets, is a set.

Replacement and the axiom of Set Induction (introduced below) suffices to axiomize hereditarily finite sets constructively and that theory is also studied without Infinity. For comparison, consider the very weak classical theory called General set theory that interprets the class of natural numbers and their arithmetic via just Extensionality, Adjunction and full Separation. Only when assuming ${\mathrm {LEM} }$ does Replacement already imply full Separation.

In ${\mathsf {ZF}}$, the Replacement is mostly important to prove the existence of sets of high rank, namely via instances of the axiom schema $\phi (x,y)$ where relates relatively small set $x$ to bigger ones, $y$.

Constructive set theories commonly have Axiom schema of Replacement, sometimes restricted to bounded formulas. However, when other axioms are dropped, this schema is actually often strengthened - not beyond ${\mathsf {ZF}}$, but instead merely to gain back some provability strength.

Within this conservative context of ${\mathsf {BCST}}$, the Bounded Separation schema is actually equivalent to Empty Set plus the existence of the binary intersection for any two sets. The latter variant of axiomatization does not make use of a schema.

Functions

Naturally, the logical meaning of existence claims is a topic of interest in intuitionistic logic. The proof calculus of a constructive theory of statements such as

$\forall (a\in A).\exists !(c\in C).P(a,c)$

might be set up in terms of programs on represented domains and possibly having to witness the claim (in the sense of, informally speaking, $\forall (a\in A).P(a,c_{a})$, where $c_{a}$ denotes the value of a program as mentioned, but this gets into questions of realizability theory). Now in the current discussion, we want to speak of a total functional relation $f\subset A\times C$ when provably

$\forall (a\in A).\exists !(c\in C).\langle a,c\rangle \in f$,

which notably involves an existential quantifier. Variants of the functional predicate definition using apartness relations on setoids have been defined as well.

Let $C^{A}$ (also written ${}^{A}C$) denote the class of such set functions. When functions are understood as just function graphs as above, the membership proposition $f\in C^{A}$ is also written $f\colon A\to C$.

Write $1$ for $S0$. Given any $A\subset B$, we are now led to reason about classes such as

$\{\langle x,y\rangle \in B\times \{0,1\}\mid (x\in A\land y=1)\lor (\neg (x\in A)\land y=0)\}.$

The boolean-valued characteristic functions $\chi _{A}\colon B\to \{0,1\}$ are among such classes, which may be taken to correspond to terminating functions. But be aware that $x\in A$ may not be decidable.

Using the standard class terminology, one can freely make use of functions, given their domain is a set. The functions as a whole will be sets if their codomain is.

ECST

Denote by $\mathrm {Ind} (A)$ the Inductive property, e.g. $0\in A\land \forall (n\in A).Sn\in A$. In terms of a predicate $P$ underling the class, this would be translated as $P(0)\land \forall n.{\big (}P(n)\implies P(Sn){\big )}$. Note that $n$ denotes a generic set variable here. Write $\bigcap A$ for $\{x\mid \forall y.(y\in A\implies x\in y)\}$. Define a class $\omega =\bigcap \{x\mid \mathrm {Ind} (x)\}$.

For some fixed predicate $P$, the statement $P(a)\land \forall x.P(x)\implies a\subset x$ expresses that $a$ is the smallest set among all sets $x$ for which $P(x)$ holds true. The elementary constructive Set Theory ${\mathsf {ECST}}$ has the axiom of ${\mathsf {BCST}}$ as well as

Strong Infinity $\exists w.{\Big (}\mathrm {Ind} (w)\,\land \,{\big (}\forall x.\mathrm {Ind} (x)\implies w\subset x{\big )}{\Big )}$

The second universally quantified conjunct expresses mathematical induction for all $x$ in the universe of discourse, i.e. for sets. In this way, the principles discussed in this section give means of proving that some predicates hold at least for all elements of $\omega$. Be aware that even the relatively strong axiom of full mathematical induction (induction for any predicate, discussed below) may also be adopted and used without ever postulating that $\omega$ forms a set.

Weak forms of axioms of infinity can be formulated, all postulating that some set with the common natural number properties exist. Then full Separation may be used to obtain the "sparse" such set, the set of natural numbers. In the context of otherwise weaker axiom systems, an axiom of infinity should be strengthened so as to imply existence of such a sparse set on its own. One weaker form of Infinity reads

$\exists w.\forall m.{\Big (}m\in w\iff {\big (}m=0\lor (\exists n\in w).\forall k.(k\in m\iff k\in n\lor k=n){\big )}{\Big )}$

which can also be written more concisely using $S$. The set thus postulated to exist is generally denoted by $\omega$, the smallest infinite von Neumann ordinal. For elements $n,m$ of this set, the claim $n=m$ is decidable.

With this, ${\mathsf {ECST}}$ proves induction for all predicates given by bounded formulas. The two of the five Peano axioms regarding $0$ and one regarding closedness of $S$ with respect to $\omega$ follow fairly directly from the axioms of infinity. Finally, $S$ can be proven to be an injective operation.

Choice

To be finite means there is a bijective function to a natural. To be subfinite means to be a subset of a finite set. The claim that being a finite set is equivalent to being subfinite is equivalent to ${\mathrm {LEM} }$.

If $g\colon \omega \to z$, we can form the one-to-many relation-set $\{\langle n,u\rangle \mid n\in \omega \land u\in g(n)\}$. The Axiom of countable choice would grant that whenever $\forall (n\in \omega ).\exists u.u\in g(n)$, we can form a function mapping each number to a unique value. Countable choice is implied by the more general Axiom of dependent choice. This is in turn implied by the Axiom of choice concerning functions on general domains.

We conclude by a remark to highlight the strength of choice and its relation to matters of Intentionality. Consider the subfinite sets

$x=\{u\in \{0,1\}\mid u=0\lor (u=1\land P)\}$

$y=\{u\in \{0,1\}\mid u=1\lor (u=0\land P)\}$

Nevertheless, here the full Axiom of Choice, granting existence of a map $f\colon \{x,y\}\to \{0,1\}$ into distinguishable elements (equality on the codomain is decidable), implies that $P\lor \neg P$. So the existence claim of general choice functions with $f(z)\in z$ is non-constructive. To better understand this phenomenon, take note of implications such as $P\implies x=y$. In this way, the Axiom of Separation ties predicates to set equality, and in turn to information about functions. The difference between the discrete codomain of natural numbers and the domain $\{x,y\}$ lies in the fact that a priori little is known about the latter. We have $0\in x$ and $1\in y$, regardless of $P$. But in the case of $x=y$, there is extensionally only one possible function input to a choice choice function $f$, so when considering the functional assignment $f(x)=0$, then unconditionally declaring $f(y)=1$ would not be consistent.

Arithmetic

In ${\mathsf {ECST}}$, many statement can be proven per individual set (as opposed to expressions involving a universal quantifier, as e.g. available with an induction axiom) and objects of mathematical interest can be made use of at the class level on an individual bases. As such, the axioms listed so far suffice as a working theory for a good portion of basic mathematics.

However, the theory still does not interpret full primitive recursion. Indeed, despite having the Replacement axiom, the theory still does not proof the addition to be a set function. To this end, the axiom granting definition of set functions via iteration-step set functions must be added. We would like for a theory to interpret Peano arithmetic or, more precisely, Heyting arithmetic ${\mathsf {HA}}$, i.e. the four rules regarding addition and multiplication. What is necessary for this is an iteration principle that is the set theoretical equivalent of a natural numbers object. The principle is implied by assuming that the class of functions

$y^{\{0,1,\dots ,n\}}$

on finite domains into sets $y$ form sets themselves. This, in turn, is a special case of the Exponentiation axiom below. The use of those axioms derives from the fact that function spaces being sets means quantification over their functions is a bounded notion, enabling use of Separation. However, the induction principle obtained this way do not prove full mathematical induction for all predicates.

Nevertheless, with this bounded arithmetic given on $\omega$, arithmetic of rational numbers ${\mathbb {Q} }$ can then also be defined and its properties, like uniqueness and countability, be proven.

Exponentiation

We already considered a weakened form of the Separation schema, and more of the standard ${\mathsf {ZF}}$ axioms shall be weakened for a more predicative and constructive theory. The first one of those is the Powerset axiom, which, in effect, we adopt for decidable subsets. The characterization of the class ${\mathcal {P}}x$ of all subsets of a set $x$ involves unbounded universal quantification, namely $\forall u.u\subset x\iff u\in {\mathcal {P}}x$. Here $\subset$ has been defined in terms of the membership predicate $\in$ above. So in such a set theoretical framework, the power class is defined not in a bottom-up construction from its constituents (like an algorithm on a list, e.g. $\langle a,b\rangle \mapsto \langle \langle \rangle ,\langle a\rangle ,\langle b\rangle ,\langle a,b\rangle \rangle$) but via a comprehension over all sets. The $\{0,1\}$-valued functions on a set $x$ inject into $\Omega ^{x}$ and thus correspond to its decidable subsets.

We now consider the axiom ${\mathrm {Exp} }$:

Exponentiation $\forall x.\forall y.\ \ \exists h.h=y^{x}$

In words, the axioms says that given two sets $x,y$, the class $y^{x}$ of all functions is, in fact, also a set. Such implications are certainly required, for example, to formalize the object map of an internal hom-functor like ${\mathrm {hom} }({\mathbb {N} },-)$.

For any formula $\phi$, the class $\{x\mid (x=0)\land \phi \}$ equals $0$ when $\phi$ can be rejected and $1$ when $\phi$ can be proven, but $\phi$ may also not be decidable at all. In this view, the powerclass of the singleton $\{0\}$, i.e. ${\mathcal {P}}1$ or informally $\{0,\dots ,1\}$ and usually denoted by $\Omega$, is called the truth value algebra. Assuming all formulas are decidable, i.e. assuming ${\mathrm {LEM} }$, one can show not only that $\Omega$ is a set, but more concretely that it is this two-element set. Assuming ${\mathrm {LEM} }$ for bounded formulas, Separation lets one demonstrate that any powerclass is a set. Alternatively, full Powerset is equivalent to merely assuming that the class of all subsets of $1$ forms a set. Full Separation is equivalent to assuming that each subclass of $1$ is a set.

So in this context, function spaces are more accessible than classes of subsets, as is the case with exponential objects resp. subobjects in category theory. In type theory, the expression "$x\to y$" exists on its own and denotes function spaces, a primitive notion. These classes naturally appear, for example, as the type of the currying bijection between $(z\times x)\to y$ and $z\to y^{x}$, an adjunction. Constructive set theories are also studied in the context of applicative axioms. In category theoretical terms, the theory ${\mathsf {BCST}}+{\mathrm {Exp} }$ essentially corresponds to a constructively well-pointed Cartesian closed Heyting pretoposes with (whenever Infinity is adopted) a natural numbers object. Existence of powerset is what would turn a Heyting pretopos into an elementary topos. Every such topos that interprets ${\mathsf {ZF}}$ is of course a model of these weaker theories, but locally cartesian closed pretoposes have been defined that e.g. interpret ${\mathsf {CZFE}}$ but reject full Separation and Powerset. Exponentiation does not imply full mathematical induction.

Towards the Reals

As mentioned, Exponentiation implies recursion principles and so in ${\mathsf {ECST}}+{\mathrm {Exp} }$, one can reason about sequences ${\mathbb {Q} }^{\mathbb {N} }$ or about shrinking intervals in $({\mathbb {Q} }\times {\mathbb {Q} })^{\mathbb {N} }$ and this also enables speaking of Cauchy sequences and their arithmetic. Any Cauchy real number is a collection of sequences, i.e. subset of a set of functions on ${\mathbb {N} }$. More axioms are required to always grant completeness of equivalence classes of such sequences and strong principles need to be postulated to imply the existence of a modulus of convergence for all Cauchy sequences. Weak countable choice is generally the context for proving uniqueness of the Cauchy reals as complete (pseudo-)ordered field. "Pseudo-" here highlights that the order will, in any case, constructively not always be decidable.

As in the classical theory, Dedekind cuts are characterized using subsets of algebraic structures such as ${\mathbb {Q} }$: The properties of being are inhabited, numerically bounded above, "closed downwards" and "open upwards" are all bounded formulas with respect to the given set underlying the algebraic structure. A standard example of a cut, the first component indeed exhibits these properties, is the representation of ${\sqrt {2}}$ given by

${\big \langle }\{x\in {\mathbb {Q} }\mid x<0\lor x^{2}<2\},\,\{x\in {\mathbb {Q} }\mid 0<x\land 2<x^{2}\}{\big \rangle }\,\ \in \,\ {{\mathcal {P}}{\mathbb {Q} }}\times {{\mathcal {P}}{\mathbb {Q} }}$

(Depending on the convention for cuts, either of the two parts or neither, like here, may makes use of the sign $\leq$.)

The theory given by the axioms so far validates that a pseudo-ordered field that is also Archimedean and Dedekind complete, if it exists at all, is in this way characterized uniquely, up to isomorphism. However, the existence of just function spaces such as $\{0,1\}^{\mathbb {Q} }$ does not grant ${{\mathcal {P}}{\mathbb {Q} }}$ to be a set, and so neither is the class of all subsets of ${\mathbb {Q} }$ that do fulfill the named properties. What is required for the class of Dedekind reals to be a set is an axiom regarding existence of a set of subsets.

In either case, fewer statements about the arithmetic of the reals are decidable, compared to the classical theory.

Induction

Mathematical Induction

The iteration principle for set functions mentioned before is also implied by full induction over ones structure modeling the naturals (e.g. $\omega$). Induction reads $\mathrm {Ind} (A)\implies \omega \subset A$ for any class. It is often formulated directly in terms of predicates.

Axiom schema of full mathematical induction: For any predicate $\phi$ on $\omega$, ${\Big (}\phi (0)\ \land \ \forall (k\in \omega ).{\big (}\phi (k)\implies \phi (Sk){\big )}{\Big )}\implies \forall (n\in \omega ).\phi (n)$

Here $0$ denotes $\{\}$ and the set $Sn$ denotes the successor set of $n\in \omega$, with $n\in Sn$. By Axiom of Infinity above, it is again a member of $\omega$.

The induction axiom is implied by the full Separation schema. It can be seen to relate to it as Induction leads to a conclusion about the class $\{n\in \omega \mid \phi (n)\}$.

Induction principles are also implied by various forms of choice principles. Roughly, formulations of the Axiom of dependent choice in terms of binary predicates on some level of the hierarchy (one may again only consider bounded formulas) can be used to prove mathematical induction for predicates on that level.

Note that in the program of Predicative Arithmetic, even the mathematical induction schema has been criticized as possibly being impredicative, when natural numbers are defined as the object which fulfill this schema.

Set Induction

Full Set Induction in ${\mathsf {ECST}}$ proves full mathematical induction over the natural numbers. Indeed, it gives induction on ordinals and ordinal arithmetic. Replacement is not required to prove induction over the set of naturals, but it is for their arithmetic modeled within the set theory.

The Axiom then reads as follows

Axiom schema of Set induction: For any predicate $\phi$, ${\Big (}\forall s.\,{\big (}\forall x\in s.\ \phi (x){\big )}\implies \phi (s){\Big )}\implies \forall y.\phi (y)$

Note that $\forall x\in \{\}.\phi (x)$ holds trivially and corresponds to the "bottom case" in the standard framework. The variant of the Axiom just for bounded formulas is also studied independently and may be derived from other axioms.

The Axiom of Regularity together with (bounded) Separation implies Set Induction but also (bounded) ${\mathrm {LEM} }$, so Regularity is non-constructive. Conversely, ${\mathrm {LEM} }$ together with Set Induction implies Regularity.

Metalogic

This now covers variants of all of the eight Zermeolo-Freankel axioms. Extensionality, Pairing, Union and Replacement are indeed identical. Infinity is stated in a strong formulation and implies Emty Set, as in the classical case. Separation, classically stated redundantly, is constructively not implied by Replacement. Without the Law of Excluded Middle, the theory here is lacking full Separation, Powerset as well as Regularity in its common form.

The theory ${\mathsf {ECST}}+{\mathrm {Exp} }$ is not stronger than Heyting arithmetic but adding ${\mathrm {LEM} }$ at this stage would lead to a theory beyond the strength of typical type theory: Assuming Separation in unrestricted form, then adding ${\mathrm {LEM} }$ to ${\mathsf {ECST}}+{\mathrm {Exp} }$ gives a theory proving the same theorems as ${\mathsf {ZF}}$ minus Regularity! Thus, adding ${\mathrm {LEM} }$ to that framework gives ${\mathsf {ZF}}$ and adding Choice to it gives ${\mathsf {ZFC}}$.

The added proof-theoretical strength attained with induction in the constructive context is significant, even if dropping Regularity in the context of ${\mathsf {ZF}}$ does not reduce the proof-theoretical strength. Note that Aczel was also one of the main developers or Non-well-founded set theory, which rejects this last axiom.

Strong Collection

With all the weakened axioms of ${\mathsf {ZF}}$ and now going beyond those axioms also seen in Myhill's typed approach, the theory called ${\mathsf {CZFE}}$ (a theory with Exponentiation) strengthens the collection schema as follows:

Axiom schema of Strong Collection: For any predicate $\phi$, $\forall a.\ \ {\Big (}\forall (x\in a).\exists y.\phi (x,y){\Big )}\implies \exists b.{\Big (}\forall (x\in a).\exists (y\in b).\phi (x,y)\ \land \ \forall (y\in b).\exists (x\in a).\phi (x,y){\Big )}$

It states that if $\phi$ is a relation between sets which is total over a certain domain set $a$ (that is, it has at least one image value for every element in the domain), then there exists a set $b$ which contains at least one image under $\phi$ of every element of the domain. And this formulation then moreover states that only such images of elements of the domain. The last clause makes the axiom - in this constructive context - stronger than the standard formulation of Collection. It is guaranteeing that $b$ does not overshoot the codomain of $\phi$ and thus the axiom is expressing some power of a Separation procedure.

The axiom is an alternative to the Replacement schema and indeed supersedes it, due to not requiring the binary relation definition to be functional.

As a rule, questions of moderate cardinality are more subtle in a constructive setting. As arithmetic is well available in ${\mathsf {CZFE}}$, the theory has dependent products, proves that the class of all subsets of natural numbers cannot be subcountable and also proves that countable unions of function spaces of countable sets remain countable.

Metalogic

This theory without ${\mathrm {LEM} }$, unbounded separation and "naive" Power set enjoys various nice properties. For example, it has the Existence Property: If, for any property $\Phi$, the theory proves that a set exist that has that property, i.e. if the theory proves the statement $\exists x.\Phi (x)$, then there is also a property $\Psi$ that uniquely describes such a set instance. I.e., the theory then also proves $\exists !x.\Psi (x)\land \Phi (x)$. This can be compared to Heyting arithmetic where theorems are realized by concrete natural numbers and have these properties. In set theory, the role is played by defined sets. For contrast, recall that in ${\mathsf {ZFC}}$, the Axiom of Choice implies the Well-ordering theorem, so that total orderings with least element for sets like $\mathbb {R}$ are formally proven to exist, even if provably no such ordering can be described.

Constructive Zermelo–Fraenkel

One may approach Power set further without losing a type theoretical interpretation. The theory known as ${\mathsf {CZF}}$ is ${\mathsf {CZFE}}$ plus a stronger form of Exponentiation. It is by adopting the following alternative, which can again be seen as a constructive version of the Power set axiom:

Axiom schema of Subset Collection: For any predicate $\phi$, $\forall a.\forall b.\ \ \exists u.\forall z.{\big (}\forall (x\in a).\exists (y\in b).\phi (x,y,z){\big )}\implies \exists (v\in u).{\big (}\forall (x\in a).\exists (y\in v).\phi (x,y,z)\;\land \;\forall (y\in v).\exists (x\in a).\phi (x,y,z){\big )}$

This Subset Collection axiom schema is equivalent to a single and somewhat clearer alternative Axiom of Fullness. To this end, let $a\Sigma {b}$ is the class of all total relations between a and b, this class is given as

$r\in a\Sigma {b}\iff {\big (}\forall (x\in a).\exists (y\in b).\langle x,y\rangle \in r{\big )}\,\land \,{\big (}\forall (p\in r).\exists (x\in a).\exists (y\in b).p=\langle x,y\rangle {\big )}$

With this, we can state ${\mathrm {Fullness} }$, an alternative to Subset Collection. It guarantees that there exists at least some set $c\subseteq a\Sigma {b}$ holding the a good amount of the desired relations. More concretely, between any two sets $a$ and $b$, there is a set $c$ which contains a total sub-relation $s$ for any total relation $r$ from $a$ to $b$.

Axiom of Fullness:

$\forall a.\forall b.\ \ \exists (c\subseteq a\Sigma {b}).\forall (r\in a\Sigma {b}).\exists (s\in c).s\subseteq r$

The Fullness axiom is in turn implied by the so called Presentation Axiom about sections, which can also be formulated category theoretically.

Fullness implies the binary refinement property necessary to prove that the class of Dedekind cuts is a set. This does not require Induction or Collection.

Neither linearity of ordinals, nor existence of power sets of finite sets are derivable in this theory. Assuming either implies Power set in this context.

Metalogic

This theory lacks the existence property due to the Schema, but in 1977 Aczel showed that ${\mathsf {CZF}}$ can still be interpreted in Martin-Löf type theory, (using the propositions-as-types approach) providing what is now seen a standard model of ${\mathsf {CZF}}$ in type theory. This is done in terms of images of its functions as well as a fairly direct constructive and predicative justification, while retaining the language of set theory. As such, ${\mathsf {CZF}}$ has modest proof theoretic strength, see ${\mathsf {IKP}}$: Bachmann–Howard ordinal.

Breaking with ZF

One may further add the non-classical axiom that all sets are subcountable. Then ${\mathbb {N} }^{\mathbb {N} }$ is a set (by Infinity and Exponentiation) while the class ${\mathcal {P}}{\mathbb {N} }$ or even ${\mathcal {P}}\{0\}$ is provably not a set, by Cantors diagonal argument. So this theory then logically rejects Powerset and ${\mathrm {LEM} }$.

In 1989 Ingrid Lindström showed that non-well-founded sets obtained by replacing the equivalent of the Axiom of Foundation (Induction) in ${\mathsf {CZF}}$ with Aczel's anti-foundation axiom (${\mathsf {CZFA}}$) can also be interpreted in Martin-Löf type theory.

Intuitionistic Zermelo–Fraenkel

The theory ${\mathsf {IZF}}$ is ${\mathsf {CZF}}$ with the standard Separation and Power set.

Here, in place of the Axiom schema of replacement, we may use the

Axiom schema of collection: For any predicate $\phi$, $\forall z.{\big (}\forall (x\in z).\exists y.\phi (x,y){\big )}\implies \exists w.\forall (x\in z).\exists (y\in w).\phi (x,y)$

While the axiom of replacement requires the relation $\phi$ to be functional over the set $z$ (as in, for every $x$ in $z$ there is associated exactly one $y$), the Axiom of Collection does not. It merely requires there be associated at least one $y$, and it asserts the existence of a set which collects at least one such $y$ for each such $x$. ${\mathrm {LEM} }$ together with the Collection implies Replacement.

As such, ${\mathsf {IZF}}$ can be seen as the most straight forward variant of ${\mathsf {ZF}}$ without ${\mathrm {LEM} }$.

Metalogic

Changing the Axiom schema of Replacement to the Axiom schema of Collection, the resulting theory has the Existence Property.

Even without ${\mathrm {LEM} }$, the proof theoretic strength of ${\mathsf {IZF}}$ equals that of ${\mathsf {ZF}}$.

While ${\mathsf {ZF}}$ is based on intuitionistic rather than classical logic, it is considered impredicative. It allows formation of sets using the Axiom of Separation with any proposition, including ones which contain quantifiers which are not bounded. Thus new sets can be formed in terms of the universe of all sets. Additionally the power set axiom implies the existence of a set of truth values. In the presence of excluded middle, this set exists and has two elements. In the absence of it, the set of truth values is also considered impredicative.

History

In 1973, John Myhill proposed a system of set theory based on intuitionistic logic taking the most common foundation, ${\mathsf {ZFC}}$, and throwing away the Axiom of choice and the law of the excluded middle, leaving everything else as is. However, different forms of some of the ${\mathsf {ZFC}}$ axioms which are equivalent in the classical setting are inequivalent in the constructive setting, and some forms imply ${\mathrm {LEM} }$. In those cases, the intuitionistically weaker formulations were then adopted for the constructive set theory.

Intuitionistic Z

Again on the weaker end, as with its historical counterpart Zermelo set theory, one may denote by ${\mathsf {IZ}}$ the intuitionistic theory set up like ${\mathsf {IZF}}$ but without Replacement, Collection or Induction.

Intuitionistic KP

Let us mention another very weak theory that has been investigated, namely Intuitionistic (or constructive) Kripke–Platek set theory ${\mathsf {IKP}}$. The theory has not only Separation but also Collection restricted, i.e. it is similar to ${\mathsf {BCST}}$ but with Induction instead of full Replacement. It is especially weak when studied without Infinity. The theory does not fit into the hierarchy as presented above, simply because it has Axiom schema of Set Induction from the start. This enables theorems involving the class of ordinals.

Sorted theories

Constructive set theory

As he presented it, Myhill's system ${\mathsf {CST}}$ is a constructive first-order logic with identity and three sorts, namely sets, natural numbers, functions:

• The usual Axiom of Extensionality for sets, as well as one for functions, and the usual Axiom of union.
• The Axiom of restricted, or predicative, separation, which is a weakened form of the Separation axiom in classical set theory, requiring that any quantifications be bounded to another set.
• A form of the Axiom of Infinity asserting that the collection of natural numbers (for which he introduces a constant ${\mathbb {N} }$) is in fact a set.
• The Axiom of Exponentiation, asserting that for any two sets, there is a third set which contains all (and only) the functions whose domain is the first set, and whose range is the second set. This is a greatly weakened form of the Axiom of power set in classical set theory, to which Myhill, among others, objected on the grounds of its impredicativity.
• An Axiom of dependent choice, which is much weaker than the usual Axiom of choice.

And furthermore:

• The usual Peano axioms for natural numbers.
• Axioms asserting that the domain and range of a function are both sets. Additionally, an Axiom of non-choice asserts the existence of a choice function in cases where the choice is already made. Together these act like the usual Replacement axiom in classical set theory.

Bishop style set theory

Set theory in the flavor of Errett Bishop's constructivist school mirrors that of Myhill, but is set up in a way that sets come equipped with relations that govern their discreteness. Commonly, Dependent Choice is adopted.

Category theories

Not all formal logic theories of sets need to axiomize the binary membership predicate "$\in$" directly. And an Elementary Theory of the Categories Of Set (${\mathsf {ETCS}}$), e.g. capturing pairs of composable mappings between objects, can also be expressed with a constructive background logic (${\mathsf {CETCS}}$).

Good models of constructive set theories in category theory are the pretoposes mentioned in the Exponentiation section - possibly also requiring enough projectives, an axiom about surjective "presentations" of set, implying Countable Dependent Choice.

Beyond that, topoi also have internal languages that can be intuitionistic themselves and capture a notion of sets.

See also

• Constructive mathematics
• Intuitionistic type theory
• Ordinal analysis
• Impredicativity
• Existence Property
• Law of excluded middle
• Subcountability

Further reading

• Troelstra, Anne; van Dalen, Dirk (1988). Constructivism in Mathematics, Vol. 2. Studies in Logic and the Foundations of Mathematics. p. 619. ISBN 978-0-444-70358-3.
• Aczel, P. and Rathjen, M. (2001). Notes on constructive set theory. Technical Report 40, 2000/2001. Mittag-Leffler Institute, Sweden.

External links

• Laura Crosilla, Set Theory: Constructive and Intuitionistic ZF, Stanford Encyclopedia of Philosophy, Feb 20, 2009
• Benno van den Berg, Constructive set theory – an overview, slides from Heyting dag, Amsterdam, 7 September 2012