IZF

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.

In addition to rejecting the principle of excluded middle ($$), constructive set theories often require some logical quantifiers in their axioms to be bounded, motivated by results tied to impredicativity.

Introduction

Constructive outlook

Use of intuitionistic logic

The logic of the set theories discussed here is constructive in that it rejects $$, i.e. that the disjunction $\phi \lor \neg \phi$ automatically holds for all propositions. As a rule, to prove the excluded middle for a proposition $P$, i.e. to prove the particular disjunction $P \lor \neg P$, either $P$ or $\neg P$ needs to be explicitly proven. When either such proof is established, one says the proposition is decidable, and this then logically implies the disjunction holds. Similarly, a predicate $Q(x)$ on a domain $X$ is said to be decidable when the more intricate statement $\forall (x\in X). \big(Q(x) \lor \neg Q(x)\big)$ is provable. Non-constructive axioms may enable proofs that ''formally'' decide such $P$ (and/or $Q$) in the sense that they prove excluded middle for $P$ (resp. the statement using the quantifier above) without demonstrating the truth of any of the disjuncts, as is often the case in classical logic. In contrast, constructive theories tend to not permit many classical proofs of properties that are provenly computationally undecidable. Similarly, a counter-example existence claim $\exist(x\in X). \neg R(x)$ is generally constructively stronger than a rejection claim $\neg \forall(x\in X). R(x)$.

The intuitionistic logic underlying the set theories discussed here, unlike the more conservative minimal logic, still permits double negation elimination for individual propositions for which excluded middle holds, and in turn the theorem formulations regarding finite objects tends to not differ from their classical counterparts. Given a model of all numbers, the equivalent for predicates, namely Markov's principle, does not automatically hold, but may be considered as an additional principle.

Expressing the instance for $\neg P$ of the valid law of noncontradiction and using a valid De Morgan's law, already minimal logic does prove $\neg\neg(P \lor \neg P)$ for any given proposition $P$. So in words, intuitionistic logic still posits: It is impossible to rule out a proposition and rule out its negation both at once, and thus the rejection of any instantiated excluded middle statement for an individual proposition is inconsistent. More generally, constructive mathematical theories 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 double negation elimination and its consequences are assumed legal, are at once classically equivalent to the classical statement. The difference is that the constructive proofs are harder to find.

Imposed restrictions

A restriction to the constructive reading of existence apriori leads to stricter requirements regarding which characterizations of a set $f\subset X\times Y$ involving unbounded collections constitute a (mathematical, and so always implying total) function. This is often because the predicate in a case-wise would-be definition may not be decidable. Compared to the classical counterpart, one is generally less likely to prove the existence of relations that cannot be realized. Adopting the standard definition of set equality via extentionality, the full Axiom of Choice is such a non-constructive principle that implies $$ for the formulas permitted in one's adopted Separation schema, by Diaconescu's theorem. Similar results hold for the Axiom of Regularity in its standard form, as shown below. So at the very least, the development of constructive set theory requires rejection of strong choice principles and the rewording of some standard axioms to classically equivalent ones. Undecidability of disjunctions also affects the claims about total orders such as that of all ordinal numbers, expressed by the provability and rejection of the clauses in the order defining disjunction $(\alpha \in \beta) \lor (\alpha = \beta) \lor (\beta \in \alpha)$. This determines whether the relation is trichotomous. And this in turn affects the proof theoretic strength defined in ordinal analysis.

Metalogic

As in the study of constructive arithmetic theories, constructive set theories can exhibit attractive disjunction and existence properties. These are features of a fixed theory which relate metalogical judgements and propositions provable in the theory. Particularly well-studied are those such features that can be expressed in Heyting arithmetic, with quantifiers over numbers and which can often be realized by numerals, as formalized in proof theory. In particular, those are the numerical existence property and the closely related disjunctive property, as well as being closed under Church's rule, witnessing any given function to be computable.

A set theory does not only express theorems about numbers. Furthermore, one may consider a more general strong existence property that is harder to come by, as will be discussed. The theory has the property if the following can be established: For any property $\phi$, if the theory proves that a set exist that has that property, i.e. if the theory claims the existence statement, then there is also a property $\psi$ that uniquely describes such a set instance. More formally, for any predicate $\phi$ there is a predicate $\psi$ so that
:$\vdash\exists x.\phi(x)\implies\vdash\exists !x. \phi(x)\land\psi(x)$
The analogous role of the realized numeral is played by defined sets proven to exist according to the theory, and so this is a subtle question concerning term construction and the theories strength. While many theories discussed tend have all the various numerical properties, the existence property can easily be spoiled, as will be discussed. Weaker forms of existence properties have been formulated.

Some classical theories can in fact also be constrained to exhibit the strong existence property. Zermelo–Fraenkel set theory $$ with the constructible universe postulate, $+(=)$, or $$ with sets all taken to be ordinal-definable, $+(=)$, do have the existence property. For contrast, consider the theory $$ given by $$ plus the full axiom of choice ''existence postulate''. Recall that this set of axioms implies the well-ordering theorem, which in particular means that relations for $$ that establish its well-ordering are formally proven to exist (and claim existence of a least element for all subsets of $$ with respect to those relations). This is despite that fact that definability of such an ordering is known to be independent of $$. The latter implies that for no particular formula $\psi$ in the language of the theory does the theory prove that the corresponding set is a well-ordering relation of the reals. So $$ formally ''proves the existence'' of a subset $x\subset\times$ with the property of being a well-ordering relation, but at the same time no particular set $x$ for which the property could be validated can possibly be defined.

Anti-classical principles

A situation commonly studied is that of a fixed theory $$ exhibiting the following meta-theoretical property: For an instance from some collection of formulas, here captured via $\phi$ and $\psi$, one established the existence of a numeral constant $e$ so that $\vdash \phi\implies\vdash \psi(e)$. When adopting such a schema as an inference rule and nothing new can be proven, one says the theory $$ is closed under that rule. Adjoining excluded middle $$ to $$, the new theory may then prove new, strictly classical statements for $\phi$ and this may spoil the meta-theoretical property that was previously established for $$.
One may instead consider adjoining the rule corresponding to the meta-theoretical property as an implication to $$, as a schema or in quantified form. That is to say, to postulate that any such $\phi$ implies $\exists (e\in)$ such that $\psi(e)$ holds, where the bound $e$ is a number variable in language of the theory. The new theory with the principle added might be anti-classical, in that it may not be consistent anymore to also adopt $$.
For example, Church's rule is an admissible rule in Heyting arithmetic $$ and the corresponding Church's thesis principle may be adopted, but the same is not possible in $+$, also known as Peano arithmetic $$.

Now for a context of set theories with quantification over a fully formal notion of an infinite sequences space, i.e. function spaces, as will be defined below. A translation of Church's ''rule'' into the language of the theory itself may then read
:$\forall (f\in^).\exists (e\in).\Big(\forall(n\in).\exists(w\in). T(e, n, w)\land U(w, f(n))\Big)$
Kleene's T predicate together with the result extraction expresses that any input number $n$ being mapped to the number $f(n)$ is, through $w$, witnessed to be a computable mapping. Here $$ now denotes a set theory model of the standard natural numbers and $e$ is an index with respect to a fixed program enumeration. Stronger variants have been used, which extend this principle to functions $f\in^X$ defined on domains $X\subset$ of low complexity. The principle rejects decidability for the predicate $Q(e)$ defined as $\exists(w\in). T(e, e, w)$, expressing that $e$ is the index of a computable function halting on its own index. Weaker, double negated forms of the principle may be considered too, which do not require the existence of a recursive implementation for every $f$, but which still make principles inconsistent that claim the existence of functions which provenly have no recursive realization. Some forms of a Church's thesis as principle are even consistent with the weak classical second order arithmetic $_0$.

The collection of total, computable functions is classically subcountable, which classically is the same as being countable. But classical set theories will generally claim that $^$ holds also other functions than the computable ones. For example there is a proof in $$ that total functions do exist that cannot be captured by a Turing machine.
Taking the computable world seriously as ontology, a prime example of an anti-classical conception related the Markovian school is the permitted subcountability of various uncountable collections. Adopting the subcountability of the collection of all unending sequences of natural numbers ($^$) as an axiom, the "smallness" (in classical terms) of this collection in some realizations of a set theory is then already captured by that theory.
A constructive theory may also adopt neither classical nor anti-classical axioms and so stay agnostic towards either possibility.

Constructive principles already prove $\forall (x\in X).\neg\neg\big(Q(x) \lor \neg Q(x)\big)$ and so for any given element $x$ of $X$, the corresponding excluded middle statement for the proposition cannot be negated. Indeed, for any given $x$, by noncontradiction it is impossible to rule out $Q(x)$ and rule out its negation both at once. But a theory may in some instances also permit the rejection claim $\neg\forall (x\in X). \big(Q(x) \lor \neg Q(x)\big)$. Adopting this does not necessitate providing a particular $t\in X$ witnessing the failure of excluded middle for the particular proposition $Q(t)$, i.e. witnessing the inconsistent $\neg\big(Q(t)\lor\neg Q(t)\big)$. One may reject the possibility of decidability of some predicate $Q(x)$ on an infinite domain $X$ without making any existence claim in $X$.
As another example, such a situation is enforced in Brouwerian intuitionistic analysis, in a case where the quantifier ranges over infinitely many unending binary sequences and $Q(x)$ states that a sequence $x$ is everywhere zero. Concerning this property, of being conclusively identified as the sequence which is forever constant, adopting Brouwer's continuity principle rules out that this could be proven decidable for all the sequences.

