Axiomatic 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 set bounded. The latter is motivated by results tied to impredicativity.

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 }$. This is also often called the law of excluded middle (${\displaystyle {\mathrm {LEM} }}$) in contexts where it is assumed. Constructively, 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 and more commonly, 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 claim decidability of 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 either side of the disjunction(s). This 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.

The law of noncontradiction is a special case of the propositional form of modus ponens. Using the former with any negated statement ${\displaystyle \neg P}$, one valid De Morgan's law thus implies ${\displaystyle \neg \neg (P\lor \neg P)}$ already in the more conservative minimal logic. 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. Here the double-negation captures that the disjunction statement now provenly can never be ruled out or rejected, even in cases where the disjunction may not be provable (for example, by demonstrating one of the disjuncts, thus deciding ${\displaystyle P}$) from the assumed axioms.

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.

The intuitionistic logic underlying the set theories discussed here, unlike minimal logic, still permits double negation elimination for individual propositions ${\displaystyle P}$ 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.

In an inhabited domain and using explosion, the disjunction ${\displaystyle P\lor \exists (x\in X).\neg Q(x)}$ implies the existence claim ${\displaystyle \exists (x\in X).(Q(x)\to P)}$, which in turn implies ${\displaystyle {\big (}\forall (x\in X).Q(x){\big )}\to P}$. Classically, these implications are always reversible. If one of the former is classically valid, it can be worth trying to establish it in the latter form. For the special case where ${\displaystyle P}$ is rejected, one deals with a counter-example existence claim ${\displaystyle \exists (x\in X).\neg Q(x)}$, which is generally constructively stronger than a rejection claim ${\displaystyle \neg \forall (x\in X).Q(x)}$: Exemplifying a ${\displaystyle t}$ such that ${\displaystyle Q(t)}$ is contradictory of course means it is not the case that ${\displaystyle Q}$ holds for all possible ${\displaystyle x}$. But one may also demonstrate that ${\displaystyle Q}$ holding for all ${\displaystyle x}$ would logically lead to a contradiction without the aid of a specific counter-example, and even while not being able to construct one. In the latter case, constructively, here one does not stipulate an existence claim.

Compared to the classical counterpart, one is generally less likely to prove the existence of relations that cannot be realized. 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 meaning total) function. This is often because the predicate in a case-wise would-be definition may not be decidable. Adopting the standard definition of set equality via extensionality, 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 existence claim, as shown below. The latter has a classically equivalent inductive substitute. So a genuinely intuitionistic development of set theory requires the rewording of some standard axioms to classically equivalent ones. Apart from demands for computability and reservations regrading of impredicativity,^[1] technical question regarding which non-logical axioms effectively extend the underlying logic of a theory is also a research subject in its own right.

With computably undecidable propositions already arising in Robinson arithmetic, even just Predicative separation lets one define elusive subsets easily. In stark contrast to the classical framework, constructive set theories may be closed under the rule that any property that is decidable for all sets is already equivalent to one of the two trivial ones, ${\displaystyle \top }$ or ${\displaystyle \bot }$. Also the real line may be taken to be indecomposable in this sense. 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. A weakened theory of ordinals in turn affects the proof theoretic strength defined in ordinal analysis.

In exchange, constructive set theories can exhibit attractive disjunction and existence properties, as is familiar from the study of constructive arithmetic theories. These are features of a fixed theory which metalogically relate judgements of 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 numbers, 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.^[2]

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 numbers in arithmetic is played here by defined sets proven to exist by (or according to) the theory. Questions concerning the axiomatic set theory's strength and its relation to term construction are subtle. 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 theories with a classical reading of existence can in fact also be constrained so as to exhibit the strong existence property. In Zermelo–Fraenkel set theory with sets all taken to be ordinal-definable, a theory denoted ${\displaystyle {\mathsf {ZF}}+({\mathrm {V} }={\mathrm {HOD} })}$, no sets without such definability exist. The property is also enforced via the constructible universe postulate in ${\displaystyle {\mathsf {ZF}}+({\mathrm {V} }={\mathrm {L} })}$. For contrast, consider the theory ${\displaystyle {\mathsf {ZFC}}}$ given by ${\displaystyle {\mathsf {ZF}}}$ plus the full axiom of choice existence postulate: Recall that this collection of axioms proves the well-ordering theorem, implying well-orderings exists for any set. In particular, this means that relations ${\displaystyle W\subset {\mathbb {R} }\times {\mathbb {R} }}$ formally exist that establish the well-ordering of ${\displaystyle {\mathbb {R} }}$ (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 the 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 W}$ for which the property could be validated can possibly be defined.

