Axiomaticconstructive set theory is an approach tomathematical constructivism following the program ofaxiomatic set theory.The samefirst-order language with "${\displaystyle =}$" and "${\displaystyle \in }$" of classical set theory is usually used, so this is not to be confused with aconstructive types approach.On the other hand, some constructive theories are indeed motivated by their interpretability intype theories.

In addition to rejecting theprinciple of excluded middle (${\displaystyle \mathrm{P}\mathrm{E}\mathrm{M}}$), constructive set theories often require some logical quantifiers in their axioms to be setbounded. The latter is motivated by results tied toimpredicativity.

The logic of the set theories discussed here isconstructive in that it rejects the principle of excluded middle${\displaystyle \mathrm{P}\mathrm{E}\mathrm{M}}$, i.e. that thedisjunction${\displaystyle \varphi \vee \mathrm{\neg }\varphi }$ automatically holds for all propositions${\displaystyle \varphi }$. This is also often called thelaw of excluded middle (${\displaystyle \mathrm{L}\mathrm{E}\mathrm{M}}$) 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\vee \mathrm{\neg }P}$, either${\displaystyle P}$ or${\displaystyle \mathrm{\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 \mathrm{\forall }(x\in X).(Q(x)\vee \mathrm{\neg }Q(x))}$ 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 computationallyundecidable.

Thelaw of noncontradiction is a special case of the propositional form ofmodus ponens. Using the former with any negated statement${\displaystyle \mathrm{\neg }P}$, one validDe Morgan's law thus implies${\displaystyle \mathrm{\neg }\mathrm{\neg }(P\vee \mathrm{\neg }P)}$ already in the more conservativeminimal 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 proveclassically equivalent reformulations of classical theorems. For example, inconstructive analysis, one cannot prove theintermediate 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 permitsdouble 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, namelyMarkov's principle, does not automatically hold, but may be considered as an additional principle.

In an inhabited domain and usingexplosion, the disjunction${\displaystyle P\vee \mathrm{\exists }(x\in X).\mathrm{\neg }Q(x)}$ implies the existence claim${\displaystyle \mathrm{\exists }(x\in X).(Q(x)\to P)}$, which in turn implies${\displaystyle (\mathrm{\forall }(x\in X).Q(x))\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 \mathrm{\exists }(x\in X).\mathrm{\neg }Q(x)}$, which is generally constructively stronger than a rejection claim${\displaystyle \mathrm{\neg }\mathrm{\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 meaningtotal) 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 fullAxiom of Choice is such a non-constructive principle that implies${\displaystyle \mathrm{P}\mathrm{E}\mathrm{M}}$ for the formulas permitted in one's adopted Separation schema, byDiaconescu's theorem. Similar results hold for theAxiom of Regularity existence claim, as shown below. The latter has a classically equivalentinductive 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 inRobinson arithmetic, even justPredicative 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 decidablefor all sets is already equivalent to one of the two trivial ones,${\displaystyle \mathrm{\top }}$ or${\displaystyle \mathrm{\perp }}$. Also the real line may be taken to beindecomposable in this sense. Undecidability of disjunctions also affects the claims about total orders such as that of allordinal numbers, expressed by the provability and rejection of the clauses in the order defining disjunction${\displaystyle (\alpha \in \beta )\vee (\alpha =\beta )\vee (\beta \in \alpha )}$. This determines whether the relation istrichotomous. A weakened theory of ordinals in turn affects the proof theoretic strength defined inordinal analysis.

In exchange, constructive set theories can exhibit attractivedisjunction and existence properties, as is familiar from the study of constructive arithmetic theories. These are features of a fixed theory which metalogically relatejudgements of propositions provable in the theory. Particularly well-studied are those such features that can be expressed inHeyting arithmetic, with quantifiers over numbers and which can often berealized by numbers, as formalized inproof theory. In particular, those are the numerical existence property and the closely related disjunctive property, as well as being closed underChurch's rule, witnessing any given function to becomputable.^[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 \varphi }$, 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 }$ thatuniquely describes such a set instance. More formally, for any predicate${\displaystyle \varphi }$ there is a predicate${\displaystyle \psi }$ so that

${\displaystyle \mathsf{T}⊢\mathrm{\exists }x.\varphi (x)⟹\mathsf{T}⊢\mathrm{\exists }!x.\varphi (x)\wedge \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. InZermelo–Fraenkel set theory with sets all taken to beordinal-definable, a theory denoted${\displaystyle \mathsf{Z}\mathsf{F}+(\mathrm{V}=\mathrm{H}\mathrm{O}\mathrm{D})}$, no sets without such definability exist. The property is also enforced via theconstructible universe postulate in${\displaystyle \mathsf{Z}\mathsf{F}+(\mathrm{V}=\mathrm{L})}$.For contrast, consider the theory${\displaystyle \mathsf{Z}\mathsf{F}\mathsf{C}}$ given by${\displaystyle \mathsf{Z}\mathsf{F}}$ plus the fullaxiom of choiceexistence postulate: Recall that this collection of axioms proves thewell-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 isknown to beindependent of${\displaystyle \mathsf{Z}\mathsf{F}\mathsf{C}}$. 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{Z}\mathsf{F}\mathsf{C}}$ formallyproves 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}⊢\mathrm{\exists }e.\psi (e)⟹\mathsf{T}⊢\psi (\underset{\_}{\mathrm{e}})}$, for some number${\displaystyle \mathrm{e}}$ and where${\displaystyle \underset{\_}{\mathrm{e}}}$ denotes the corresponding numeral in the formal theory. Here one must carefully distinguish between provable implications between two propositions,${\displaystyle \mathsf{T}⊢P\to Q}$, and a theory's properties of the form${\displaystyle \mathsf{T}⊢P⟹\mathsf{T}⊢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 anaxiom 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 \varphi }$ and${\displaystyle \psi }$, one established the existence of a number${\displaystyle \mathrm{e}}$ so that${\displaystyle \mathsf{T}⊢\varphi ⟹\mathsf{T}⊢\psi (\underset{\_}{\mathrm{e}})}$. Here one may then postulate${\displaystyle \varphi \to \mathrm{\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 anadmissible rule in first-order Heyting arithmetic${\displaystyle \mathsf{H}\mathsf{A}}$ and, furthermore, thecorresponding Church's thesis principle${\displaystyle {\mathrm{C}\mathrm{T}}_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{P}\mathrm{E}\mathrm{M}}$. Similarly, adjoining the excluded middle principle${\displaystyle \mathrm{P}\mathrm{E}\mathrm{M}}$ 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{C}\mathrm{T}}_0}$ may not be adopted in${\displaystyle \mathsf{H}\mathsf{A}+\mathrm{P}\mathrm{E}\mathrm{M}}$, also known asPeano arithmetic${\displaystyle \mathsf{P}\mathsf{A}}$.

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'srule into the language of the theory itself may here read

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

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 \mathrm{\exists }(w\in \mathbb{N}).T(e,e,w)}$, expressing that${\displaystyle e}$ is the index of a computable functionhalting 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 calledsecond-order arithmetic theory${\displaystyle {\mathsf{R}\mathsf{C}\mathsf{A}}_0}$, a subsystem of thetwo-sorted first-order theory${\displaystyle {\mathsf{Z}}_2}$.