So in a constructive context with a so-called non-classical logic as used here, one may consistently adopt axioms which are both in contradiction to quantified forms of excluded middle, but also non-constructive in the computable sense or as gauged by meta-logical existence properties discussed previously. In that way, a constructive set theory can also provide the framework to study non-classical theories.

History and overview

Historically, the subject of constructive set theory (often also "$$") begun with John Myhill's work on the theories also called $$ and $$.
In 1973, he had proposed the former as a first-order set theory based on intuitionistic logic, taking the most common foundation $$ and throwing out the Axiom of choice as well as the principle of the excluded middle, initially leaving everything else as is. However, different forms of some of the $$ axioms which are equivalent in the classical setting are inequivalent in the constructive setting, and some forms imply $$, as will be demonstrated. In those cases, the intuitionistically weaker formulations were consequently adopted. The far more conservative system $$ is also a first-order theory, but of several sorts and bounded quantification, aiming to provide a formal foundation for Errett Bishop's program of constructive mathematics.

The main discussion presents sequence of theories in the same language as $$, leading up to Peter Aczel's well studied ''$$'', and beyond. Many modern results trace back to Rathjen and his students.
$$ 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, see also Lévy hierarchy.
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.
Adding $$ to a theory even weaker than $$ recovers $$, as detailed below.
The system, which has come to be known as Intuitionistic Zermelo–Fraenkel set theory ($$), is a strong set theory without $$. It is similar to $$, but less conservative or predicative.
The theory denoted $$ is the constructive version of $$, the classical Kripke–Platek set theory without a form of Powerset and where even the Axiom of Collection is bounded.

Models

As far as constructive realizations go there is a relevant realizability theory. Relatedly, Aczel's theory constructive Zermelo-Fraenkel $$ has been interpreted in a Martin-Löf type theories, as described below. In this way, set theory theorems provable in $$ and weaker theories are candidates for a computer realization.

For a set theory context without infinite sets, constructive first-order arithmetic can also be taken as an apology for most axioms adopted in $$: The arithmetic theory $$ is bi-interpretable with a weak constructive set theory, as described in the article on Heyting arithmetic. One may arithmetically characterize a membership relation "$\in$" and with it prove - instead of the existence of a set of natural numbers $\omega$ - that all sets in its theory are in bijection with a (finite) von Neumann natural, a principle denoted $=$. This context further validates Extensionality, Pairing, Union, Binary Intersection (which is related to the Axiom schema of predicative separation) and the Set Induction schema. Taken as axioms, the aforementioned principles constitute a set theory that is already identical with the theory given by $$ minus the existence of $\omega$ but plus $=$ as axiom. All those axioms are discussed in detail below.
Relatedly, $$ also proves that the hereditarily finite sets fulfill all the previous axioms. This is a result which persists when passing on to $$ and $$ minus Infinity.

Many theories studied in constructive set theory are mere restrictions of Zermelo–Fraenkel set theory ($$) with respect to their axiom as well as their underlying logic. Such theories can then also be interpreted in any model of $$.

More recently, presheaf models for constructive set theories have been introduced. These are analogous to presheaf models for intuitionistic set theory developed by Dana Scott in the 1980s.

Subtheories of ZF

Notation

Language

The propositional connective symbols used to form syntactic formulas are standard. The axioms of set theory give a means to prove equality "$=$" of sets and that symbol may, by abuse of notation, be used for classes. Negation "$\neg$" of elementhood "$\in$" is often written "$\notin$", and usually the same goes for non-equality "$\neq$", although in constructive mathematics the latter symbol is also used in the context with apartness relations.

Variables

Below the Greek $\phi$ denotes a predicate variable in axiom schemas and $P$ or $Q$ is used for particular predicates. The word "predicate" is often used interchangeably with "formulas" as well, even in the unary case.

Quantifiers range over sets and those are denoted by lower case letters.
As is common, one may use argument brackets to express predicates, for the sake of highlighting particular free variables in their syntactic expression, as in "$P(z)$".

One abbreviates $\forall z. \big(z\in A\to P(z)\big)$ by $\forall (z\in A). P(z)$ and $\exists z. \big(z\in A\land P(z)\big)$ by $\exists (z\in A). P(z)$. The syntactic notion of bounded quantification in this sense can play a role in the formulation of axiom schemas, as seen below.

Express the subclass claim $\forall (z\in A). z\in B$, i.e. $\forall z. (z\in A\to z\in B)$, by $A\subset B$.
The similar notion of subset-bounded quantifiers, as in $\forall (z\subset A). z\in B$, has been used in set theoretical investigation as well, but will not be further highlighted here.

Unique existence $\exists!x. P(x)$ here means $\exists x. \forall y. \big(y=x \leftrightarrow P(y)\big)$.

Classes

As is also common in the study of set theories, 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=\$", 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 $\$ as shorthand for $\$.
For a property $P$, trivially $\forall z.\big((z\in B\land P(z))\to z\in B\big)$. And so follows that $\\subset B$.

Equality

Denote by $A\simeq B$ the statement expressing that two classes have exactly the same elements, i.e. $\forall z. (z\in A \leftrightarrow z\in B)$, or equivalently $(A\subset B)\land (B\subset A)$. This is not to be conflated with the concept of equinumerosity.

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

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

In a constructive interpretation, the elements of a subclass $A=\$ of $B$ may come equipped with more information than those of $B$, in the sense that being able to judge $b\in A$ is being able to judge $Q(b)\lor\neg Q(b)$. And (unless the whole disjunction follows from axioms) in the Brouwer–Heyting–Kolmogorov interpretation, this means to have proven $Q(b)$ or having rejected it.
As $Q$ may be not decidable for all elements in $B$, the two classes must a priori be distinguished.

Consider a property $P$ that provenly holds for all elements of a set $y$, so that $\\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. While often adopted, this axiom has been criticized in constructive thought, as it effectively collapses differently defined properties, or at least the sets viewed as the extension of these properties, a Fregian notion.

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 for the elements $z\in x$ of each and every set $x$ discussed. Even then, the above definition can be used to characterize equality of subsets $u\subset x$ and $v\subset x$.
Note that adopting "$=$" as a symbol in a predicate logic theory makes equality of two terms a quantifier-free expression.

Merging sets

Two other basic axioms are as follows. Firstly,

saying that for any two sets $x$ and $y$, there is at least one set $p$, which hold at least those two sets ($z$).

And then,

saying that for any set $x$, there is at least one set $u$, which holds all members $y$, of $x$'s members $z$.

The two axioms may also be formulated stronger in terms of "$\leftrightarrow$". In the context of $$ with Separation, this is not necessary.

Together, the two previous 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 by $\bigcup\$ or $a\cup b$. For a fixed set $y$, to validate membership $y\in a\cup b$ in the union of two given sets $z=a$ and $z=b$, one needs to validate the $y\in z$ part of the axiom, which can be done by validating the disjunction of the predicates defining the sets $a$ and $b$, for $y$.

Define class notation for a few given elements via disjunctions, e.g. $c\in\$ says $(c=a)\lor(c=b)$.
Denote by $\langle x, y\rangle$ the standard ordered pair model $\$.

Set existence

The property that is false for any set corresponds to the empty class, which is denoted by $\$ or zero, 0. That the empty class 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 one's study, one may at this point adopt the

This axiom would also readily be accepted, but is not relevant in the context of stronger axioms below. Introduction of the symbol $\$ (as abbreviating notation for expressions in involving characterizing properties) is justified as uniqueness for this set can be proven.
If there provenly ''exists'' a set $t\in s$ inside a set $s$, then we call $s$ ''inhabited'' and it is then provenly not the empty set. While classically equivalent, constructively ''non-empty'' is a weaker notion with two negations. Unfortunately, the word for the more useful notion of 'inhabited' is rarely used in classical mathematics.

For a set $x$, define the successor set $Sx$ as $x\cup\$, for which $x\in Sx$.
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.

A simple and provenly false proposition then is, for example, $\\in\$, corresponding to $0 < 0$ in the standard arithmetic model.
Again, here symbols such as $\$ are treated as convenient notation and any proposition really translates to an expression using only "$\in$" and logical symbols, including quantifiers. Accompanied by a metamathematical analysis that the capabilities of the new theories are equivalent in an effective manner, formal extensions by symbols such as $0$ may also be considered.

BCST

The following makes use of axiom schemas, i.e. 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.

Separation

Basic constructive set theory $$ consists of several axioms also part of standard set theory, except the Separation axiom is weakened.
Beyond the four axioms above, it the Predicative Separation as well as the Replacement schema.

This axiom amounts to postulating the existence of a set $s$ obtained by the intersection of any set $y$ and any predicatively described class $\$.
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$. Intersection corresponds to conjunction in an analog way to how union corresponds to disjunction.

As noted, from Separation and the existence of at least one set (e.g. Infinity below) and a predicate that is false of any set, like $\neg(x=x)$, will follow the existence of the empty set.
Within this conservative context of $$, 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 formula schema.