As mentioned above, a constructive theory ${\displaystyle {\mathsf {T}}}$ may exhibit the numerical existence property, ${\displaystyle {\mathsf {T}}\vdash \exists e.\psi (e)\implies {\mathsf {T}}\vdash \psi ({\underline {\mathrm {e} }})}$, for some number ${\displaystyle {\mathrm {e} }}$ and where ${\displaystyle {\underline {\mathrm {e} }}}$ denotes the corresponding numeral in the formal theory. Here one must carefully distinguish between provable implications between two propositions, ${\displaystyle {\mathsf {T}}\vdash P\to Q}$, and a theory's properties of the form ${\displaystyle {\mathsf {T}}\vdash P\implies {\mathsf {T}}\vdash Q}$. When adopting a metalogically established schema of the latter type as an inference rule of one's proof calculus and nothing new can be proven, one says the theory ${\displaystyle {\mathsf {T}}}$ is closed under that rule.

One may instead consider adjoining the rule corresponding to the meta-theoretical property as an implication (in the sense of "${\displaystyle \to }$") to ${\displaystyle {\mathsf {T}}}$, as an axiom schema or in quantified form. A situation commonly studied is that of a fixed ${\displaystyle {\mathsf {T}}}$ exhibiting the meta-theoretical property of the following type: For an instance from some collection of formulas of a particular form, here captured via ${\displaystyle \phi }$ and ${\displaystyle \psi }$, one established the existence of a number ${\displaystyle {\mathrm {e} }}$ so that ${\displaystyle {\mathsf {T}}\vdash \phi \implies {\mathsf {T}}\vdash \psi ({\underline {\mathrm {e} }})}$. Here one may then postulate ${\displaystyle \phi \to \exists (e\in {\mathbb {N} }).\psi (e)}$, where the bound ${\displaystyle e}$ is a number variable in language of the theory. For example, Church's rule is an admissible rule in first-order Heyting arithmetic ${\displaystyle {\mathsf {HA}}}$ and, furthermore, the corresponding Church's thesis principle ${\displaystyle {\mathrm {CT} }_{0}}$ may consistently be adopted as an axiom. The new theory with the principle added is anti-classical, in that it may not be consistent anymore to also adopt ${\displaystyle {\mathrm {PEM} }}$. Similarly, adjoining the excluded middle principle ${\displaystyle {\mathrm {PEM} }}$ to some theory ${\displaystyle {\mathsf {T}}}$, the theory thus obtained may prove new, strictly classical statements, and this may spoil some of the meta-theoretical properties that were previously established for ${\displaystyle {\mathsf {T}}}$. In such a fashion, ${\displaystyle {\mathrm {CT} }_{0}}$ may not be adopted in ${\displaystyle {\mathsf {HA}}+{\mathrm {PEM} }}$, also known as Peano arithmetic ${\displaystyle {\mathsf {PA}}}$.

The focus in this subsection shall be on set theories with quantification over a fully formal notion of an infinite sequences space, i.e. function space, as it will be introduced further below. A translation of Church's rule into the language of the theory itself may here 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 classical, weak so called second-order arithmetic theory ${\displaystyle {\mathsf {RCA}}_{0}}$, a subsystem of the two-sorted first-order theory ${\displaystyle {\mathsf {Z}}_{2}}$.

The collection of 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 (in the set theory sense) 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. When 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 )}}$ for any ${\displaystyle Q}$. 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, and the relevant De Morgan's rule applies as above. 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 )}}$. Predicates ${\displaystyle Q(x)}$ on an infinite domain ${\displaystyle X}$ correspond to decision problems. Motivated by provenly computably undecidable problems, one may reject the possibility of decidability of a predicate without also 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 strictly 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, say rings modeling smooth infinitesimal analysis.

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}}}$.^[3][4][5] 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 a sequence of theories in the same language as ${\displaystyle {\mathsf {ZF}}}$, leading up to Peter Aczel's well studied ${\displaystyle {\mathsf {CZF}}}$,^[6] 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. 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.^[7] 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.

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}}}$.