The collection of computable functions is classicallysubcountable, 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{Z}\mathsf{F}}$ that total functions (in the set theory sense) do exist that cannot be captured by aTuring 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 \mathrm{\forall }(x\in X).\mathrm{\neg }\mathrm{\neg }(Q(x)\vee \mathrm{\neg }Q(x))}$ 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 \mathrm{\neg }\mathrm{\forall }(x\in X).(Q(x)\vee \mathrm{\neg }Q(x))}$. 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 \mathrm{\neg }(Q(t)\vee \mathrm{\neg }Q(t))}$. Predicates${\displaystyle Q(x)}$ on an infinite domain${\displaystyle X}$ correspond todecision problems. Motivated by provenlycomputably 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 inBrouwerian intuitionistic analysis, in a case where the quantifier ranges over infinitely manyunending 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-callednon-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 modelingsmooth infinitesimal analysis.

Historically, the subject of constructive set theory (often also "${\displaystyle \mathsf{C}\mathsf{S}\mathsf{T}}$") begun withJohn Myhill's work on the theories also called${\displaystyle \mathsf{I}\mathsf{Z}\mathsf{F}}$ and${\displaystyle \mathsf{C}\mathsf{S}\mathsf{T}}$.^[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{Z}\mathsf{F}\mathsf{C}}$ 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{Z}\mathsf{F}\mathsf{C}}$ axioms which are equivalent in the classical setting are inequivalent in the constructive setting, and some forms imply${\displaystyle \mathrm{P}\mathrm{E}\mathrm{M}}$, as will be demonstrated. In those cases, the intuitionistically weaker formulations were consequently adopted. The far more conservative system${\displaystyle \mathsf{C}\mathsf{S}\mathsf{T}}$ is also a first-order theory, but of several sorts and bounded quantification, aiming to provide a formal foundation forErrett Bishop's program of constructive mathematics.