The axiom schema is also called Bounded Separation, as in Separation for set-bounded quantifiers only. It is a schema that takes into account syntactic aspects of predicates. The scope of legal formulas is enriched by further set existence postulates. The bounded formulas are also denoted by $\Delta_0$ in the set theoretical Lévy hierarchy, in analogy to $\Delta_0^0$ in the arithmetical hierarchy. (Note however that the arithmetic classification is sometimes expressed not syntactically but in terms of subclasses of the naturals. Also, the bottom level of the arithmetical hierarchy has several common definitions, some not allowing the use of some total functions. The distinction is not relevant on the level $\Sigma_1^0$ or higher.) The schema is also the way in which Mac Lane weakens a system close to Zermelo set theory $$, for mathematical foundations related to topos theory.

No universal set

The following holds for any relation $E$, giving a purely logical condition by which two terms $s$ and $y$ non-relatable
:$\forall x. \big(xEs\leftrightarrow(xEy \land \neg xEx)\big) \to \neg(yEs\lor sEs\lor sEy)$
The expression $\neg(x\in x)$ is a bounded one and thus allowed in separation. By virtue of the rejection of the final disjunct above, $\neg sEy$, Russel's construction shows that $\\notin y$. So for any set $y$, Predicative Separation alone implies that there exists a set which is not a member of $y$. In particular, no universal set can exist in this theory.
In a theory with the axiom of regularity, like $$, of course that subset $\$ can be proven to be equal to $y$ itself. As an aside, in a theory with stratification, a universal set may exist because use of the syntactic expression $x\in x$ may be disallowed in proofs of existence by, essentially, separation.

Predicativity

The restriction in the axiom is also gatekeeping impredicative definitions: Existence should at best not be claimed for objects that are not explicitly describable, or whose definition involves themselves or reference to a proper class, such as when a property to be checked involves a universal quantifier. So in a constructive theory without Axiom of power set, when $Q$ denotes some 2-ary predicate, one should not generally expect a subclass $s$ of $y$ to be a set, in case that it is defined, for example, as in
:$\$,
or via a similar definitions involving any quantification over the sets $t\subset y$. Note that if this subclass $s$ of $y$ is provenly a set, then this subset itself is also in the unbounded scope of set variable $t$. In other words, as the subclass property $s\subset y$ is fulfilled, this exact set $s$, defined using the expression $Q(x, s)$, would play a role in its own characterization.

While 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. So in this way, one gets a broader theory, constructively.
Due to the potential undecidability of general predicates, the notion of subset and subclass is more elaborate in constructive set theories than in classical ones. This remains true if full Separation is adopted, as in the theory $$, which however spoils the existence property as well as the standard type theoretical interpretations, and in this way spoils a bottom-up view of constructive sets. As an aside, as subtyping is not a necessary feature of constructive type theory, constructive set theory can be said to quite differ from that framework.

Replacement

Next consider the

It is granting existence, as sets, of the range of function-like predicates, obtained via their domains. In the above formulation, the predicate is not restricted akin to the Separation schema, but this axiom already involves an existential quantifier in the antecedent. Of course, weaker schemas could be considered as well.

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.
Equality of elements inside a set $x$ is decidable if the corresponding relation as a subset of $x\times x$ is decidable.

Replacement is not necessary in the design of a weak constructive set theory that is bi-interpretable with Heyting arithmetic $$. However, some form of induction is. Replacement together with Set Induction (introduced below) also 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.

Replacement can be seen as a form of comprehension. Only when assuming $$ does Replacement already imply full Separation. In $$, Replacement is mostly important to prove the existence of sets of high rank, namely via instances of the axiom schema where $\phi(x,y)$ 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 $$, but instead merely to gain back some provability strength. Such stronger axioms exist that do not spoil the strong existence properties of a theory, as discussed further below.

The discussion now proceeds with axioms granting existence of objects also found in dependent type theory, namely natural numbers and products.

ECST

Denote by $\mathrm(A)$ the inductive property, $0\in A\land\forall (n\in A). Sn \in A$. Here $n$ denotes a generic set variable.
In terms of a predicate $P$ underlying the class so that $\forall n. (n\in A)\leftrightarrow P(n)$, this translates to $P(0) \land \forall n. \big(P(n)\to P(Sn)\big)$.

For some fixed predicate $Q$, the statement $Q(a)\land\big(\forall x. Q(x)\to a\subset x\big)$ expresses that $a$ is the smallest (in the sense of "$\subset$") set among all sets $x$ for which $Q(x)$ holds true.

The elementary constructive Set Theory $$ has the axiom of $$ as well as the postulate of the existence of a smallest inductive set

Write $\bigcap B$ for $\$, the general intersection.
Define a class $\omega=\bigcap\$, the intersection of all inductive sets.
With the above axiom, $\omega$ is a uniquely characterized set, the smallest infinite von Neumann ordinal. Its elements include the empty set and, for each set in $\omega$, another set in $\omega$ that contains one element more. Symbols called zero and successor are in the signature of the theory of Peano. In $$, the above defined successor of any number also being in the class $\omega$ follow directly from the characterization of the natural naturals by our von Neumann model. Since the successor of such a set contains itself, one also finds that no successor equals zero. So two of the Peano axioms regarding the symbols zero and the one regarding closedness of $S$ come easily. Fourthly, in $$, where $\omega$ is a set, $S$ can be proven to be an injective operation.

The pairwise order "$<$" on the naturals is captured by their membership relation "$\in$". It is important to note that the theory proves the order as well as the equality relation on this set to be decidable. The value of formulating the axiom using the inductive property is explained in the discussion on arithmetic.
Weak forms of axioms of infinity can be formulated, all postulating that some set containing elements 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 is
:$\exists w. \forall m. \big( m \in w \leftrightarrow (m=0 \lor (\exists p \in w). E(p, m)) \big)$,
where $E(p, m)$ captures the predecessor membership relation in the von Neumann model
:$\forall n. (n\in m \leftrightarrow (n = p \lor n \in p))$.
This weaker axioms characterizes the infinite set by expressing that all elements $m$ of it are either equal to $0$ or themselves hold a predecessor set which shares all other members with $m$.
This form can also be written more concisely using the successor notation $S$.

Number bounds