Peano arithmetic ${\displaystyle {\mathsf {PA}}}$ is bi-interpretable with the theory given by ${\displaystyle {\mathsf {ZF}}}$ minus Infinity and without infinite sets, plus the existence of all transitive closures. (The latter is also implied after promoting Regularity to the Set Induction schema, which is discussed below.) Likewise, constructive arithmetic can also be taken as an apology for most axioms adopted in ${\displaystyle {\mathsf {CZF}}}$: Heyting arithmetic ${\displaystyle {\mathsf {HA}}}$ is bi-interpretable with a weak constructive set theory,^[8][9] as also described in the article on ${\displaystyle {\mathsf {HA}}}$. 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.

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 sketched in the section on ${\displaystyle {\mathsf {CZF}}}$. In this way, theorems provable in this and weaker set theories are candidates for a computer realization.

Presheaf models for constructive set theories have also been introduced. These are analogous to presheaf models for intuitionistic set theory developed by Dana Scott in the 1980s.^[10][11] Realizability models of ${\displaystyle {\mathsf {CZF}}}$ within the effective topos have been identified, which, say, at once validate full Separation, relativized dependent choice ${\displaystyle {\mathrm {RDC} }}$, independence of premise ${\displaystyle {\mathrm {IP} }}$ for sets, but also the subcountability of all sets, Markov's principle ${\displaystyle {\mathrm {MP} }}$ and Church's thesis ${\displaystyle {\mathrm {CT} _{0}}}$ in the formulation for all predicates.^[12]

In an axiomatic set theory, sets are the entities exhibiting properties. But there is then a more intricate relation between the set concept and logic. For example, the property of being a natural number smaller than 100 may be reformulated as being a member of the set of numbers with that property. The set theory axioms govern set existence and thus govern which predicates can be materialized as entity in itself, in this sense. Specification is also directly governed by the axioms, as discussed below. For a practical consideration, consider for example the property of being a sequence of coin flip outcomes that overall show more heads than tails. This property may be used to separate out a corresponding subset of any set of finite sequences of coin flips. Relatedly, the measure theoretic formalization of a probabilistic event is explicitly based around sets and provides many more examples.

This section introduces the object language and auxiliary notions used to formalize this materialization.

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. A set in which the equality predicate is decidable is also called discrete. Negation "${\displaystyle \neg }$" of equality is sometimes called the denial of equality, and is commonly written "${\displaystyle \neq }$". However, in a context with apartness relations, for example when dealing with sequences, the latter symbol is also sometimes used for something different.

The common treatment, as also adopted here, formally only extends the underlying logic by one primitive binary predicate of set theory, "${\displaystyle \in }$". As with equality, negation of elementhood "${\displaystyle \in }$" is often written "${\displaystyle \notin }$".

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

Quantifiers only ever 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 Q(z)}$". Unique existence ${\displaystyle \exists !x.Q(x)}$ here means ${\displaystyle \exists x.\forall y.{\big (}y=x\leftrightarrow Q(y){\big )}}$.

As is also common, 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 Q(z)\}}$", for the purpose of expressing any ${\displaystyle Q(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 Q(z)\}}$ as shorthand for ${\displaystyle \{z\mid z\in B\land Q(z)\}}$. For example, one may consider ${\displaystyle \{z\in B\mid z\notin C\}}$ and this is also denoted ${\displaystyle B\setminus C}$.

One abbreviates ${\displaystyle \forall z.{\big (}z\in A\to Q(z){\big )}}$ by ${\displaystyle \forall (z\in A).Q(z)}$ and ${\displaystyle \exists z.{\big (}z\in A\land Q(z){\big )}}$ by ${\displaystyle \exists (z\in A).Q(z)}$. The syntactic notion of bounded quantification in this sense can play a role in the formulation of axiom schemas, as seen in the discussion of axioms 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}$. For a predicate ${\displaystyle Q}$, trivially ${\displaystyle \forall z.{\big (}(z\in B\land Q(z))\to z\in B{\big )}}$. And so follows that ${\displaystyle \{z\in B\mid Q(z)\}\subset B}$. The 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.

If there provenly exists a set inside a class, meaning ${\displaystyle \exists z.(z\in A)}$, then one calls it inhabited. One may also use quantification in ${\displaystyle A}$ to express this as ${\displaystyle \exists (z\in A).(z=z)}$. The class ${\displaystyle A}$ is then provenly not the empty set, introduced below. While classically equivalent, constructively non-empty is a weaker notion with two negations and ought to be called not uninhabited. Unfortunately, the word for the more useful notion of 'inhabited' is rarely used in classical mathematics.