The main discussion presents a sequence of theories in the same language as${\displaystyle \mathsf{Z}\mathsf{F}}$, leading up toPeter Aczel's well studied${\displaystyle \mathsf{C}\mathsf{Z}\mathsf{F}}$,^[6] and beyond. Many modern results trace back to Rathjen and his students.${\displaystyle \mathsf{C}\mathsf{Z}\mathsf{F}}$ is also characterized by the two features present also in Myhill's theory:On the one hand, it is using thePredicative 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, theimpredicativePowerset axiom is discarded, generally in favor of related but weaker axioms. The strong form is very casually used in classicalgeneral topology.Adding${\displaystyle \mathrm{P}\mathrm{E}\mathrm{M}}$ to a theory even weaker than${\displaystyle \mathsf{C}\mathsf{Z}\mathsf{F}}$ recovers${\displaystyle \mathsf{Z}\mathsf{F}}$, as detailed below.^[7]The system, which has come to be known as Intuitionistic Zermelo–Fraenkel set theory (${\displaystyle \mathsf{I}\mathsf{Z}\mathsf{F}}$), is a strong set theory without${\displaystyle \mathrm{P}\mathrm{E}\mathrm{M}}$. It is similar to${\displaystyle \mathsf{C}\mathsf{Z}\mathsf{F}}$, but less conservative orpredicative.The theory denoted${\displaystyle \mathsf{I}\mathsf{K}\mathsf{P}}$ is the constructive version of${\displaystyle \mathsf{K}\mathsf{P}}$, the classicalKripke–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 ofZermelo–Fraenkel set theory (${\displaystyle \mathsf{Z}\mathsf{F}}$) with respect to their axiom as well as their underlying logic. Such theories can then also be interpreted in any model of${\displaystyle \mathsf{Z}\mathsf{F}}$.