For a class of numbers $I\subset\omega$, the statement
:\exists(m\in \omega).\forall(n\in\omega).(n\in I\to n
or the weaker contrapositive variant
:$\exists(m\in \omega).\forall(n\in\omega).(m\le n\to n\notin I)$
are statements of finiteness. For decidable properties, these are $\Sigma_2^0$-statements in arithmetic, but with the axiom of Infinity, the two quantifiers are set-bound. Denote an initial segment of the natural numbers, i.e.
$\$
for any $m\in\omega$ and including the empty set, by
$\$.
This set equals $m$ and so at this point "$m-1$" is mere notation for its predecessor (i.e. not involving subtraction function).
To reflect more closely the discussion of functions below, write the above condition as
:\exists(m\in \omega).\forall(n\in I).(n.
Now for a general set, to be finitely enumerable shall mean that there is a surjection from a von Neumann natural number onto it, which is a function existence claim. Further, 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 $$. Terminology for finiteness conditions varies with authors and there are many more related definitions.

For a class $C$, the statement
:$\forall(m\in\omega).\exists(n\in\omega).(m\le n\land n\in C)$
is one of infinitude. It is $\Pi_2^0$ in the decidable arithmetic case. To validate infinitude of a set, this property even works if the set holds other elements besides infinitely many of members of $\omega$. But more generally, call a set infinite if one can inject $\omega$ into it, which is again a function existence claim.

It is appropriate to discuss the function concept at this point.

Functions

General notes on functions

Naturally, the logical meaning of existence claims is a topic of interest in intuitionistic logic, be it for a theory of sets or any other mathematical framework. A constructive proof calculus may validate statements as above,
:$\forall (a\in A). \exists (c\in C). P(a, c)$,
in terms of programs on represented domains. Consider for example the notions of proof through type- or realizability theory. Roughly, the task then is to provide a mapping $a\mapsto c_a$ and witness the rewriting $\forall (a\in A). P(a, c_a)$.

It is a theorem that already Robinson arithmetic $$ ''represents'' exactly the recursive functions in terms of particular predicates $P$, which are then also proven total ''functional'',
:$\forall (a\in). \exists! (c\in). P(a, c)$.
The weak classical arithmetic theory $$ postulates, instead of using the full mathematical induction schema for arithmetic formulas, that every number is either zero or that there exists a predecessor number to it.

Finally, beware of a common ambiguity in related texts on recursion theory, where "function" needs to be understood in the computable sense, which is generally narrower than what is discussed further below. Similarly, below there is also no need to speak of "''total'' functions", as this is part of the definition of a set theoretical function.

Total functional relations

Now in the current set theoretical approach, define the property involving the function application brackets, $f(a)=c$, as $\langle a, c\rangle \in f$ and speak of a function $f\subset A\times C$ when provenly
:$\forall (a\in A).\, \exists! (c\in C). f(a)=c$,
i.e.
:$\forall (a\in A).\, \exists (c\in C).\, \forall (d\in C). \big(d=c \leftrightarrow \langle a, d\rangle \in f\big)$,
which notably involves quantifier explicitly asking for existence. So one studies sets capturing particular total relations. Whether a subclass can be judged to be a function will depend on the strength of the theory, which is to say the axioms one adopts.
Notably, a general class could fulfill the above predicate without being a subclass of the product $A\times C$, i.e. the property is expressing not more or less than functionality w.r.t. inputs from $A$.
If the domain is a set, then the function has a pair for each of its elements and so exists as set.
If domain and codomain are sets, then the above predicate only involves bounded quantifiers.
Let $C^A$ (also written $^AC$) denote the class of 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$. Below might write $x\to y$ for $y^x$ for the sake of distinguishing it from ordinal exponentiation.

Common notions such as surjectivity and injectivity can be expressed in a bounded fashion as well. Note that injectivity shall be defined positively, not by its contrapositive, which is common practice in classical mathematics.

The axiom scheme of Replacement can also be formulated in terms of the ranges of such set functions.
It is a metatheorem for theories containing $$ that adding a function symbol for a provenly total class function is a conservative extension, despite this changing the scope of bounded Separation.

Separation lets us cut out subsets of products $A\times C$, at least when they are described in a bounded fashion.
Write $1$ for $S0$. Given any $B\subset A$, one is now led to reason about classes such as
:$\.$
The boolean-valued characteristic functions $\chi_B\colon A\to\$ are among such classes. But be aware that $a\in B$ may in generally not be decidable. That is to say, in absence of any non-constructive axioms, the disjunction $a\in B\lor a\notin B$ may not be provable, since one requires an explicit proof of either disjunct. Constructively, when
:$\exists(y\in\). f(a) = y$
cannot be witnessed for all $a\in A$, or uniqueness of a term $y$ associated with $a$ not be proven, then one cannot judge the comprehended collection to be total functional.

Variants of the functional predicate definition using apartness relations on setoids have been defined as well. A function will be a set if its range is. Care must be taken with nomenclature "function", which sees use in most mathematical frameworks, also because some tie a function term itself to a particular codomain.

Computable sets

Given Infinity and any propositions $Q$, let $I=\$. Given any natural $n\in\omega$, then
:$\big(Q(n)\lor \neg Q(n)\big)\to\big(n\in I\lor n\notin I\big)$.
In classical set theory, as $Q$ is formally decidable just by $$, so is subclass membership. If the class $I$ is not finite, then successively going through the natural numbers $n$, and thus "listing" all numbers in $I$ by simply skipping those with $n\notin I$, classically constitutes an increasing surjective sequence $a:\omega\twoheadrightarrow I$. There, one can obtain a bijective ''function''. In this way, the classical class of functions is provenly rich, as it also contains objects that are beyond what we know to be ''effectively'' computable, or programmatically listable in praxis.

In computability theory, the computable sets are ranges of non-decreasing total functions ''in the recursive sense'', at the level $\Sigma_1^0 \cap \Pi_1^0 = \Delta_1^0$ of the arithmetical hierarchy, and not higher. Deciding a predicate at that level amounts to solving the task of eventually finding a certificate that either validates or rejects membership.
As not every predicate $Q$ is computably decidable, the theory $$ alone will not claim (prove) that all infinite $I\subset \omega$ are the range of some bijective function with domain $\omega$. See also Kripke's schema.

But being compatible with $$, the development in this section still always permits "function on $\omega$" to be interpreted as an object not necessarily given as lawlike sequence. Applications may be found in the common models for claims about probability, e.g. statements involving the notion of "being given" an unending random sequence of coin flips.

Choice functions

Choice principles postulate the existence of functions. These can then be translated to claims of existence of inverses, ordering, and so on. Choice moreover implies statements about cardinalities of different sets, e.g. they imply or rule out countability of sets.
The constructive development here proceeds in a fashion agnostic to any discussed choice principles, but here are well studied variants:

* Axiom of countable choice: If $g\colon\omega\to z$, one can form the one-to-many relation-set $\$. The axiom of countable choice would grant that whenever $\forall (n\in\omega). \exists u. u\in g(n)$, one can form a function mapping each number to a unique value. Countable choice can also be weakened further. One common consideration is to restrict the possible cardinalities of the range of $g$, giving the weak countable choice into countable, finite or even just binary sets. Another means of weakening countable choice is by restricting the involved definitions w.r.t. their place in the syntactic hierarchies. Countable choice is not valid in the internal logic of a general topos, which can be seen as models of constructive set theories.
* Axiom of dependent choice: Countable choice is implied by the more general axiom of dependent choice, extracting a function from any entire relation on an inhabited set. Countable choice is akin to constructive Church's thesis principle and indeed dependent choice holds in many realizability models and it is thus adopted in many constructive schools.
* Relativized dependent choice: The stronger relativized dependent choice principle is a variant of it - a schema involving an extra predicate variable. Adopting this for just bounded formulas in $$, the theory already proves the $\Sigma_1$-induction.
* $\Pi\Sigma$-$AC$: A family of sets is better controllable if it comes indexed by a function. A set $B$ is a base if all indexed families of sets $i_S\colon B\to S$ over it, have a choice function $f_S$, i.e. $\forall (x\in B). f_S(x)\in i_S(x)$. A collection of sets holding $\omega$ and its elements and which is closed by taking indexed sums and products (see dependent type) is called $\Pi\Sigma$-closed. While the axiom that all sets in the smallest $\Pi\Sigma$-closed class are a base does need some work to formulate, it is the strongest principle over $$ that holds in the type theoretical interpretation $$.
* Axiom of choice: The axiom of choice concerning functions on general sets of inhabited sets. The codomain here is the general union of sets. It implies Dependent choice. It also implies instances of $$ via Diaconescu's theorem. In turn, extensional theories with full choice broadly tend to contradict the constructive Church's rule.

Diaconescu's theorem

To highlight the strength of full Choice and its relation to matters of intentionality, one should consider the classes
:$a=\$
:$b=\$
from the proof of Diaconescu's theorem. Referring back to the introductory elaboration on the meaning of such convenient class notation, as well as to the principle of distributivity, $t\in a\leftrightarrow \big(t=0\lor (t=1\land P)\big)$. So unconditionally, $0\in a$, $1\in b$. But otherwise, the uncountable classes $a$ and $b$ are as contingent as the proposition $P$ involved in their definition. Nonetheless, the setup entails several consequences, when inspecting the provable case, starting with $P\to(a=\\land b=\)$. So $P\to a=b$ and indeed the equality is equivalent and decides $P$. As $a$ are $b$ are then sets, also $P\to \=\$. A contrapositive gives $\neg(a=b)\leftrightarrow\neg P$, which is important for the proof of the theorem. In fact, as $\neg P\to(a=\\land b=\)$ and, as $\neg(0=1)$, one finds in which way the sets are then different. One may moreover reason using the disjunctive syllogism that both $0\in b$ and $1\in a$ are each equivalent to $P$.

In the following assume a context in which $a, b$ are established to be sets, and thus subfinite sets. Then for inhabited such sets, the general axiom of choice claims existence of a function $f\colon\\to a\cup b$ with $f(z)\in z$. It is important that the elements $a,b$ of the function's domain are different than the natural numbers $0, 1$ in that a priori less is known about the former. When forming then union of the two classes, $u=0\lor u=1$ is a necessary but then also sufficient condition. Thus $a\cup b = \$ and one is dealing with functions $f$ into a set of two ''distinguishable'' values. With choice come the conjunction $f(a)\in a \land f(b)\in b$ in the codomain of the function. Using the distributivity, there arises a list of conditions on the ''possible'' function return values, a disjunction. Expanding what is then established, one finds that either both $P$ as well as the sets equality, or that the return values are different and $P$ can be rejected. The conclusion is that the choice postulate actually implies $P\lor\neg P$ whenever a Separation axiom allows for set comprehension using undecidable $P$. Consider, for example, an undecidable membership claim inside a given set.

So full choice is generally non-constructive. The issue is that propositions, as part of set comprehension used to separate and define the classes $a$ and $b$ from $\$, ramify truth values into set terms. Equality defined by the set theoretical axiom of extensionality, which itself is not related to functions, in turn couples knowledge about the predicate to information about function values. Spoken in terms function values: On the one hand, witnessing $f(a)=1$ implies $P$ and $a=b$ and this conclusion independently also applies to witnessing $f(b)=0$. On the other hand, witnessing $f(a)=0\land f(b)=1$ implies the two function arguments are not equal and this rules out $P$. There are really only three combinations, as the axiom of extensionality in the given setup makes $f(a)=1\land f(b)=0$ inconsistent. The conclusion can be summarized by the already formally derived equivalence of disjuncts $\big((1\in a)\lor(0\in b)\lor\neg(a=b)\big) \leftrightarrow (P\lor\neg P)$. So if the constructive reading of existence is to be preserved, full choice may be not adopted in the set theory, because the mere claim of function existence does not realize a particular function.

To better understand why we cannot expect to be granted a definitive (total) function, consider naive function candidates. It was noted that it is the case that $0\in a$ and $1\in b$, regardless of $P$. So without further analysis, this would seem to make
:$f = \$
a contender for a choice function. Indeed, if $P$ can be rejected, this is the only option. But in the case of provability of $P$, when $\=\$, there is extensionally only one possible function input to a choice function. So in that situation, a choice function would have type $f\colon\\to\$, for example
:$f = \$
and this would rule out the initial contender. For general $P$, the domain of a would-be choice function is not concrete but contingent on $P$ and uncountable. When considering the above functional assignment $f(a)=0$, then neither unconditionally declaring $f(b)=1$ nor $f(b)=0$ is necessarily consistent. Having identified $1$ with $\$, the two candidates described above can be represented simultaneously via the uncountable $f = \$ with the would-be natural $j = \$. In $j$, the proposition $P$ in the "if-clause" may be replaced by $a=b$. As $(P\to j=0)\land(\neg P\to j=1)$, postulating the classical $P\lor\neg P$ here would indeed imply that this is a choice function no matter which of two truth values $P$ takes. And as in the constructive case, given a ''particular'' choice function - a set holding either exactly one or exactly two pairs - one could actually infer whether $P$ or whether $\neg P$ does hold. Vice versa, the third and last candidate
:$f = \$
can be captured as part of $f = \$, where $i=\$. This is a classical choice function either way as well. Constructively, the domain and values of such $P$-dependent would-be functions will be undecidable and as such one fails to prove functional totality.
In computable interpretations, set theory axioms postulating (total) function existence lead to the requirement for recursive functions. From a function realization one can infer the branches taken by the "if-clauses" of the classical solutions, which were undecided in the interpreted theory.

Regularity implies PEM

The axiom of regularity states that for every inhabited set $s$, there ''exists'' an element $t$ in $s$, which shares no elements with $s$.
As opposed to the axiom of choice, this existence claim reaches for an element of every inhabited set, i.e. the "domain" are all inhabited sets. Its formulation does not involve a unique existence claim but instead guarantees a set with a specific property.
As the axiom correlates membership claims at different rank, the axiom also ends up implying $$:

The proof from choice above had used a particular set $\$ from above. The proof below also uses this $b$, for which it was already established that $0\in b\leftrightarrow P$.
Also recall that when Separation applies to $P$, the set $b$ is defined using the clause $u\in\$, so that any given $u\in b$ has $u=0\lor u=\$. Now let $t\in b$ be the postulated member with the empty intersection property, which in particular means $t=\\to\neg(0\in b)$. Together, one finds $(0\in b)\lor\neg(0\in b)$, which also formally decides $P$.

Arithmetic

The four Peano axioms for $0$ and $S$, characterizing $\omega$ as a model of the natural numbers in $$, have been discussed. The order "$<$" of natural numbers is captured by membership "$\in$" in this von Neumann model and this set is discrete, i.e. also equality is decidable. Indeed, also Heyting arithmetic proves
:$\vdash\forall n. \forall m. \big((n=m)\lor\neg(n=m)\big)$
The first-order theory $$ has the same non-logical axioms as Peano arithmetic.
An account of induction is given in the next paragraph.
Then, it is clarified which set theory axiom must be asserted to prove existence of the binary functions addition "$+$" and multiplication "$\times$" with their respective relation to zero and successor.

Moderate induction in ECST

The second universally quantified conjunct in the axiom of Infinity expresses mathematical induction for all $x$ in the universe of discourse, i.e. for sets. This is because sets $x$ can be read as corresponding to predicates and the consequent $\omega\subset x$ states that all $n\in\omega$ fulfill said predicate. So $$ proves induction for all predicates $\phi(n)$ involving only set-bounded quantifiers. The much stronger axiom of full mathematical induction for any predicate expressed though set theory language could also be adopted at this point in our development. That induction principle follows from full (i.e. unbounded) Separation as well as from (full) Set induction.

Note: In naming induction statements, one must take care not to conflate terminology with arithmetic theories. The first-order induction schema of natural number arithmetic claims induction for all predicates definable in the language of first-order arithmetic, namely predicates of just numbers. So to interpret the axiom schema of $$, one interprets these arithmetical formulas. One may also speak about the induction in second-order arithmetic, explicitly expressed for subsets of the naturals. The class of subsets can be taken to correspond to a richer collection of formulas than the first-order arithmetic definable ones. Typical set theories like the one discussed here are also first-order, but those theories are not arithmetics and so formulas may also quantify over the subsets of the naturals. Finally, bounded quantification in that context here means quantification over the elements of whatever is established to be a set.

Recursion

In $$, many mathematical statements can be proven per individual set, opposed to many formulas involving universal quantification, as would be possible, for example, with an induction principle for classes. With this, the set theory axioms listed so far suffice as formalized framework for a good portion of basic mathematics. That said, the constructive set theory $$ does actually not even enable primitive recursion for function definitions of what would be $h\colon(x\times\omega)\to y$. Indeed, despite having the Replacement axiom, the theory does not prove the addition function $+\colon(\omega\times\omega)\to \omega$ to be a set function. Going beyond $$ with regards to arithmetic, the axiom granting definition of set functions via iteration-step set functions must be added: For any set $y$, set $z\in y$ and $f\colon y\to y$, there must also exist a function $g\colon \omega\to y$ attained by making use of the former, namely such that $g(0)=z$ and $g(Sn)=f(g(n))$. This postulate is akin to the transfinite recursive theorem, except it is restricted to set functions and finite ordinals, i.e. there is no clause about limit ordinals. It functions as the set theoretical equivalent of a natural numbers object in category theory.
This then enables a full interpretation of Heyting arithmetic $$ in our set theory, including addition and multiplication functions.

With this, arithmetic of rational numbers $$ can then also be defined and its properties, like uniqueness and countability, be proven.
A set theory with this will also prove that, for any naturals $n$ and $m$, the function spaces
:$\to$
are sets.
(As an aside, note that, moreover, a bounded variant of this iteration schema that grants the existence of a unique such $g$, proves the existence of a transitive closure for every set with respect to $\in$.)

Now conversely, a proof of the spelled out, $$-model enabling iteration principle can be based on the collection of functions one would want to write as the union $\cup_y^$. The existence of this becomes provable when asserting that the individual function spaces on finite domains into sets $y$ form sets themselves. That principle may be written as
:$\forall(n\in\omega). \forall y.\ \ \exists h. h=y^n$

This should further motivate the adoption of an even stronger axiom of more set theoretical flavor, instead of just directly embedding arithmetic principles into our theory. This more set theoretical exponentiation axiom will, however, still not prove the full induction schema for formulas with quantifiers over sets.

Induction without Infinity

Before discussing (even classically) uncountable sets, here taking a step back to $$, note that induction schemas may be adopted without ever postulating that the collection of naturals exists as a set.
It is worth noting that in the program of predicative arithmetic, the mathematical induction schema has been criticized as possibly being impredicative, when natural numbers are defined as the object which fulfill this schema, which itself is defined in terms of all naturals.
The minimal assumptions necessary to obtain theories of natural number arithmetic are thoroughly studied in proof theory and are naturally framed as insights into first- and second-order arithmetic theories.

The classical theories starting with bounded arithmetic adopt different conservative induction schemas and may add symbols for particular functions. On the first-order side, this leads to theories between the Robinson arithmetic $$ and Peano arithmetic $$: The theory $$ does not have any induction. $$ has full mathematical induction for arithmetical formulas and has ordinal $\varepsilon_0$, meaning the theory lets one encode ordinals of weaker theories as recursive relation on just the naturals.
Many of the well studied arithmetic theories are weak regarding proof of totality for some more fast growing functions. Some of the most basic examples of arithmetics include elementary function arithmetic $$, which includes induction for just bounded arithmetical formulas, here meaning with quantifiers over finite number ranges. The theory has a proof theoretic ordinal (the least not provenly recursive well-ordering) of $\omega^3$.
The $\Sigma_1^0$-induction schema for arithmetical existential formulas allows for induction for those properties of naturals a validation of which is computable via a finite search with unbound (any, but finite) runtime. The schema is also classically equivalent to the $\Pi_1^0$-induction schema.
The relatively weak classical first-order arithmetic which adopts that schema is denoted $\mathsf_1$ and proves the primitive recursive functions total. The theory $\mathsf_1$ is $\Pi_2^0$-conservative over primitive recursive arithmetic $$.
Note that the $\Sigma_1^0$-induction is also part of the second-order reverse mathematics base system $\mathsf_0$, its other axioms being $$ plus $\Delta_1^0$-comprehension of subsets of naturals. The theory $\mathsf_0$ is $\Pi_1^1$-conservative over $\mathsf_1$. Those last mentioned arithmetic theories all have ordinal $\omega^\omega$.

Let us mention one more step beyond the $\Sigma_1^0$-induction schema. Lack of stronger induction schemas means, for example, that some infinite versions of the pigeon hole principle are unprovable. One relatively weak one being the Ramsey theorem type claim here expressed as follows: For any $m>0$ and coding of a coloring map $f$, associating each $n\in\omega$ with a color $\$, it is not the case that for every color c there exists a threshold input number $n_c$ beyond which $c$ is not ever the mappings return value anymore. Higher indirection as in induction for mere existential statements is needed to rewrite such a negation and prove it. Namely to rewrite it as the negation of the existence of a joint threshold number, depending on all the ''hypothetical'' $n_c$'s, beyond which the function would still have to attain some color value. More specifically, the strength of the required bounding principle is strictly between the induction schema in $\mathsf_1^0$ and $\mathsf_2^0$.
For properties in terms of return values of functions on finite domains, brute force verification through checking all possible inputs has computational overhead which is larger the larger the size of the domain, but always finite. Acceptance of an induction schema as in $\mathsf_2^0$ validates the former so called infinite pigeon hole principle, which concerns unbounded domains, and so is about mappings with infinitely many inputs. In the classical context, this claim about coloring may be phrased positively, in terms of sets, as saying that there always exists at least one return value $k$ such that, in effect, for some infinite domain $K\subset\omega$ it holds that $\forall(n\in K). f(n) = k$. In words, when $f$ provides infinite enumerated assignments, each being of one of $m$ different possible colors, then a particular $k$ coloring infinitely many numbers is claimed to exist and that the set can be specified. When read constructively, one would want $k$ to be concretely specifiable.

Higher-order classical arithmetics with low complexity comprehension are a relevant reference point for weaker set theories insofar as their language does not merely express arithmetical sets, while all sets of naturals particular such theories prove to exist are just computable sets. Constructive reverse mathematics, which lacks double negation elimination for undecidable sentences, exists as a field but is less developed than its classical counterpart.

Exponentiation

Classical $$ without the Powerset axiom is still consistent with all existing sets of reals being subcountable, and there even countable. Possible choice principles were discussed, a weakened form of the Separation schema was already adopted, and more of the standard $$ axioms shall be weakened for a more predicative and constructive theory. The first one of those is the Powerset axiom, which is adopted in the form of the space of characteristic functions, itself tied to exactly the decidable subclasses. So consider the axiom $$.

The formulation here uses the convenient notation for function spaces. Otherwise the axiom is lengthier, characterizing $h$ using bounded quantifiers in the total function predicate.
In words, the axiom says that given two sets $x, y$, the class $y^x$ of all functions is, in fact, also a set.
This is certainly required, for example, to formalize the object map of an internal hom-functor like $(,-)$.

Existence statements like Exponentiation, i.e. function spaces being sets, enable the derivation of more sets via bounded Separation. Adopting the axiom, quantification $\forall f$ over the elements of certain classes of functions only ranges over a set, also when such function spaces are even classically uncountable. E.g. the collection of all functions $f\colon\omega\to 2$ where $2=\$, i.e. the set $2^$ of points underlying the Cantor space, is uncountable, by Cantor's diagonal argument, and can at best be taken to be a subcountable set. (In this section and beyond, the symbol for the semiring of natural numbers in expressions like $y^$ is used, or written $\omega\to y$, just to avoid conflation of cardinal- with ordinal exponentiation.) Roughly, classically uncountable sets tend to not have computably decidable equality.

On countable sets

Enumerable forms of the pigeon hole principle can now be proven, e.g. that on a finitely enumerable set, every injection is also a surjection. At last, all finitely enumerable sets are finite. The finitely enumerable union of a family of subfinite resp. subcountable sets is itself subfinite resp. subcountable.

For any countable family of counting functions together with their ranges, the theory proves the union of those ranges to be countable. Recall that not even classical $$ (without countable choice) proves a countable union of countable sets to be countable, as this requires infinitely many existential instantiations of functions. With Exponentiation, the union of all finite sequences over a countable set is now a countable set.

With function spaces with the finite von Neumann ordinals as domains, we can model $$ as discussed and can thus encode ordinals in the arithmetic. One then furthermore obtains the ordinal-exponentiated number $\omega^\omega$ as a set, which may be characterized as $\cup_\omega^n$. Relatedly, the set theory then also proves the existence of any primitive recursive function on the naturals $\omega$, as set functions in the uncountable set $\omega\to\omega$.

As far as comprehension goes, the dependent or indexed products $\Pi_\,y_i$ are now sets. The theory now proves the collection of all the countable subsets of any set (the collection is a subclass of the powerclass) to be a set.

The class of subsets of a set

The characterization of the class $_x$ of all subsets of a set $x$ involves unbounded universal quantification, namely $\forall u. \left(u\subset x\leftrightarrow u\in _x\right)$. Here $\subset$ has been defined in terms of the membership predicate $\in$ above. So in a mathematical set theory framework, the power class is defined not in a bottom-up construction from its constituents (like an algorithm on a list, that e.g. maps $\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. If $_x$ is a set, that defining quantification even ranges over $_x$, which makes the axiom of powerset impredicative. The statement $y=_x$ itself is $\Pi_1$.

The richness of the powerclass in a theory without excluded middle can best be understood by considering small classically finite sets. For any proposition $P$, the class $\\subset\$ equals $0$ when $P$ can be rejected and $1$ (i.e. $\$) when $P$ can be proven, but $P$ may also not be decidable at all. Consider three different undecidable proposition, none of which provenly imply another. They can ben used to define three subclasses of the singleton $\$, none of which are provenly the same. In this view, the powerclass $_1$ of the singleton, usually denoted by $\Omega$, is called the truth value algebra and does not necessarily provenly have only two elements.
The set $2^x$ of $\$-valued functions on a set $x$ injects into the function space $^x$ and corresponds to just its decidable subsets.

It has been pointed out that the empty set $0$ and the set $1$ itself are of course two subsets of $1$. Whether also $_1\subset \$ is true in a theory is contingent on a simple disjunction:
:$\big(\forall x. x\subset 1 \to(0\in x\lor 0\notin x)\big)\to _1\subset \$.
So assuming $$ for just bounded formulas, predicative Separation then lets one demonstrate that the powerclass $_1$ is a set.
With exponentiation, $_1$ being a set already implies Powerset for sets in general. The proof is via replacement for the association of $f\in^x$ to $\\in_x$, and an argument why all subsets are covered.
So in this context, also full Choice proves Powerset.
Moreover, with bounded excluded middle, $_x$ is in bijection with $2^x$. See also $$.

Full Separation is equivalent to just assuming that each individual subclass of $1$ is a set. Assuming full Separation, both full Choice and Regularity prove $$.

Relatedly, assuming $$ in this theory, Set induction becomes equivalent to Regularity and Replacement becomes capable of proving full Separation.

Metalogic

While the theory $+$ does not exceed the consistency strength of Heyting arithmetic, adding Excluded Middle gives a theory proving the same theorems as classical $$ minus Regularity!
Thus, adding Regularity as well as either $$ or full Separation to $+$ gives full classical $$.
Adding full Choice and full Separation gives $$ minus Regularity.

So this would thus lead to a theory beyond the strength of typical type theory.

Category and type theoretic notions

So in this context with Exponentiation, function spaces are more accessible than classes of subsets, as is the case with exponential objects resp. subobjects in category theory.
In category theoretical terms, the theory $+$ essentially corresponds to 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 $$ is of course a model of these weaker theories, but locally Cartesian closed pretoposes have been defined that e.g. interpret theories with Exponentiation but reject full Separation and Powerset.
A form of $$ corresponds to any subobject having a complement, in which case we call the topos Boolean. Diaconescu's theorem in its original topos form says that this hold iff any coequalizer of two nonintersecting monomorphisms has a section. The latter is a formulation of choice. Barr's theorem states that any topos admits a surjection from a Boolean topos onto it, relating to classical statements being provable intuitionistically.

In type theory, the expression "$x\to y$" exists on its own and denotes function spaces, a primitive notion. These types (or, in set theory, classes or sets) naturally appear, for example, as the type of the currying bijection between $(z\times x)\to y$ and $z\to y^x$, an adjunction.
A typical type theory with general programming capability - and certainly those that can model $$, which is considered a constructive set theory - will have a type of integers and function spaces representing $\to$, and as such also include types that are not countable. This is just to say, or implies, that among the function terms $f\colon \to(\to)$, none have the property of being a bijection.

Constructive set theories are also studied in the context of applicative axioms.

Analysis

In this section the strength of $+$ is elaborated on.
For context, possible further principles are mentioned, which are not necessarily classical and also not generally considered constructive.
Here a general warning is in order: When reading proposition equivalence claims in the computable context, one shall always be aware which ''choice'', ''induction'' and ''comprehension'' principles are silently assumed.
See also the related Constructive analysis and Computable analysis.

Cauchy sequences

Exponentiation implies recursion principles and so in $+$, one can comfortably reason about sequences $s\colon\omega\to$, their regularity properties such as $, s_n-s_m, \le \tfrac+\tfrac$, or about shrinking intervals in $\omega\to(\times)$. So this enables speaking of Cauchy sequences and their arithmetic.

Cauchy reals

Any Cauchy real number is a collection of sequences, i.e. subset of a set of functions on $\omega$. 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. The prefix "pseudo" here highlights that the order will, in any case, constructively not always be decidable.

Towards the Dedekind reals

As in the classical theory, Dedekind cuts are characterized using subsets of algebraic structures such as $$: The properties of being 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 exhibiting these properties, is the representation of $\sqrt 2$ given by
:$\big\langle\,\,\\big\rangle\,\ \in\,\ \times$
(Depending on the convention for cuts, either of the two parts or neither, like here, may makes use of the sign $\le$.)

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 $\^$ does not grant $$ to be a set, and so neither is the class of all subsets of $$ 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 and this is discussed further below in the section on Binary refinement.
In a context without $$ or Powerset, countable choice into finite sets is commonly assumed to prove the uncountability of the Dedekind reals.

Whether Cauchy or Dedekind reals, fewer statements about the arithmetic of the reals are decidable, compared to the classical theory.

Constructive schools

Non-constructive claims valuable in the study of constructive analysis are commonly formulated as concerning all binary sequences, i.e. functions $f\colon\omega\to\$. That is to say claims which are now set bound via "$\forall (f \in 2^)$".

A most prominent example is the limited principle of omniscience $$, postulating a disjunctive property, like $$ at the level of $\Pi_1^0$-sentences or functions. (Example functions can be constructed in raw $$ such that, if $$ is consistent, the competing disjuncts are $$-unprovable.) The principle is independent of e.g. $$ introduced below. In that constructive set theory, $$ implies its "weaker" version, itself implying the "lesser" version, denoted $$ and $$. $$ moreover implies Markov's principle $$, a form of proof by contradiction motivated by (unbound memory capacity) computable search, as well as the $\Pi_1^0$-version of the fan theorem. Mention of such principles holding for $\Pi_1^0$-sentences generally hint at equivalent formulations in terms of sequences, deciding apartness of reals. In a constructive analysis context with countable choice, $$ is e.g. equivalent to the claim that every real is either rational or irrational - again without the requirement to witness either disjunct. The three omniscience principles are each equivalent to theorems of the apartness, equality or order of two reals in this way.

Here a list of some propositions employed in theories of constructive analysis that are not provable using just base intuitionistic logic.
For example, see $$ or even the anti-classical constructive Church's thesis principle $$ for number-theoretic functions as a postulate in the theory, or some of its consequences on the recursive mathematics side (variously called $$, $$ or $$). This is discussed below.
On another end, there are Kripke's schema (turning all subclasses of $\omega$ countable), bar induction, the decidable fan theorem $_\Delta$ (which contradicts strong forms of Church's thesis), or even Brouwer's anti-classical continuity principle determining functions on unending sequences through finite initial segments, on the Brouwerian intuitionist side ($$). Both mentioned schools contradict $$, so that choosing to adopt certain of its laws makes the theory inconsistent with theorems in classical analysis. Those two schools are moreover not consistent with one another.

Infinite trees

Through the relation between computability and the arithmetical hierarchy, insights in this classical study are also revealing for constructive considerations. A basic insight of reverse mathematics concerns computable infinite finitely branching binary trees. Such a tree may e.g. be encoded as an infinite set of finite sets
:$T\,\subset\,\cup_\^$,
with decidable membership, and those trees then provenly contain elements of arbitrary big finite size. The so called Weak KÅ‘nigs lemma $$ states: For such $T$, there always exists an infinite path in $\omega\to\$, i.e. an infinite sequence such that all its initial segments are part of the tree. In reverse mathematics, the second-order arithmetic $\mathsf_0$ does not prove $$. To understand this, note that there are computable trees $K$ for which no ''computable'' such path through it exists. To prove this, one enumerates the partial computable sequences and then diagonalizes all total computable sequences in one partial computable sequences $d$. One can then roll out a certain tree $K$, one exactly compatible with the still possible values of $d$ everywhere, which by construction is incompatible with any total computable path.

In $$, the principle $$ implies the non-constructive lesser limited principle of omniscience $$. In a more conservative context, they are equivalent assuming $\Pi_1^0$-$_$ (a very weak countable choice). It is also equivalent to the Brouwer fixed point theorem and other theorems regarding values of continuous functions on the reals. The fixed point theorem in turn implies the intermediate value theorem, but be aware that the classical theorems can translate to different variants when expressed in a constructive context.

The $$ concerns ''infinite'' graphs and so its contrapositive gives a condition for finiteness. Again to connect to analysis, over the classical arithmetic theory $\mathsf_0$, the claim of $$ is for example equivalent to the Borel compactness regarding finite subcovers of the real unit interval. A closely related existence claim involving finite sequences in an infinite context is the decidable fan theorem $_\Delta$. Over $\mathsf_0$, they are actually equivalent. In $$ those are distinct, but, after again assuming some choice, here then $$ implies $_\Delta$.

Restricting function spaces

In the following short remark ''function'' and claims made about them is again meant in the sense of computability theory: The μ operator enables all partial general recursive functions (or programs, in the sense that they are Turing computable), including ones e.g. non-primitive recursive but $$-total, such as the Ackermann function. The definition of the operator involves predicates over the naturals and so the theoretical analysis of functions and their totality depends on the formal framework and proof calculus at hand. This is highlighted because of the concern with axioms in theories other than arithmetic.

The predicate expressing a program to be total is famously computably undecidable.
An anti-classical constructive Church's principle $$, expressed in the language of the theory, concerns those set functions and it postulates that they corresponds to computable programs. The natural numbers which are thought of as indices (for the computable functions which are total) in computability theory are $\Pi_2^0$ in the arithmetical hierarchy. Which is to say it is still a subclass of the naturals and so this is, when put in relation to some classical function spaces, a conceptually small class. In this sense, adopting the $$ postulate makes $\omega\to\omega$ into a "sparse" set, as viewed from classical set theory. Subcountability of sets can also be postulated independently.
$$ is still consistent with some choice, but it contradicts classically valid principles such as $$ and $_\Delta$, which are amongst the weakest often discussed principles.

Induction

Mathematical induction

In set language, induction principles can read $\mathrm(A)\to \omega\subset A$, with the antecedent $\mathrm(A)$ defined as further above, and with $\omega\subset A$ meaning $\forall (n\in\omega). n\in A$ where $\omega$ is always the set of naturals. Via the strong axiom of Infinity and bounded Separation, the validity of induction for bounded definitions was already established.

At this point it is instructive to recall how set comprehension was encoding statements in predicate logic. For an example, given set $y$, let $P(n)$ denote the existential statement that a certain function space set exist, $\exists x. x=y^$. Here the existential quantifier is not merely one over natural numbers or bounded by any other set. Now a proposition like the exponentiation claim $\forall(n\in\omega). P(n)$ and the subclass claim $\omega\subset\$, are just two ways of formulating the same desired claim, namely an $n$-indexed conjunction of existential propositions where $n$ spans over the set of all naturals. The second form is expressed using class notation involving a subclass comprehension that may not constitute a set, in which case many set axioms won't apply, so that establishing it as a theorem may not be possible. A set theory with just ''bounded'' Separation can thus also be strengthened by adopting arithmetical induction schemas for predicates beyond just the bounded ones.

The iteration principle for set functions mentioned in the section dedicated to arithmetic is also implied by the full induction schema over one's structure modeling the naturals (e.g. $\omega$). So for that theorem, granting a model of Heyting arithmetic, it represents an alternative to Exponentiation.
The schema is often formulated in terms of predicates as follows:

Here the 0 denotes $\$ as above, 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 full induction schema is implied by the full Separation schema. As elaborated in the section on induction from infinity, here formulas in schemas are to be understood as formulas in first-order set theory.
And as stated in the section on Choice, induction principles are also implied by various forms of choice principles.

Set Induction

Full Set Induction in $$ proves induction in transitive sets and so transitive sets or transitive sets (ordinals). This enables ordinal arithmetic.
In particular, it proves full mathematical induction. Replacement is not required to prove induction over the set of naturals, but it is for their arithmetic modeled within the set theory.

It then reads as follows:

Here $\forall(z\in \). \phi(z)$ holds trivially and so this covers to the "bottom case" $\phi(\)$ 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 allows definitions of class functions by transfinite recursion. The study of the various principles that grant set definitions by induction, i.e. inductive definitions, is a main topic in the context of constructive set theory and their comparatively weak strengths. This also holds for their counterparts in type theory.

The axiom of regularity is a single statement with universal quantifier over sets and not a schema. As show, it implies $$, and so is non-constructive. Now for $\phi$ taken to be the negation of some predicate $\neg S$ and writing $\Sigma$ for the class $\$, induction reads
:$\forall(x\in\Sigma).x\cap \Sigma\neq\\,\to\,\Sigma=\$
Via the contrapositive, set induction implies all instances of regularity but only with double-negated existence in the conclusion. In the other direction, given enough transitive sets, regularity implies each instance of set induction.

Metalogic

This now covers variants of all of the eight Zermelo–Fraenkel 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, in its classical form, full Separation, Powerset as well as Regularity. Adding $$ at this point would already give $$. Replacement and Exponentiation can be further strengthened without losing a type theoretical interpretation and in a way that is not going beyond $$. Those two alterations are discussed next.

Like the axiom of regularity, set induction restricts the possible models of the membership relation "$\in$" and thus that of a set theory, as was the motivation for the principle in the 20's.
The added proof-theoretical strength attained with Induction in the constructive context is significant, even if dropping Regularity in the context of $$ does not reduce the proof-theoretical strength.
Aczel was also one of the main developers or Non-well-founded set theory, which rejects this last axiom.

Strong Collection

Having discussed all the weakened form of axioms of $$, one can reflect upon the strength of the axiom of replacement, also in the context of the classical set theory. For any set $y$ and any natural $n$, there exists the product $y^n$ recursively given by $y^\times y$, which have ever deeper rank. Induction for unbound predicates proves that these sets exist for all of the infinitely many naturals. Replacement "for $n\mapsto y^n$" now moreover states that this infinite class of products can be turned into the infinite set, $\$. This is also not a subset of any previously established set.

Going beyond those axioms also seen in Myhill's typed approach, consider the discussed constructive theory with Exponentiation and Induction, but now strengthened by the collection schema. This is an alternative to the Replacement schema and indeed supersedes it, due to not requiring the binary relation definition to be functional, but possibly multi-valued. The principle may be used in the constructive study of larger sets beyond the everyday need of analysis.

The axiom concerns a property for relations, giving rise to a somewhat repetitive format in its first-order formulation. The antecedent states that one considers relation $\phi$ between sets $x$ and $y$ that are total over a certain domain set $a$, that is, $\phi$ has at least one "image value" $y$ for every element $x$ in the domain. This is more general than an inhabitance condition $x\in y$ in a choice axiom, but also more general than the condition of Replacement, which demands unique existence $\exists!y$. In the consequent, firstly, the axioms states that then there exists a set $b$ which contains at least one "image" value $y$ under $\phi$, for every element of the domain. Secondly, in this axioms formulation it then moreover states that only such images $y$ are elements of that new codomain set $b$. It is guaranteeing that $b$ does not overshoot the codomain of $\phi$ and thus the axiom is also expressing some power akin to a Separation procedure. The axiom may be expressed as saying that for every total relation, there exists a set $b$ such that the relation is total in both directions.

Metalogic

This theory without $$, without unbounded separation and without "naive" Power set enjoys various nice properties. For example, as opposed to $$ with its subset collection schema below, it has the existence property.

Constructive Zermelo–Fraenkel

Subset Collection

One may approach Power set further without losing a type theoretical interpretation.
The theory known as $$ is the axioms above 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:

An alternative that is not a schema is elaborated on below.

Fullness

For given $a$ and $b$, let $_$ be the class of all total relations between $a$ and $b$. This class is given as
:$r \in _ \leftrightarrow \Big(\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)\Big)$
As opposed to the function definition, there is no unique existence quantifier in $\exists!(y \in b)$. The class $_$ represents the space of "non-unique-valued functions" or "multivalued functions" from $a$ to $b$, but as set of individual pairs with right projection in $b$, and only those.

One does not postulate $_$ to be a set, since with Replacement one can use this collection of relations between a set $a$ and the finite $b=\$, i.e. the "bi-valued functions on $a$", to extract the set $_a$ of all its subsets. In other words $_$ being a set would imply the Powerset axiom.

Over $+\text$, there is a single, somewhat clearer alternative axiom to the Subset Collection schema. It postulates the existence of a sufficiently large ''set'' $_$ of total relations between $a$ and $b$.

This says that for any two sets $a$ and $b$, there exists a set $_\subset _$ which among its members inhabits a still total relation $s\in _$ for any given total relation $r\in _$.

On a given domain $a$, the functions are exactly the sparsest total relations, namely the unique valued ones. Therefore, the axiom implies that there is a set such that all functions are in it. In this way, Fullness implies Exponentiation.
The Fullness axiom is in turn also implied by the so-called Presentation Axiom about sections, which can also be formulated category theoretically.

Binary refinement

The so called binary refinement axiom says that for any $a$ there exists a set $_a\subset_a$ such that for any covering $a=x\cup y$, the set $_a$ holds two subsets $c\subset x$ and $d\subset y$ that also do this covering job, $a=c\cup d$. It is a weakest form of the powerset axiom and at the core of some important mathematical proofs.
Fullness for relations between the set $a$ and the finite $\$ implies that this is indeed possible.

Taking another step back, $$ plus Recursion and plus Binary refinement already proves that there exists an Archimedean, Dedekind complete pseudo-ordered field. That set theory also proves that the class of left Dedekind cuts is a set, not requiring Induction or Collection. And it moreover proves that function spaces into discrete sets are sets (there e.g. $\omega\to\omega$), without assuming $$. Already over the weak theory $$ (which is to say without Infinity) does binary refinement prove that function spaces into discrete sets are sets, and therefore e.g. the existence of all characteristic function spaces $\^a$.

Unprovable claims

The bounded notion of a transitive sets of transitive sets is a good way to define ordinals and enables induction on ordinals. With this, in $$, assuming that membership of $0$ is decidable in all successor ordinals $S\alpha$ proves $$ for bounded formulas. Also, neither linearity of ordinals, nor existence of power sets of finite sets are derivable in this theory, as assuming either implies Power set. The theory $$ does not prove that all function spaces formed from sets in the constructible universe $L$ are sets ''inside'' $L$, and this holds even when assuming Powerset instead of the weaker Exponentiation axiom. So such theories do not prove $L$ to be a model of $$.

Metalogic

This theory has the numerical existence property and the disjunctive property, but there are concessions: $$ lacks the existence property due to the Subset Schema or Fullness axiom. The existence property is not lacking when the weaker Exponentiation or the stronger but impredicative Powerset axiom axiom is adopted instead. The latter is in general lacking a constructive interpretation.

In 1977 Aczel showed that $$ 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 $$ 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. Conversely, $$ interprets $$.
All statements validated in the subcountable model of the set theory can be proven exactly via $$ plus the choice principle $\Pi\Sigma$-$AC$, stated further above.
Exhibiting a type theoretical model, the theory $$ has modest proof theoretic strength, the Bachmann–Howard ordinal (see also $$). Those theories with choice have the existence property for a broad class of sets in common mathematics.
Martin-Löf type theories with additional induction principles validate corresponding set theoretical axioms.

Breaking with ZF

One may further add the anti-classical claim that all sets are subcountable, as is the case in the type theoretical model, as an axiom. By Infinity and Exponentiation, $\omega\to\omega$ is an uncountable set, while the class $_\omega$ or even $_1$ is then provenly not a set, by Cantor's diagonal argument. So this theory then logically rejects Powerset and $$.

In 1989 Ingrid Lindström showed that non-well-founded sets obtained by replacing Set Induction, the constructive equivalent of the axiom of regularity (a.k.a. axiom of foundation), in $$ with Aczel's anti-foundation axiom ($$) can also be interpreted in Martin-Löf type theory.Lindström, Ingrid: 1989
A construction of non-well-founded sets within Martin-Löf type theory
Journal of Symbolic Logic 54: 57–64. The theory $$ may be studied by also adding back the $\omega$-induction schema or relativized dependent choice, as well as the assertion that every set is member of a transitive set.

Intuitionistic Zermelo–Fraenkel

The theory $$ is $$ adopting both the standard Separation as well as Power set and, as in $$, one conventionally formulates the theory with Collection below. As such, $$ can be seen as the most straight forward variant of $$ without $$.
So as noted, in $$, in place of Replacement, one may use the

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$.
In classical $$, the Collection schema implies the Axiom schema of replacement. When making use of Powerset (and only then), they can be shown to be classically equivalent.

While $$ 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, distancing the theory from the bottom-up constructive perspective. With this general Separation, it is easy to define ''sets'' $\$ with undecidable membership, namely by making use of undecidable predicates defined on a set.
Further, the power set axiom implies the existence of a set of truth values. In the presence of excluded middle, this set has two elements. In the absence of it, the set of truth values is also considered impredicative. The axioms of $$ are strong enough so that full $$ is already implied by $$ for bounded formulas, or in fact by $\forall x. \big(0\in x\lor 0\notin x\big)$.

Metalogic

As implied above, the subcountability property cannot be adopted for all sets, given the theory proves $_\omega$ to be a set.
The theory has many of the nice numerical existence properties and is e.g. consistent with Church's thesis principle as well as with $\omega\to\omega$ being subcountable. It also has the disjunctive property.

$$ with Replacement instead of Collection has the general existence property, even when adopting relativized dependent choice on top of it all. but $$ as formulated does not. The combination of schemas including full separation spoils it.

Even without $$, the proof theoretic strength of $$ equals that of $$.

Intuitionistic Z

Again on the weaker end, as with its historical counterpart Zermelo set theory, one may denote by $$ the intuitionistic theory set up like $$ 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 $$.
The theory has not only Separation but also Collection restricted to $\Delta_0$, i.e. it is similar to $$ 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. Of course, weaker versions of $$ are obtained by restricting the induction schema to narrower classes of formulas, say $\Sigma_1$.

Sorted theories

Constructive set theory

As he presented it, Myhill's system $$ is a theory using constructive first-order logic with identity and three sorts, namely
sets, natural numbers, functions. Its axioms are:

* 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 from classical set theory, requiring that any quantifications be bounded to another set, as discussed.
* A form of the Axiom of Infinity asserting that the collection of natural numbers (for which he introduces a constant $\omega$) 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.

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.

One can roughly identify the strength of this theory with a constructive subtheories of $$ when comparing with the previous sections.

And finally the theory adopts
* An Axiom of dependent choice, which is much weaker than the usual Axiom of choice.

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.

A lot of analysis and module theory has been developed in this context.

Category theories

Not all formal logic theories of sets need to axiomize the binary membership predicate "$\in$" directly. A theory like the Elementary Theory of the Categories Of Set ($$), e.g. capturing pairs of composable mappings between objects, can also be expressed with a constructive background logic. Category theory can be set up as a theory of arrows and objects, although first-order axiomatizations only in terms of arrows are possible.

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

Good models of constructive set theories in category theory are the pretoposes mentioned in the Exponentiation section. For some good set theory, this may require enough projectives, an axiom about surjective "presentations" of set, implying Countable Dependent Choice.

See also

* Axiom schema of predicative separation
* Constructive mathematics
* Constructive analysis
* Constructive Church's thesis rule and principle
* Computable set
* Existence Property
* Diaconescu's theorem
* Epsilon-induction
* Hereditarily finite set
* Heyting arithmetic
* Impredicativity
* Intuitionistic type theory
* Law of excluded middle
* Ordinal analysis
* Subcountability

References

Further reading

*
* 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

{{DEFAULTSORT:Constructive Set Theory
Constructivism (mathematics)
Intuitionism
Systems of set theory