Two ways to express that classes are disjoint does capture many of the intuitionistically valid negation rules: ${\displaystyle {\big (}\forall (x\in A).x\notin B{\big )}\leftrightarrow \neg \exists (x\in A).x\in B}$. Using the above notation, this is a purely logical equivalence and in this article the proposition will furthermore be expressible as ${\displaystyle A\cap B=\{\}}$.

A subclass ${\displaystyle A\subset B}$ is called detachable from ${\displaystyle B}$ if the relativized membership predicate is decidable, i.e. if ${\displaystyle \forall (x\in B).x\in A\lor x\notin A}$ holds. It is also called decidable if the superclass is clear from the context - often this is the set of natural numbers.

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 also used below.

With ${\displaystyle A}$ standing for ${\displaystyle \{z\mid Q(z)\}}$, the convenient notational relation between ${\displaystyle x\in A}$ and ${\displaystyle Q(x)}$, axioms of the form ${\displaystyle \exists a.\forall z.{\big (}z\in a\leftrightarrow Q(z){\big )}}$ postulate that the class of all sets for which ${\displaystyle Q}$ holds actually forms a set. Less formally, this may be expressed as ${\displaystyle \exists a.a\simeq A}$. Likewise, the proposition ${\displaystyle \forall a.(a\simeq A)\to P(a)}$ conveys "${\displaystyle P(A)}$ when ${\displaystyle A}$ is among the theory's sets." For the case where ${\displaystyle P}$ is the trivially false predicate, the proposition is equivalent to the negation of the former existence claim, expressing the non-existence of ${\displaystyle A}$ as a set.

Further extensions of class comprehension notation as above are in common used in set theory, giving meaning to statements such as "${\displaystyle \{f(z)\mid Q(z)\}\simeq \{\langle x,y,z\rangle \mid T(x,y,z)\}}$", and so on.

Syntactically more general, a set ${\displaystyle w}$ may also be characterized using another 2-ary predicate ${\displaystyle R}$ trough ${\displaystyle \forall x.x\in w\leftrightarrow R(x,w)}$, where the right hand side may depend on the actual variable ${\displaystyle w}$, and possibly even on membership in ${\displaystyle w}$ itself.

Here a series of familiar axioms is presented, or the relevant slight reformulations thereof. It is emphasized how the absence of ${\displaystyle {\mathrm {PEM} }}$ in the logic affects what is provable and it is highlighted which non-classical axioms are, in turn, consistent.

Using the notation introduced above, 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 of the postulated implication 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 \{z\in B\mid Q(z)\}}$ may not be detachable from ${\displaystyle B}$, i.e. as ${\displaystyle Q}$ may be not decidable for all elements in ${\displaystyle B}$, the two classes ${\displaystyle A}$ and ${\displaystyle B}$ must a priori be distinguished.

Consider a predicate ${\displaystyle Q}$ that provenly holds for all elements of a set ${\displaystyle y}$, so that ${\displaystyle y\simeq \{z\in y\mid Q(z)\}}$, and assume that the class on the right hand side is established to be a set. Note that, even if this set on the right informally also ties to proof-relevant information about the validity of ${\displaystyle Q}$ for all the elements, the Extensionality axiom postulates that, in our set theory, the set on the right hand side is judged equal to the one on the left hand side. This above analysis also shows that a statement of the form ${\displaystyle \forall (x\in w).Q(x)}$, which in informal class notation may be expressed as ${\displaystyle w\subset \{x\mid Q(x)\}}$, is then equivalently expressed as ${\displaystyle \{x\in w\mid Q(x)\}=w}$. This means that establishing such ${\displaystyle \forall }$-theorems (e.g. the ones provable from full mathematical induction) enables substituting the subclass of ${\displaystyle w}$ on the left hand side of the equality for just ${\displaystyle w}$, in any formula.