Peano arithmetic${\displaystyle \mathsf{P}\mathsf{A}}$ isbi-interpretable with the theory given by${\displaystyle \mathsf{Z}\mathsf{F}}$ minus Infinity and without infinite sets, plus the existence of alltransitive closures. (The latter is also implied after promotingRegularity to theSet Induction schema, which is discussed below.) Likewise, constructive arithmetic can also be taken as an apology for most axioms adopted in${\displaystyle \mathsf{C}\mathsf{Z}\mathsf{F}}$:Heyting arithmetic${\displaystyle \mathsf{H}\mathsf{A}}$ is bi-interpretable with a weak constructive set theory,^[8][9] as also described in the article on${\displaystyle \mathsf{H}\mathsf{A}}$. 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{F}\mathrm{i}\mathrm{n}}$. This context further validates Extensionality, Pairing, Union, Binary Intersection (which is related to theAxiom 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{C}\mathsf{Z}\mathsf{F}}$ minus the existence of${\displaystyle \omega }$ but plus${\displaystyle \mathrm{V}=\mathrm{F}\mathrm{i}\mathrm{n}}$ as axiom. All those axioms are discussed in detail below.Relatedly,${\displaystyle \mathsf{C}\mathsf{Z}\mathsf{F}}$ also proves that thehereditarily finite sets fulfill all the previous axioms. This is a result which persists when passing on to${\displaystyle \mathsf{P}\mathsf{A}}$ and${\displaystyle \mathsf{Z}\mathsf{F}}$ minus Infinity.

As far as constructive realizations go there is a relevantrealizability theory. Relatedly, Aczel's theory constructive Zermelo-Fraenkel${\displaystyle \mathsf{C}\mathsf{Z}\mathsf{F}}$ has been interpreted in aMartin-Löf type theories, as sketched in the section on${\displaystyle \mathsf{C}\mathsf{Z}\mathsf{F}}$. 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 byDana Scott in the 1980s.^[10][11] Realizability models of${\displaystyle \mathsf{C}\mathsf{Z}\mathsf{F}}$ within theeffective topos have been identified, which, say, at once validate full Separation, relativized dependent choice${\displaystyle \mathrm{R}\mathrm{D}\mathrm{C}}$,independence of premise${\displaystyle \mathrm{I}\mathrm{P}}$ for sets, but also the subcountability of all sets, Markov's principle${\displaystyle \mathrm{M}\mathrm{P}}$ and Church's thesis${\displaystyle {\mathrm{C}\mathrm{T}}_0}$ in the formulation for all predicates.^[12]

In an axiomaticset theory, sets are the entities exhibiting properties. But there is then a more intricate relation between the set concept and logic. For example, theproperty of being a natural number smaller than 100 may be reformulated as being a member of theset 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, themeasure theoretic formalization of aprobabilistic 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.

Thepropositional connective symbols used to form syntactic formulas are standard. The axioms of set theory give a means to proveequality "${\displaystyle =}$" of sets and that symbol may, byabuse of notation, be used for classes. A set in which the equality predicate is decidable is also calleddiscrete. Negation "${\displaystyle \mathrm{\neg }}$" of equality is sometimes called the denial of equality, and is commonly written "${\displaystyle \ne }$". However, in a context withapartness 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 \varphi }$ denotes a proposition or predicate variable inaxiom 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 theunary 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 \mathrm{\exists }!x.Q(x)}$ here means${\displaystyle \mathrm{\exists }x.\mathrm{\forall }y.(y=x\leftrightarrow Q(y))}$.

