Constructive set theory is an approach to mathematical constructivism following the program of axiomatic set theory. The same first-order language with "${\displaystyle =}$" and "${\displaystyle \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 (${\displaystyle {\mathrm {PEM} ))$), 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 the principle of excluded middle ${\displaystyle {\mathrm {PEM} ))$, i.e. that the disjunction ${\displaystyle \phi \lor \neg \phi }$ automatically holds for all propositions ${\displaystyle \phi }$. As a rule, to prove the excluded middle for a proposition ${\displaystyle P}$, i.e. to prove the particular disjunction ${\displaystyle P\lor \neg P}$, either ${\displaystyle P}$ or ${\displaystyle \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 ${\displaystyle Q(x)}$ for ${\displaystyle x}$ in a domain ${\displaystyle X}$ is said to be decidable when the more intricate statement ${\displaystyle \forall (x\in X).{\big (}Q(x)\lor \neg Q(x){\big )))$ is provable. Non-constructive axioms may enable proofs that formally decide such ${\displaystyle P}$ (and/or ${\displaystyle Q}$) in the sense that they prove excluded middle for ${\displaystyle 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, axiomatic theories deemed constructive tend to not permit many classical proofs of statements involving properties that are provenly computationally undecidable. Similarly, a counter-example existence claim ${\displaystyle \exists (x\in X).\neg R(x)}$ is generally constructively stronger than a rejection claim ${\displaystyle \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. In turn the theorem formulations regarding finite objects tends to not differ from their classical counterparts. Given a model of all natural 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 ${\displaystyle \neg P}$ of the valid law of noncontradiction and using a valid De Morgan's law, already minimal logic does prove ${\displaystyle \neg \neg (P\lor \neg P)}$ for any given proposition ${\displaystyle 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 ${\displaystyle 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 ${\displaystyle {\mathrm {PEM} ))$ 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 ${\displaystyle (\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, and so one may consider a more general so-called strong existence property that is harder to come by, as will be discussed. A theory has this property if the following can be established: For any property ${\displaystyle \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 ${\displaystyle \psi }$ that uniquely describes such a set instance. More formally, for any predicate ${\displaystyle \phi }$ there is a predicate ${\displaystyle \psi }$ so that

${\displaystyle {\mathsf {T))\vdash \exists x.\phi (x)\implies {\mathsf {T))\vdash \exists !x.\phi (x)\land \psi (x)}$