Note that adopting "${\displaystyle =}$" as a symbol in a predicate logic theory makes equality of two terms a quantifier-free expression.

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. But also in an approach to sets emphasizing apartness may the above definition in terms of subsets be used to characterize a notion of equality "${\displaystyle \simeq }$" of those subsets. Relatedly, a loose notion of complementation of two subsets ${\displaystyle u\subset x}$ and ${\displaystyle v\subset x}$ is given when any two members ${\displaystyle s\in u}$ and ${\displaystyle t\in v}$ are provably apart from each other. The collection of complementing pairs ${\displaystyle \langle u,v\rangle }$ is algebraically well behaved.

Define class notation for the pairing of a few given elements via disjunctions. E.g. ${\displaystyle z\in \{a,b\}}$ is the quantifier-free statement ${\displaystyle (z=a)\lor (z=b)}$, and likewise ${\displaystyle z\in \{a,b,c\}}$ says ${\displaystyle (z=a)\lor (z=b)\lor (z=c)}$, and so on.

Two other basic existence postulates given some other sets are as follows. Firstly,

Given the definitions above, ${\displaystyle \{x,y\}\subset p}$ expands to ${\displaystyle \forall z.(z=x\lor z=y)\to z\in p}$, so this is making use of equality and a disjunction. The axiom says 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.

With bounded Separation below, also the class ${\displaystyle \{x,y\}}$ exists as a set. Denote by ${\displaystyle \langle x,y\rangle }$ the standard ordered pair model ${\displaystyle \{\{x\},\{x,y\}\}}$, so that e.g. ${\displaystyle q=\langle x,y\rangle }$ denotes another bounded formula in the formal language of the theory.

And then, using existential quantification and a conjunction,

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

The two axioms are commonly formulated stronger, in terms of "${\displaystyle \leftrightarrow }$" instead of just "${\displaystyle \to }$", although this is technically redundant in the context of ${\displaystyle {\mathsf {BCST}}}$: As the Separation axiom below is formulated with "${\displaystyle \leftrightarrow }$", for statements ${\displaystyle \exists t.\forall z.\phi (z)\to z\in t}$ the equivalence can be derived, given the theory allows for separation using ${\displaystyle \phi }$. In cases where ${\displaystyle \phi }$ is an existential statement, like here in the union axiom, there is also another formulation using a universal quantifier.

Also using bounded Separation, the two axioms just stated together imply the existence of a binary union of two classes ${\displaystyle a}$ and ${\displaystyle b}$, when they have been established to be sets, denoted by ${\displaystyle \bigcup \{a,b\}}$ or ${\displaystyle a\cup b}$. For a fixed set ${\displaystyle z}$, to validate membership ${\displaystyle z\in a\cup b}$ in the union of two given sets ${\displaystyle y=a}$ and ${\displaystyle y=b}$, one needs to validate the ${\displaystyle z\in y}$ 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 z}$. In terms of the associated sets, it is done by validating the disjunction ${\displaystyle z\in a\lor z\in b}$.

The union and other set forming notations are also used for classes. For instance, the proposition ${\displaystyle z\in A\land z\notin C}$ is written ${\displaystyle z\in A\setminus C}$. Let now ${\displaystyle B\subset A}$. Given ${\displaystyle z\in A}$, the decidability of membership in ${\displaystyle B}$, i.e. the potentially independent statement ${\displaystyle z\in B\lor z\notin B}$, can also be expressed as ${\displaystyle z\in B\cup (A\setminus B)}$. But, as for any excluded middle statement, the double-negation of the latter holds: That union isn't not inhabited by ${\displaystyle z}$. This goes to show that partitioning is also a more involved notion, constructively.

The property that is false for any set corresponds to the empty class, which is denoted by ${\displaystyle \{\}}$ or zero, ${\displaystyle 0}$. That the empty class is a set readily follows from other existence 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

Introduction of the symbol ${\displaystyle \{\}}$ (as abbreviating notation for expressions in involving characterizing properties) is justified as uniqueness for this set can be proven. As ${\displaystyle y\in \{\}}$ is false for any ${\displaystyle y}$, the axiom then reads ${\displaystyle \exists x.x\simeq \{\}}$.

Write ${\displaystyle 1}$ for ${\displaystyle S0}$, which equals ${\displaystyle \{\{\}\}}$, i.e. ${\displaystyle \{1\}}$. Likewise, write ${\displaystyle 2}$ for ${\displaystyle S1}$, which equals ${\displaystyle \{\{\},\{\{\}\}\}}$, i.e. ${\displaystyle \{0,1\}}$. 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.