As is also common, one makes use set builder notation forclasses, 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 correspondingclass 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\wedge 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 \mathrm{\forall }z.(z\in A\to Q(z))}$ by${\displaystyle \mathrm{\forall }(z\in A).Q(z)}$ and${\displaystyle \mathrm{\exists }z.(z\in A\wedge Q(z))}$ by${\displaystyle \mathrm{\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 thesubclass claim${\displaystyle \mathrm{\forall }(z\in A).z\in B}$, i.e.${\displaystyle \mathrm{\forall }z.(z\in A\to z\in B)}$, by${\displaystyle A\subset B}$.For a predicate${\displaystyle Q}$, trivially${\displaystyle \mathrm{\forall }z.((z\in B\wedge Q(z))\to z\in B)}$. And so follows that${\displaystyle \{z\in B\mid Q(z)\}\subset B}$.The notion of subset-bounded quantifiers, as in${\displaystyle \mathrm{\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 provenlyexists a set inside a class, meaning${\displaystyle \mathrm{\exists }z.(z\in A)}$, then one calls itinhabited. One may also use quantification in${\displaystyle A}$ to express this as${\displaystyle \mathrm{\exists }(z\in A).(z=z)}$. The class${\displaystyle A}$ is then provenly not the empty set, introduced below. While classically equivalent, constructivelynon-empty is a weaker notion with two negations and ought to be callednot uninhabited. Unfortunately, the word for the more useful notion of 'inhabited' is rarely used in classical mathematics.

Two ways to express that classes aredisjoint does capture many of the intuitionistically valid negation rules:${\displaystyle (\mathrm{\forall }(x\in A).x\notin B)\leftrightarrow \mathrm{\neg }\mathrm{\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 calleddetachable from${\displaystyle B}$ if the relativized membership predicate is decidable, i.e. if${\displaystyle \mathrm{\forall }(x\in B).x\in A\vee 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 \mathrm{\forall }z.(z\in A\leftrightarrow z\in B)}$, or equivalently${\displaystyle (A\subset B)\wedge (B\subset A)}$. This is not to be conflated with the concept ofequinumerosity 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 \mathrm{\exists }a.\mathrm{\forall }z.(z\in a\leftrightarrow Q(z))}$ postulate that theclass of all sets for which${\displaystyle Q}$ holds actually forms aset. Less formally, this may be expressed as${\displaystyle \mathrm{\exists }a.a\simeq A}$. Likewise, the proposition${\displaystyle \mathrm{\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 \{⟨x,y,z⟩\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 \mathrm{\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.

As he presented it, Myhill's system${\displaystyle \mathsf{C}\mathsf{S}\mathsf{T}}$ is a theory using constructive first-order logic with identity and two moresorts beyond sets, namelynatural numbers andfunctions. Its axioms are:

• The usualAxiom of Extensionality for sets, as well as one for functions, and the usualAxiom of union.
• The Axiom of restricted, or predicative,separation, which is a weakened form of theSeparation axiom from classical set theory, requiring that anyquantifications be bounded to another set, as discussed.
• A form of theAxiom of Infinity asserting that the collection of natural numbers (for which he introduces a constant${\displaystyle \omega }$) is in fact a set.
• The axiom of Exponentiation, asserting that for any two sets, there is a third set which contains all (and only) the functions whose domain is the first set, and whose range is the second set. This is a greatly weakened form of theAxiom of power set in classical set theory, to which Myhill, among others, objected on the grounds of itsimpredicativity.

And furthermore:

• The usualPeano axioms for natural numbers.
• Axioms asserting that thedomain andrange of a function are both sets. Additionally, anAxiom of non-choice asserts the existence of a choice function in cases where the choice is already made. Together these act like the usualReplacement axiom in classical set theory.

One can roughly identify the strength of this theory with a constructive subtheory of${\displaystyle \mathsf{Z}\mathsf{F}}$ when comparing with the previous sections.

And finally the theory adopts

• AnAxiom of dependent choice, which is much weaker than the usualAxiom of choice.

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

A lot ofanalysis andmodule theory has been developed in this context.

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

Beyond that, topoi also haveinternal languages that can be intuitionistic themselves and capture anotion of sets.

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

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

• Crosilla, Laura (13 February 2019)."Set Theory: Constructive and Intuitionistic ZF". InZalta, Edward N. (ed.).Stanford Encyclopedia of Philosophy.ISSN 1095-5054.OCLC 429049174.
• Van den Berg, Benno (7 September 2012)."Constructive set theory – an overview"(PDF).Slides from Heyting dag, Amsterdam

• Constructivism (philosophy of mathematics)
• Intuitionism
• Systems of set theory

• Articles with short description
• Short description matches Wikidata
• Articles with hatnote templates targeting a nonexistent page
• Pages that use a deprecated format of the math tags