The role analogous to that of realized numerals in arithmetic is played here 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 so as to exhibit the strong existence property. Zermelo–Fraenkel set theory ${\displaystyle {\mathsf {ZF))}$ with the constructible universe postulate, ${\displaystyle {\mathsf {ZF))+({\mathrm {V} }={\mathrm {L} })}$, or ${\displaystyle {\mathsf {ZF))}$ with sets all taken to be ordinal-definable, ${\displaystyle {\mathsf {ZF))+({\mathrm {V} }={\mathrm {OD} })}$, do have the existence property. For contrast, consider the theory ${\displaystyle {\mathsf {ZFC))}$ given by ${\displaystyle {\mathsf {ZF))}$ 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 ${\displaystyle W\subset {\mathbb {R} }\times {\mathbb {R} ))$ that establish the well-ordering of ${\displaystyle {\mathbb {R} ))$ formally provably exist (i.e. the theory claims the existence of a least element for all subsets of ${\displaystyle {\mathbb {R} ))$ with respect to those relations). This is despite that fact that definability of such an ordering is known to be independent of ${\displaystyle {\mathsf {ZFC))}$. The latter implies that for no particular formula ${\displaystyle \psi }$ in the language of the theory does the theory prove that the corresponding set is a well-ordering relation of the reals. So ${\displaystyle {\mathsf {ZFC))}$ formally proves the existence of a subset ${\displaystyle W\subset {\mathbb {R} }\times {\mathbb {R} ))$ with the property of being a well-ordering relation, but at the same time no particular set ${\displaystyle 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 ${\displaystyle {\mathsf {T))}$ exhibiting the following meta-theoretical property: For an instance from some collection of formulas, here captured via ${\displaystyle \phi }$ and ${\displaystyle \psi }$, one established the existence of a numeral constant ${\displaystyle e}$ so that ${\displaystyle {\mathsf {T))\vdash \phi \implies {\mathsf {T))\vdash \psi (e)}$. When adopting such a schema as an inference rule and nothing new can be proven, one says the theory ${\displaystyle {\mathsf {T))}$ is closed under that rule. Adjoining excluded middle ${\displaystyle {\mathrm {PEM} ))$ to ${\displaystyle {\mathsf {T))}$, the new theory may then prove new, strictly classical statements for ${\displaystyle \phi }$ and this may spoil the meta-theoretical property that was previously established for ${\displaystyle {\mathsf {T))}$. One may instead consider adjoining the rule corresponding to the meta-theoretical property as an implication to ${\displaystyle {\mathsf {T))}$, as a schema or in quantified form. That is to say, to postulate that any such ${\displaystyle \phi }$ implies ${\displaystyle \exists (e\in {\mathbb {N} })}$ such that ${\displaystyle \psi (e)}$ holds, where the bound ${\displaystyle 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 ${\displaystyle {\mathrm {PEM} ))$. For example, Church's rule is an admissible rule in Heyting arithmetic ${\displaystyle {\mathsf {HA))}$ and the corresponding Church's thesis principle may be adopted, but the same is not possible in ${\displaystyle {\mathsf {HA))+{\mathrm {PEM} ))$, also known as Peano arithmetic ${\displaystyle {\mathsf {PA))}$.

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

${\displaystyle \forall (f\in {\mathbb {N} }^{\mathbb {N} }).\exists (e\in {\mathbb {N} }).{\Big (}\forall (n\in {\mathbb {N} }).\exists (w\in {\mathbb {N} }).T(e,n,w)\land U(w,f(n)){\Big )))$

Kleene's T predicate together with the result extraction expresses that any input number ${\displaystyle n}$ being mapped to the number ${\displaystyle f(n)}$ is, through ${\displaystyle w}$, witnessed to be a computable mapping. Here ${\displaystyle {\mathbb {N} ))$ now denotes a set theory model of the standard natural numbers and ${\displaystyle e}$ is an index with respect to a fixed program enumeration. Stronger variants have been used, which extend this principle to functions ${\displaystyle f\in {\mathbb {N} }^{X))$ defined on domains ${\displaystyle X\subset {\mathbb {N} ))$ of low complexity. The principle rejects decidability for the predicate ${\displaystyle Q(e)}$ defined as ${\displaystyle \exists (w\in {\mathbb {N} }).T(e,e,w)}$, expressing that ${\displaystyle 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 ${\displaystyle 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 ${\displaystyle {\mathsf {RCA))_{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 ${\displaystyle {\mathbb {N} }^{\mathbb {N} ))$ holds also other functions than the computable ones. For example there is a proof in ${\displaystyle {\mathsf {ZF))}$ 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 (${\displaystyle {\mathbb {N} }^{\mathbb {N} ))$) as an axiom in a constructive theory, the "smallness" (in classical terms) of this collection, in some set theoretical realizations, is then already captured by the theory itself. A constructive theory may also adopt neither classical nor anti-classical axioms and so stay agnostic towards either possibility.

Constructive principles already prove ${\displaystyle \forall (x\in X).\neg \neg {\big (}Q(x)\lor \neg Q(x){\big )))$ and so for any given element ${\displaystyle x}$ of ${\displaystyle X}$, the corresponding excluded middle statement for the proposition cannot be negated. Indeed, for any given ${\displaystyle x}$, by noncontradiction it is impossible to rule out ${\displaystyle Q(x)}$ and rule out its negation both at once. But a theory may in some instances also permit the rejection claim ${\displaystyle \neg \forall (x\in X).{\big (}Q(x)\lor \neg Q(x){\big )))$. Adopting this does not necessitate providing a particular ${\displaystyle t\in X}$ witnessing the failure of excluded middle for the particular proposition ${\displaystyle Q(t)}$, i.e. witnessing the inconsistent ${\displaystyle \neg {\big (}Q(t)\lor \neg Q(t){\big )))$. One may reject the possibility of decidability of some predicate ${\displaystyle Q(x)}$ on an infinite domain ${\displaystyle X}$ without making any existence claim in ${\displaystyle 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 ${\displaystyle Q(x)}$ states that a sequence ${\displaystyle 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 "${\displaystyle {\mathsf {CST))}$") begun with John Myhill's work on the theories also called ${\displaystyle {\mathsf {IZF))}$ and ${\displaystyle {\mathsf {CST))}$.^[1] In 1973, he had proposed the former as a first-order set theory based on intuitionistic logic, taking the most common foundation ${\displaystyle {\mathsf {ZFC))}$ 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 ${\displaystyle {\mathsf {ZFC))}$ axioms which are equivalent in the classical setting are inequivalent in the constructive setting, and some forms imply ${\displaystyle {\mathrm {PEM} ))$, as will be demonstrated. In those cases, the intuitionistically weaker formulations were consequently adopted. The far more conservative system ${\displaystyle {\mathsf {CST))}$ 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 ${\displaystyle {\mathsf {ZF))}$, leading up to Peter Aczel's well studied ${\displaystyle {\mathsf {CZF))}$,^[2] and beyond. Many modern results trace back to Rathjen and his students. ${\displaystyle {\mathsf {CZF))}$ is also characterized by the two features present also in Myhill's theory: On the one hand, it is using the Predicative Separation instead of the full, unbounded Separation schema, 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 ${\displaystyle {\mathrm {PEM} ))$ to a theory even weaker than ${\displaystyle {\mathsf {CZF))}$ recovers ${\displaystyle {\mathsf {ZF))}$, as detailed below.^[3] The system, which has come to be known as Intuitionistic Zermelo–Fraenkel set theory (${\displaystyle {\mathsf {IZF))}$), is a strong set theory without ${\displaystyle {\mathrm {PEM} ))$. It is similar to ${\displaystyle {\mathsf {CZF))}$, but less conservative or predicative. The theory denoted ${\displaystyle {\mathsf {IKP))}$ is the constructive version of ${\displaystyle {\mathsf {KP))}$, 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 ${\displaystyle {\mathsf {CZF))}$ has been interpreted in a Martin-Löf type theories, as described below. In this way, set theory theorems provable in ${\displaystyle {\mathsf {CZF))}$ 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 ${\displaystyle {\mathsf {CZF))}$: The arithmetic theory ${\displaystyle {\mathsf {HA))}$ is bi-interpretable with a weak constructive set theory, as described in the article on Heyting arithmetic. One may arithmetically characterize a membership relation "${\displaystyle \in }$" and with it prove - instead of the existence of a set of natural numbers ${\displaystyle \omega }$ - that all sets in its theory are in bijection with a (finite) von Neumann natural, a principle denoted ${\displaystyle {\mathrm {V} }={\mathrm {Fin} ))$. 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 ${\displaystyle {\mathsf {CZF))}$ minus the existence of ${\displaystyle \omega }$ but plus ${\displaystyle {\mathrm {V} }={\mathrm {Fin} ))$ as axiom. All those axioms are discussed in detail below. Relatedly, ${\displaystyle {\mathsf {CZF))}$ also proves that the hereditarily finite sets fulfill all the previous axioms. This is a result which persists when passing on to ${\displaystyle {\mathsf {PA))}$ and ${\displaystyle {\mathsf {ZF))}$ minus Infinity.

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

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.^[4][5][6]

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 "${\displaystyle =}$" of sets and that symbol may, by abuse of notation, be used for classes. Negation "${\displaystyle \neg }$" of elementhood "${\displaystyle \in }$" is often written "${\displaystyle \notin }$", and usually the same goes for non-equality "${\displaystyle \neq }$", although in constructive mathematics the latter symbol is also used in the context with apartness relations.

Variables

Below the Greek ${\displaystyle \phi }$ denotes a predicate variable in axiom schemas and ${\displaystyle P}$ or ${\displaystyle 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 "${\displaystyle P(z)}$".

One abbreviates ${\displaystyle \forall z.{\big (}z\in A\to P(z){\big )))$ by ${\displaystyle \forall (z\in A).P(z)}$ and ${\displaystyle \exists z.{\big (}z\in A\land P(z){\big )))$ by ${\displaystyle \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 ${\displaystyle \forall (z\in A).z\in B}$, i.e. ${\displaystyle \forall z.(z\in A\to z\in B)}$, by ${\displaystyle A\subset B}$. The similar notion of subset-bounded quantifiers, as in ${\displaystyle \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 ${\displaystyle \exists !x.P(x)}$ here means ${\displaystyle \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 "${\displaystyle A=\{z\mid P(z)\))$", for the purpose of expressing ${\displaystyle P(a)}$ as ${\displaystyle a\in A}$. Logically equivalent predicates can be used to introduce the same class. One also writes ${\displaystyle \{z\in B\mid P(z)\))$ as shorthand for ${\displaystyle \{z\mid z\in B\land P(z)\))$. For a property ${\displaystyle P}$, trivially ${\displaystyle \forall z.{\big (}(z\in B\land P(z))\to z\in B{\big )))$. And so follows that ${\displaystyle \{z\in B\mid P(z)\}\subset B}$.

Equality

Denote by ${\displaystyle A\simeq B}$ the statement expressing that two classes have exactly the same elements, i.e. ${\displaystyle \forall z.(z\in A\leftrightarrow z\in B)}$, or equivalently ${\displaystyle (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 "${\displaystyle =}$" of two sets, so that through substitution, any predicate about ${\displaystyle x}$ translates to one of ${\displaystyle y}$.

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

In a constructive interpretation, the elements of a subclass ${\displaystyle A=\{z\in B\mid Q(z)\lor \neg Q(z)\))$ of ${\displaystyle B}$ may come equipped with more information than those of ${\displaystyle B}$, in the sense that being able to judge ${\displaystyle b\in A}$ is being able to judge ${\displaystyle 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 ${\displaystyle Q(b)}$ or having rejected it. As ${\displaystyle Q}$ may be not decidable for all elements in ${\displaystyle B}$, the two classes must a priori be distinguished.

Consider a property ${\displaystyle P}$ that provenly holds for all elements of a set ${\displaystyle y}$, so that ${\displaystyle \{z\in y\mid P(z)\}\simeq y}$, and assume that the class on the left hand side is established to be a set. Note that, even if this set on the left informally also ties to proof-relevant information about the validity of ${\displaystyle 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 "${\displaystyle \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 ${\displaystyle z\in x}$ of each and every set ${\displaystyle x}$ discussed. Even then, the above definition can be used to characterize equality of subsets ${\displaystyle u\subset x}$ and ${\displaystyle v\subset x}$. Note that adopting "${\displaystyle =}$" 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 ${\displaystyle x}$ and ${\displaystyle y}$, there is at least one set ${\displaystyle p}$, which hold at least those two sets (${\displaystyle z}$).

And then,

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

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

Together, the two previous axioms imply the existence of the binary union of two classes ${\displaystyle a}$ and ${\displaystyle b}$ when they have been established to be sets, and this is denoted by ${\displaystyle \bigcup \{a,b\))$ or ${\displaystyle a\cup b}$. For a fixed set ${\displaystyle y}$, to validate membership ${\displaystyle y\in a\cup b}$ in the union of two given sets ${\displaystyle z=a}$ and ${\displaystyle z=b}$, one needs to validate the ${\displaystyle y\in z}$ part of the axiom, which can be done by validating the disjunction of the predicates defining the sets ${\displaystyle a}$ and ${\displaystyle b}$, for ${\displaystyle y}$.

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

Set existence

The property that is false for any set corresponds to the empty class, which is denoted by ${\displaystyle \{\))$ 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 ${\displaystyle \{\))$ (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 ${\displaystyle t\in s}$ inside a set ${\displaystyle s}$, then we call ${\displaystyle 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 ${\displaystyle x}$, define the successor set ${\displaystyle Sx}$ as ${\displaystyle x\cup \{x\))$, for which ${\displaystyle x\in Sx}$. A sort of blend between pairing and union, an axiom more readily related to the successor is the Axiom of adjunction.^[7][8] It is relevant for the standard modeling of individual Neumann ordinals.

A simple and provenly false proposition then is, for example, ${\displaystyle \{\}\in \{\))$, corresponding to ${\displaystyle 0<0}$ in the standard arithmetic model. Again, here symbols such as ${\displaystyle \{\))$ are treated as convenient notation and any proposition really translates to an expression using only "${\displaystyle \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 ${\displaystyle 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 ${\displaystyle v}$ as well, i.e. variants with extra universal closures ${\displaystyle \forall v}$ such that the ${\displaystyle \phi }$'s may depend on the parameters.

Separation

Basic constructive set theory ${\displaystyle {\mathsf {BCST))}$ 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 ${\displaystyle s}$ obtained by the intersection of any set ${\displaystyle y}$ and any predicatively described class ${\displaystyle \{x\mid \phi (x)\))$. When the predicate is taken as ${\displaystyle x\in z}$ for ${\displaystyle z}$ proven to be a set, one obtains the binary intersection of sets and writes ${\displaystyle 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 ${\displaystyle \neg (x=x)}$, will follow the existence of the empty set. Within this conservative context of ${\displaystyle {\mathsf {BCST))}$, the Bounded Separation schema is actually equivalent to Empty Set plus the existence of the binary intersection for any two sets. The latter variant of axiomatization does not make use of a 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 ${\displaystyle \Delta _{0))$ in the set theoretical Lévy hierarchy, in analogy to ${\displaystyle \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 ${\displaystyle \Sigma _{1}^{0))$ or higher.) The schema is also the way in which Mac Lane weakens a system close to Zermelo set theory ${\displaystyle {\mathsf {Z))}$, for mathematical foundations related to topos theory.

No universal set

The following holds for any relation ${\displaystyle E}$, giving a purely logical condition by which two terms ${\displaystyle s}$ and ${\displaystyle y}$ non-relatable

${\displaystyle \forall x.{\big (}xEs\leftrightarrow (xEy\land \neg xEx){\big )}\to \neg (yEs\lor sEs\lor sEy)}$

The expression ${\displaystyle \neg (x\in x)}$ is a bounded one and thus allowed in separation. By virtue of the rejection of the final disjunct above, ${\displaystyle \neg sEy}$, Russel's construction shows that ${\displaystyle \{x\in y\mid x\notin x\}\notin y}$. So for any set ${\displaystyle y}$, Predicative Separation alone implies that there exists a set which is not a member of ${\displaystyle y}$. In particular, no universal set can exist in this theory. In a theory with the axiom of regularity, like ${\displaystyle {\mathsf {ZF))}$, of course that subset ${\displaystyle \{x\in y\mid x\notin x\))$ can be proven to be equal to ${\displaystyle y}$ itself. As an aside, in a theory with stratification, a universal set may exist because use of the syntactic expression ${\displaystyle 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 ${\displaystyle Q}$ denotes some 2-ary predicate, one should not generally expect a subclass ${\displaystyle s}$ of ${\displaystyle y}$ to be a set, in case that it is defined, for example, as in

${\displaystyle \{x\in y\mid \forall t.{\big (}(t\subset y)\to Q(x,t){\big )}\))$,

or via a similar definitions involving any quantification over the sets ${\displaystyle t\subset y}$. Note that if this subclass ${\displaystyle s}$ of ${\displaystyle y}$ is provenly a set, then this subset itself is also in the unbounded scope of set variable ${\displaystyle t}$. In other words, as the subclass property ${\displaystyle s\subset y}$ is fulfilled, this exact set ${\displaystyle s}$, defined using the expression ${\displaystyle 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 ${\displaystyle {\mathsf {IZF))}$, 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 ${\displaystyle x}$ is decidable if the corresponding relation as a subset of ${\displaystyle 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 ${\displaystyle {\mathsf {HA))}$. 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 ${\displaystyle {\mathrm {PEM} ))$ does Replacement already imply full Separation. In ${\displaystyle {\mathsf {ZF))}$, Replacement is mostly important to prove the existence of sets of high rank, namely via instances of the axiom schema where ${\displaystyle \phi (x,y)}$ relates relatively small set ${\displaystyle x}$ to bigger ones, ${\displaystyle 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 ${\displaystyle {\mathsf {ZF))}$, 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 ${\displaystyle \mathrm {Ind} (A)}$ the inductive property, ${\displaystyle 0\in A\land \forall (n\in A).Sn\in A}$. Here ${\displaystyle n}$ denotes a generic set variable. In terms of a predicate ${\displaystyle P}$ underlying the class so that ${\displaystyle \forall n.(n\in A)\leftrightarrow P(n)}$, this translates to ${\displaystyle P(0)\land \forall n.{\big (}P(n)\to P(Sn){\big )))$.

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

The elementary constructive Set Theory ${\displaystyle {\mathsf {ECST))}$ has the axiom of ${\displaystyle {\mathsf {BCST))}$ as well as the postulate of the existence of a smallest inductive set

Write ${\displaystyle \bigcap B}$ for ${\displaystyle \{x\mid \forall (y\in B).x\in y\))$, the general intersection. Define a class ${\displaystyle \omega =\bigcap \{x\mid \mathrm {Ind} (x)\))$, the intersection of all inductive sets. Explicitly, this class has those sets as members which are members of all inductive sets. With the above axiom, ${\displaystyle \omega }$ is a uniquely characterized set, the smallest infinite von Neumann ordinal. It contains the empty set and, for each set in ${\displaystyle \omega }$, another set in ${\displaystyle \omega }$ that contains one element more. Symbols called zero and successor are in the signature of the theory of Peano. In ${\displaystyle {\mathsf {BCST))}$, the above defined successor of any number also being in the class ${\displaystyle \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 ${\displaystyle S}$ come easily. Fourthly, in ${\displaystyle {\mathsf {ECST))}$, where ${\displaystyle \omega }$ is a set, ${\displaystyle S}$ can be proven to be an injective operation.

The pairwise order "${\displaystyle <}$" on the naturals is captured by their membership relation "${\displaystyle \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

${\displaystyle \exists w.\forall m.{\big (}m\in w\leftrightarrow (m=0\lor (\exists p\in w).E(p,m)){\big )))$,

where ${\displaystyle E(p,m)}$ captures the predecessor membership relation in the von Neumann model

${\displaystyle \forall n.(n\in m\leftrightarrow (n=p\lor n\in p))}$.

This weaker axioms characterizes the infinite set by expressing that all elements ${\displaystyle m}$ of it are either equal to ${\displaystyle 0}$ or themselves hold a predecessor set which shares all other members with ${\displaystyle m}$. This form can also be written more concisely using the successor notation ${\displaystyle S}$. Note that in "${\displaystyle p\in w}$", the defining expression here does again contain the symbol ${\displaystyle w}$ being characterized.

Number bounds

For a class of numbers ${\displaystyle I\subset \omega }$, the statement

${\displaystyle \exists (m\in \omega ).\forall (n\in \omega ).(n\in I\to n<m)}$

or the weaker contrapositive variant

${\displaystyle \exists (m\in \omega ).\forall (n\in \omega ).(m\leq n\to n\notin I)}$

are statements of finiteness. For decidable properties, these are ${\displaystyle \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. ${\displaystyle \{n\in \omega \mid n<m\))$ for any ${\displaystyle m\in \omega }$ and including the empty set, by ${\displaystyle \{0,1,\dots ,m-1\))$. This set equals ${\displaystyle m}$ and so at this point "${\displaystyle 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

${\displaystyle \exists (m\in \omega ).\forall (n\in I).(n<m)}$.

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 ${\displaystyle {\mathrm {PEM} ))$. Terminology for finiteness conditions varies with authors and there are many more related definitions.

For a class ${\displaystyle C}$, the statement

${\displaystyle \forall (m\in \omega ).\exists (n\in \omega ).(m\leq n\land n\in C)}$

is one of infinitude. It is ${\displaystyle \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 ${\displaystyle \omega }$. But more generally, call a set infinite if one can inject ${\displaystyle \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,

${\displaystyle \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 ${\displaystyle a\mapsto c_{a))$ and witness the rewriting ${\displaystyle \forall (a\in A).P(a,c_{a})}$.

It is a theorem that already Robinson arithmetic ${\displaystyle {\mathsf {Q))}$ represents exactly the recursive functions in terms of particular predicates ${\displaystyle P}$, which are then also proven total functional,

${\displaystyle \forall (a\in {\mathbb {N} }).\exists !(c\in {\mathbb {N} }).P(a,c)}$.

The weak classical arithmetic theory ${\displaystyle {\mathsf {Q))}$ 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, speak of a function when ${\displaystyle f\subset A\times C}$ and provenly

${\displaystyle \forall (a\in A).\,\exists (c\in C).\,\forall (d\in C).{\big (}d=c\leftrightarrow \langle a,d\rangle \in f{\big )))$.

Notably, this definition involves quantifier explicitly asking for existence - an aspect which is particularly important in the constructive context. In words: For every ${\displaystyle a}$, it demands the unique existence of a ${\displaystyle c}$ so that ${\displaystyle \langle a,c\rangle \in f}$. In the case that this holds, define the expression ${\displaystyle f(a)=c}$, involving the function application brackets, as ${\displaystyle \langle a,c\rangle \in f}$. With this notation, the above property may be stated as

${\displaystyle \forall (a\in A).\,\exists !(c\in C).f(a)=c}$

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 ${\displaystyle A\times C}$, i.e. the property is expressing not more or less than functionality w.r.t. inputs from ${\displaystyle A}$. If the domain is a set, then the function has a pair for each of its elements and so the mapping information exists as set. If domain and codomain are sets, then the above predicate only involves bounded quantifiers.

Let ${\displaystyle C^{A))$ (also written ${\displaystyle ^{A}C}$) denote the class of sets that fulfill the function property. This is the class of functions from ${\displaystyle A}$ to ${\displaystyle C}$ in a pure set theory. When functions are understood as just function graphs as above, the membership proposition ${\displaystyle f\in C^{A))$ is also written ${\displaystyle f\colon A\to C}$. Below the notation ${\displaystyle x\to y}$ is also used for ${\displaystyle 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 ${\displaystyle {\mathsf {BCST))}$ 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 ${\displaystyle A\times C}$, at least when they are described in a bounded fashion. Write ${\displaystyle 1}$ for ${\displaystyle S0}$. Given any ${\displaystyle B\subset A}$, one is now led to reason about classes such as

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

The boolean-valued characteristic functions ${\displaystyle \chi _{B}\colon A\to \{0,1\))$ are among such classes. But be aware that ${\displaystyle a\in B}$ may in generally not be decidable. That is to say, in absence of any non-constructive axioms, the disjunction ${\displaystyle a\in B\lor a\notin B}$ may not be provable, since one requires an explicit proof of either disjunct. Constructively, when

${\displaystyle \exists (y\in \{0,1\}).f(a)=y}$

cannot be witnessed for all ${\displaystyle a\in A}$, or uniqueness of a term ${\displaystyle y}$ associated with ${\displaystyle 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 always 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 ${\displaystyle Q}$, let ${\displaystyle I=\{k\in \omega \mid Q(k)\))$. Given any natural ${\displaystyle n\in \omega }$, then

${\displaystyle {\big (}Q(n)\lor \neg Q(n){\big )}\to {\big (}n\in I\lor n\notin I{\big )))$.

In classical set theory, as ${\displaystyle Q}$ is formally decidable just by ${\displaystyle {\mathrm {PEM} ))$, so is subclass membership. If the class ${\displaystyle I}$ is not finite, then successively going through the natural numbers ${\displaystyle n}$, and thus "listing" all numbers in ${\displaystyle I}$ by simply skipping those with ${\displaystyle n\notin I}$, classically constitutes an increasing surjective sequence ${\displaystyle 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 ${\displaystyle \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 ${\displaystyle Q}$ is computably decidable, the theory ${\displaystyle {\mathsf {CZF))}$ alone will not claim (prove) that all infinite ${\displaystyle I\subset \omega }$ are the range of some bijective function with domain ${\displaystyle \omega }$. See also Kripke's schema.

But being compatible with ${\displaystyle {\mathsf {ZF))}$, the development in this section still always permits "function on ${\displaystyle \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:^[9]

• Axiom of countable choice: If ${\displaystyle g\colon \omega \to z}$, one can form the one-to-many relation-set ${\displaystyle \{\langle n,u\rangle \mid n\in \omega \land u\in g(n)\))$. The axiom of countable choice would grant that whenever ${\displaystyle \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 ${\displaystyle 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 ${\displaystyle {\mathsf {ECST))}$, the theory already proves the ${\displaystyle \Sigma _{1))$-induction.
• ${\displaystyle \Pi \Sigma }$-${\displaystyle AC}$: A family of sets is better controllable if it comes indexed by a function. A set ${\displaystyle B}$ is a base if all indexed families of sets ${\displaystyle i_{S}\colon B\to S}$ over it, have a choice function ${\displaystyle f_{S))$, i.e. ${\displaystyle \forall (x\in B).f_{S}(x)\in i_{S}(x)}$. A collection of sets holding ${\displaystyle \omega }$ and its elements and which is closed by taking indexed sums and products (see dependent type) is called ${\displaystyle \Pi \Sigma }$-closed. While the axiom that all sets in the smallest ${\displaystyle \Pi \Sigma }$-closed class are a base does need some work to formulate, it is the strongest principle over ${\displaystyle {\mathsf {CZF))}$ that holds in the type theoretical interpretation ${\displaystyle {\mathsf {ML_{1}V))}$.
• 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 ${\displaystyle {\mathrm {PEM} ))$ 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

${\displaystyle a=\{u\in \{0,1\}\mid (u=0)\lor P\))$

${\displaystyle b=\{u\in \{0,1\}\mid (u=1)\lor P\))$

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, ${\displaystyle t\in a\leftrightarrow {\big (}t=0\lor (t=1\land P){\big )))$. So unconditionally, ${\displaystyle 0\in a}$, ${\displaystyle 1\in b}$. But otherwise, the uncountable classes ${\displaystyle a}$ and ${\displaystyle b}$ are as contingent as the proposition ${\displaystyle P}$ involved in their definition. Nonetheless, the setup entails several consequences, when inspecting the provable case, starting with ${\displaystyle P\to (a=\{0,1\}\land b=\{0,1\})}$. So ${\displaystyle P\to a=b}$ and indeed the equality is equivalent and decides ${\displaystyle P}$. As ${\displaystyle a}$ are ${\displaystyle b}$ are then sets, also ${\displaystyle P\to \{a,b\}=\{a\))$. A contrapositive gives ${\displaystyle \neg (a=b)\leftrightarrow \neg P}$, which is important for the proof of the theorem. In fact, as ${\displaystyle \neg P\to (a=\{0\}\land b=\{1\})}$ and, as ${\displaystyle \neg (0=1)}$, one finds in which way the sets are then different. One may moreover reason using the disjunctive syllogism that both ${\displaystyle 0\in b}$ and ${\displaystyle 1\in a}$ are each equivalent to ${\displaystyle P}$.

In the following assume a context in which ${\displaystyle 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 ${\displaystyle f\colon \{a,b\}\to a\cup b}$ with ${\displaystyle f(z)\in z}$. It is important that the elements ${\displaystyle a,b}$ of the function's domain are different than the natural numbers ${\displaystyle 0,1}$ in that a priori less is known about the former. When forming then union of the two classes, ${\displaystyle u=0\lor u=1}$ is a necessary but then also sufficient condition. Thus ${\displaystyle a\cup b=\{0,1\))$ and one is dealing with functions ${\displaystyle f}$ into a set of two distinguishable values. With choice come the conjunction ${\displaystyle 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 ${\displaystyle P}$ as well as the sets equality, or that the return values are different and ${\displaystyle P}$ can be rejected. The conclusion is that the choice postulate actually implies ${\displaystyle P\lor \neg P}$ whenever a Separation axiom allows for set comprehension using undecidable ${\displaystyle P}$. Consider, for example, an undecidable membership claim inside a given set.

Analysis of Diaconescu's theorem

So full choice is generally non-constructive. The issue is that propositions, as part of set comprehension used to separate and define the classes ${\displaystyle a}$ and ${\displaystyle b}$ from ${\displaystyle \{0,1\))$, 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 ${\displaystyle f(a)=1}$ implies ${\displaystyle P}$ and ${\displaystyle a=b}$ and this conclusion independently also applies to witnessing ${\displaystyle f(b)=0}$. On the other hand, witnessing ${\displaystyle f(a)=0\land f(b)=1}$ implies the two function arguments are not equal and this rules out ${\displaystyle P}$. There are really only three combinations, as the axiom of extensionality in the given setup makes ${\displaystyle f(a)=1\land f(b)=0}$ inconsistent. The conclusion can be summarized by the already formally derived equivalence of disjuncts ${\displaystyle {\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 ${\displaystyle 0\in a}$ and ${\displaystyle 1\in b}$, regardless of ${\displaystyle P}$. So without further analysis, this would seem to make

${\displaystyle f=\{\langle a,0\rangle ,\langle b,1\rangle \))$

a contender for a choice function. Indeed, if ${\displaystyle P}$ can be rejected, this is the only option. But in the case of provability of ${\displaystyle P}$, when ${\displaystyle \{a,b\}=\{a\))$, there is extensionally only one possible function input to a choice function. So in that situation, a choice function would have type ${\displaystyle f\colon \{a\}\to \{0,1\))$, for example

${\displaystyle f=\{\langle a,0\rangle \))$

and this would rule out the initial contender. For general ${\displaystyle P}$, the domain of a would-be choice function is not concrete but contingent on ${\displaystyle P}$ and uncountable. When considering the above functional assignment ${\displaystyle f(a)=0}$, then neither unconditionally declaring ${\displaystyle f(b)=1}$ nor ${\displaystyle f(b)=0}$ is necessarily consistent. Having identified ${\displaystyle 1}$ with ${\displaystyle \{0\))$, the two candidates described above can be represented simultaneously via the uncountable ${\displaystyle f=\{\langle a,0\rangle ,\langle b,j\rangle \))$ with the would-be natural ${\displaystyle j=\{u\in \{0\}\mid \neg P\))$. In ${\displaystyle j}$, the proposition ${\displaystyle P}$ in the "if-clause" may be replaced by ${\displaystyle a=b}$. As ${\displaystyle (P\to j=0)\land (\neg P\to j=1)}$, postulating the classical ${\displaystyle P\lor \neg P}$ here would indeed imply that this is a choice function no matter which of two truth values ${\displaystyle 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 ${\displaystyle P}$ or whether ${\displaystyle \neg P}$ does hold. Vice versa, the third and last candidate

${\displaystyle f=\{\langle b,1\rangle \))$

can be captured as part of ${\displaystyle f=\{\langle a,i\rangle ,\langle b,1\rangle \))$, where ${\displaystyle i=\{u\in \{0\}\mid P\))$. This is a classical choice function either way as well. Constructively, the domain and values of such ${\displaystyle 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 ${\displaystyle s}$, there exists an element ${\displaystyle t}$ in ${\displaystyle s}$, which shares no elements with ${\displaystyle 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 ${\displaystyle {\mathrm {PEM} ))$:

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

Arithmetic

The four Peano axioms for ${\displaystyle 0}$ and ${\displaystyle S}$, characterizing ${\displaystyle \omega }$ as a model of the natural numbers in ${\displaystyle {\mathsf {ECST))}$, have been discussed. The order "${\displaystyle <}$" of natural numbers is captured by membership "${\displaystyle \in }$" in this von Neumann model and this set is discrete, i.e. also equality is decidable. Indeed, also Heyting arithmetic proves

${\displaystyle {\mathsf {HA))\vdash \forall n.\forall m.{\big (}(n=m)\lor \neg (n=m){\big )))$

The first-order theory ${\displaystyle {\mathsf {HA))}$ 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 "${\displaystyle +}$" and multiplication "${\displaystyle \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 ${\displaystyle x}$ in the universe of discourse, i.e. for sets. This is because sets ${\displaystyle x}$ can be read as corresponding to predicates and the consequent ${\displaystyle \omega \subset x}$ states that all ${\displaystyle n\in \omega }$ fulfill said predicate. So ${\displaystyle {\mathsf {ECST))}$ proves induction for all predicates ${\displaystyle \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 ${\displaystyle {\mathsf {HA))}$, 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 ${\displaystyle {\mathsf {ECST))}$, 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 ${\displaystyle {\mathsf {ECST))}$ does actually not even enable primitive recursion for function definitions of what would be ${\displaystyle h\colon (x\times \omega )\to y}$. Indeed, despite having the Replacement axiom, the theory does not prove the addition function ${\displaystyle +\colon (\omega \times \omega )\to \omega }$ to be a set function. Going beyond ${\displaystyle {\mathsf {ECST))}$ with regards to arithmetic, the axiom granting definition of set functions via iteration-step set functions must be added: For any set ${\displaystyle y}$, set ${\displaystyle z\in y}$ and ${\displaystyle f\colon y\to y}$, there must also exist a function ${\displaystyle g\colon \omega \to y}$ attained by making use of the former, namely such that ${\displaystyle g(0)=z}$ and ${\displaystyle 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 ${\displaystyle {\mathsf {HA))}$ in our set theory, including addition and multiplication functions.

With this, arithmetic of rational numbers ${\displaystyle {\mathbb {Q} ))$ 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 ${\displaystyle n}$ and ${\displaystyle m}$, the function spaces

${\displaystyle {\{0,1,\dots ,n-1\))\to {\{0,1,\dots ,m-1\))}$

are sets. (As an aside, note that, moreover, a bounded variant of this iteration schema that grants the existence of a unique such ${\displaystyle g}$, proves the existence of a transitive closure for every set with respect to ${\displaystyle \in }$.)

Now conversely, a proof of the spelled out, ${\displaystyle {\mathsf {HA))}$-model enabling iteration principle can be based on the collection of functions one would want to write as the union ${\displaystyle \cup _{n\in \omega }y^{\{0,1,\dots ,n-1\))}$. The existence of this becomes provable when asserting that the individual function spaces on finite domains into sets ${\displaystyle y}$ form sets themselves. That principle may be written as

${\displaystyle \forall (n\in \omega ).\forall y.\ \ \exists h.h=y^{n))$