More generally, for a set ${\displaystyle x}$, define the successor set ${\displaystyle Sx}$ as ${\displaystyle x\cup \{x\}}$. The interplay of the successor operation with the membership relation has a recursive clause, in the sense that ${\displaystyle (y\in Sx)\leftrightarrow (y\in x\lor y=x)}$. By reflexivity of equality, ${\displaystyle x\in Sx}$, and in particular ${\displaystyle Sx}$ is always inhabited.

The following makes use of axiom schemas, i.e. axioms for some collection of predicates. Some of the stated axiom schemas shall allow for any collection of set parameters as well (meaning any particular named variables ${\displaystyle v_{0},v_{1},\dots ,v_{n}}$). That is, instantiations of the schema are permitted in which the predicate (some particular ${\displaystyle \phi }$) also depends on a number of further set variables and the statement of the axiom is understood with corresponding extra outer universal closures (as in ${\displaystyle \forall v_{0}.\forall v_{1}.\cdots \forall v_{n}.}$).

Basic constructive set theory ${\displaystyle {\mathsf {BCST}}}$ consists of several axioms also part of standard set theory, except the so called "full" Separation axiom is weakened. Beyond the four axioms above, it postulates 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)\}}$. For any ${\displaystyle z}$ proven to be a set, when the predicate is taken as ${\displaystyle \phi (x):=x\in z}$, 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.

When the predicate is taken as the negation ${\displaystyle \phi (x):=x\notin z}$, one obtains the difference principle, granting existence of any set ${\displaystyle y\setminus z}$. Note that sets like ${\displaystyle y\setminus y}$ or ${\displaystyle \{x\in y\mid \neg (x=x)\}}$ are always empty. So, as noted, from Separation and the existence of at least one set (e.g. Infinity below) will follow the existence of the empty set ${\displaystyle \{\}}$ (also denoted ${\displaystyle 0}$). Within this conservative context of ${\displaystyle {\mathsf {BCST}}}$, the Predicative 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.

Predicative Separation is a schema that takes into account syntactic aspects of set defining predicates, up to provable equivalence. The permitted formulas are denoted by ${\displaystyle \Delta _{0}}$, the lowest level in the set theoretical Lévy hierarchy.^[13] General predicates in set theory are never syntactically restricted in such a way and so, in praxis, generic subclasses of sets are still part of the mathematical language. As the scope of subclasses that are provably sets is sensitive to what sets already exist, this scope is expanded when further set existence postulates added added.

For a proposition ${\displaystyle P}$, a recurring trope in the constructive analysis of set theory is to view the predicate ${\displaystyle x=0\land P}$ as the subclass ${\displaystyle B:=\{x\in 1\mid P\}}$ of the second ordinal ${\displaystyle 1:=S0=\{0\}}$. If it is provable that ${\displaystyle P}$ holds, or ${\displaystyle \neg P}$, or ${\displaystyle \neg \neg P}$, then ${\displaystyle B}$ is inhabited, or empty (uninhabited), or non-empty (not uninhabited), respectively. Clearly, ${\displaystyle P}$ is equivalent to both the proposition ${\displaystyle 0\in B}$, and also ${\displaystyle B=1}$. Likewise, ${\displaystyle \neg P}$ is equivalent to ${\displaystyle B=0}$ and, equivalently, also ${\displaystyle \neg (0\in B)}$. So, here, ${\displaystyle B}$ being detachable from ${\displaystyle 1}$ exactly means ${\displaystyle P\lor \neg P}$. In the model of the naturals, if ${\displaystyle B}$ is a number, ${\displaystyle 0\in B}$ also expresses that ${\displaystyle 0}$ is smaller than ${\displaystyle B}$. The union that is part of the successor operation definition above may be used to express the excluded middle statement as ${\displaystyle 0\in SB}$. In words, ${\displaystyle P}$ is decidable if and only if the successor of ${\displaystyle B}$ is larger than the smallest ordinal ${\displaystyle 0}$. The proposition ${\displaystyle P}$ is decided either way through establishing how ${\displaystyle 0}$ is smaller: By ${\displaystyle 0}$ already being smaller than ${\displaystyle B}$, or by ${\displaystyle 0}$ being ${\displaystyle SB}$'s direct predecessor. Yet another way to express excluded middle for ${\displaystyle P}$ is as the existence of a least number member of the inhabited class ${\displaystyle b:=B\cup \{1\}}$.