Constructive set theory
Axiomatic constructive set theory is an approach to
In addition to rejecting the
Introduction
Constructive outlook
Preliminary on the use of intuitionistic logic
The logic of the set theories discussed here is
The law of noncontradiction is a special case of the propositional form of modus ponens. Using the former with any negated statement , one valid De Morgan's law thus implies 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 doublenegation 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 ) 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
In an inhabited domain and using explosion, the disjunction implies the existence claim , which in turn implies . 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 is rejected, one deals with a counterexample existence claim , which is generally constructively stronger than a rejection claim : Exemplifying a such that is contradictory of course means it is not the case that holds for all possible . But one may also demonstrate that holding for all would logically lead to a contradiction without the aid of a specific counterexample, and even while not being able to construct one. In the latter case, constructively, here one does not stipulate an existence claim.
Imposed restrictions on a set theory
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 involving unbounded collections constitute a (mathematical, and so always meaning
Metalogic
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, or . Also the real line may be taken to be
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 wellstudied 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 socalled 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 , 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 that uniquely describes such a set instance. More formally, for any predicate there is a predicate so that
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 ordinaldefinable, a theory denoted , no sets without such definability exist. The property is also enforced via the constructible universe postulate in . For contrast, consider the theory given by plus the full axiom of choice existence postulate: Recall that this collection of axioms proves the wellordering theorem, implying wellorderings exists for any set. In particular, this means that relations formally exist that establish the wellordering of (i.e. the theory claims the existence of a least element for all subsets of with respect to those relations). This is despite the fact that definability of such an ordering is known to be independent of . The latter implies that for no particular formula in the language of the theory does the theory prove that the corresponding set is a wellordering relation of the reals. So formally proves the existence of a subset with the property of being a wellordering relation, but at the same time no particular set for which the property could be validated can possibly be defined.
Anticlassical principles
As mentioned above, a constructive theory may exhibit the numerical existence property, , for some number and where denotes the corresponding numeral in the formal theory. Here one must carefully distinguish between provable implications between two propositions, , and a theory's properties of the form . 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 is closed under that rule.
One may instead consider adjoining the rule corresponding to the metatheoretical property as an implication (in the sense of "") to , as an axiom schema or in quantified form. A situation commonly studied is that of a fixed exhibiting the metatheoretical property of the following type: For an instance from some collection of formulas of a particular form, here captured via and , one established the existence of a number so that . Here one may then postulate , where the bound is a number variable in language of the theory. For example, Church's rule is an admissible rule in firstorder Heyting arithmetic and, furthermore, the corresponding Church's thesis principle may consistently be adopted as an axiom. The new theory with the principle added is anticlassical, in that it may not be consistent anymore to also adopt . Similarly, adjoining the excluded middle principle to some theory , the theory thus obtained may prove new, strictly classical statements, and this may spoil some of the metatheoretical properties that were previously established for . In such a fashion, may not be adopted in , also known as
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
Kleene's T predicate together with the result extraction expresses that any input number being mapped to the number is, through , witnessed to be a computable mapping. Here now denotes a set theory model of the standard natural numbers and is an index with respect to a fixed program enumeration. Stronger variants have been used, which extend this principle to functions defined on domains of low complexity. The principle rejects decidability for the predicate defined as , expressing that 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 , 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 secondorder arithmetic theory , a subsystem of the twosorted firstorder theory .
The collection of computable functions is classically
Constructive principles already prove for any . And so for any given element of , the corresponding excluded middle statement for the proposition cannot be negated. Indeed, for any given , by noncontradiction it is impossible to rule out 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 . Adopting this does not necessitate providing a particular witnessing the failure of excluded middle for the particular proposition , i.e. witnessing the inconsistent . Predicates on an infinite domain correspond to
So in a constructive context with a socalled nonclassical logic as used here, one may consistently adopt axioms which are both in contradiction to quantified forms of excluded middle, but also nonconstructive in the computable sense or as gauged by metalogical existence properties discussed previously. In that way, a constructive set theory can also provide the framework to study nonclassical theories, say rings modeling smooth infinitesimal analysis.
History and overview
Historically, the subject of constructive set theory (often also "") begun with John Myhill's work on the theories also called and .^{[3]}^{[4]}^{[5]} In 1973, he had proposed the former as a firstorder set theory based on intuitionistic logic, taking the most common foundation and throwing out the Axiom of choice as well as the principle of the excluded middle, initially leaving everything else as is. However, different forms of some of the axioms which are equivalent in the classical setting are inequivalent in the constructive setting, and some forms imply , as will be demonstrated. In those cases, the intuitionistically weaker formulations were consequently adopted. The far more conservative system is also a firstorder 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 , leading up to Peter Aczel's well studied ,^{[6]} and beyond. Many modern results trace back to Rathjen and his students. is also characterized by the two features present also in Myhill's theory: On the one hand, it is using the
Models
Many theories studied in constructive set theory are mere restrictions of Zermelo–Fraenkel set theory () with respect to their axiom as well as their underlying logic. Such theories can then also be interpreted in any model of .
As far as constructive realizations go there is a relevant realizability theory. Relatedly, Aczel's theory constructive ZermeloFraenkel has been interpreted in a MartinLöf type theories, as sketched in the section on . 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 within the effective topos have been identified, which, say, at once validate full Separation, relativized dependent choice , independence of premise for sets, but also the subcountability of all sets, Markov's principle and Church's thesis in the formulation for all predicates.^{[12]}
Notation
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 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
This section introduces the object language and auxiliary notions used to formalize this materialization.
Language
The propositional connective symbols used to form syntactic formulas are standard. The axioms of set theory give a means to prove equality "" of sets and that symbol may, by abuse of notation, be used for classes. A set in which the equality predicate is decidable is also called discrete. Negation "" of equality is sometimes called the denial of equality, and is commonly written "". However, in a context with
The common treatment, as also adopted here, formally only extends the underlying logic by one primitive binary predicate of set theory, "". As with equality, negation of elementhood "" is often written "".
Variables
Below the Greek denotes a proposition or predicate variable in axiom schemas and or 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 "". Unique existence here means .
Classes
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 "", for the purpose of expressing any as . Logically equivalent predicates can be used to introduce the same class. One also writes as shorthand for . For example, one may consider and this is also denoted .
One abbreviates by and by . 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 , i.e. , by . For a predicate , trivially . And so follows that . The notion of subsetbounded quantifiers, as in , 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 , then one calls it inhabited. One may also use quantification in to express this as . The class is then provenly not the empty set, introduced below. While classically equivalent, constructively nonempty 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: . Using the above notation, this is a purely logical equivalence and in this article the proposition will furthermore be expressible as .
A subclass is called detachable from if the relativized membership predicate is decidable, i.e. if holds. It is also called decidable if the superclass is clear from the context  often this is the set of natural numbers.
Extensional equivalence
Denote by the statement expressing that two classes have exactly the same elements, i.e. , or equivalently . This is not to be conflated with the concept of equinumerosity also used below.
With standing for , the convenient notational relation between and , axioms of the form postulate that the class of all sets for which holds actually forms a set. Less formally, this may be expressed as . Likewise, the proposition conveys " when is among the theory's sets." For the case where is the trivially false predicate, the proposition is equivalent to the negation of the former existence claim, expressing the nonexistence of as a set.
Further extensions of class comprehension notation as above are in common used in set theory, giving meaning to statements such as "", and so on.
Syntactically more general, a set may also be characterized using another 2ary predicate trough , where the right hand side may depend on the actual variable , and possibly even on membership in itself.
Subtheories of ZF
Here a series of familiar axioms is presented, or the relevant slight reformulations thereof. It is emphasized how the absence of in the logic affects what is provable and it is highlighted which nonclassical axioms are, in turn, consistent.
Equality
Using the notation introduced above, the following axiom gives a means to prove equality "" of two sets, so that through substitution, any predicate about translates to one of . By the logical properties of equality, the converse direction of the postulated implication holds automatically.
Extensionality

In a constructive interpretation, the elements of a subclass of may come equipped with more information than those of , in the sense that being able to judge is being able to judge . And (unless the whole disjunction follows from axioms) in the Brouwer–Heyting–Kolmogorov interpretation, this means to have proven or having rejected it. As may not be detachable from , i.e. as may be not decidable for all elements in , the two classes and must a priori be distinguished.
Consider a predicate that provenly holds for all elements of a set , so that , 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 proofrelevant information about the validity of 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 , which in informal class notation may be expressed as , is then equivalently expressed as . This means that establishing such theorems (e.g. the ones provable from full mathematical induction) enables substituting the subclass of on the left hand side of the equality for just , in any formula.
Note that adopting "" as a symbol in a predicate logic theory makes equality of two terms a quantifierfree expression.
Alternative approaches
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 "" 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 of each and every set 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 "" of those subsets. Relatedly, a loose notion of complementation of two
Merging sets
Define class notation for the pairing of a few given elements via disjunctions. E.g. is the quantifierfree statement , and likewise says , and so on.
Two other basic existence postulates given some other sets are as follows. Firstly,

Given the definitions above, expands to , so this is making use of equality and a disjunction. The axiom says that for any two sets and , there is at least one set , which hold at least those two sets.
With bounded Separation below, also the class exists as a set. Denote by the standard ordered pair model , so that e.g. denotes another bounded formula in the formal language of the theory.
And then, using existential quantification and a conjunction,

saying that for any set , there is at least one set , which holds all the members , of 's members . The minimal such set is the union.
The two axioms are commonly formulated stronger, in terms of "" instead of just "", although this is technically redundant in the context of : As the Separation axiom below is formulated with "", for statements the equivalence can be derived, given the theory allows for separation using . In cases where 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 and , when they have been established to be sets, denoted by or . For a fixed set , to validate membership in the union of two given sets and , one needs to validate the part of the axiom, which can be done by validating the disjunction of the predicates defining the sets and , for . In terms of the associated sets, it is done by validating the disjunction .
The union and other set forming notations are also used for classes. For instance, the proposition is written . Let now . Given , the decidability of membership in , i.e. the potentially independent statement , can also be expressed as . But, as for any excluded middle statement, the doublenegation of the latter holds: That union isn't not inhabited by . This goes to show that partitioning is also a more involved notion, constructively.
Set existence
The property that is false for any set corresponds to the empty class, which is denoted by or zero, . 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 (as abbreviating notation for expressions in involving characterizing properties) is justified as uniqueness for this set can be proven. As is false for any , the axiom then reads .
Write for , which equals , i.e. . Likewise, write for , which equals , i.e. . A simple and provenly false proposition then is, for example, , corresponding to in the standard arithmetic model. Again, here symbols such as are treated as convenient notation and any proposition really translates to an expression using only "" 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 may also be considered.
More generally, for a set , define the successor set as . The interplay of the successor operation with the membership relation has a recursive clause, in the sense that . By reflexivity of equality, , and in particular is always inhabited.
BCST
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 ). That is, instantiations of the schema are permitted in which the predicate (some particular ) 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 ).
Separation
Basic constructive set theory 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.
Axiom schema of predicative separation: For any bounded predicate , with parameters and with set variable not free in it, 
This axiom amounts to postulating the existence of a set obtained by the intersection of any set and any predicatively described class . For any proven to be a set, when the predicate is taken as , one obtains the binary intersection of sets and writes . Intersection corresponds to conjunction in an analog way to how union corresponds to disjunction.
When the predicate is taken as the negation , one obtains the difference principle, granting existence of any set . Note that sets like or 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 (also denoted ). Within this conservative context of , 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 , 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 , a recurring trope in the constructive analysis of set theory is to view the predicate as the subclass of the second ordinal . If it is provable that holds, or , or , then is inhabited, or empty (uninhabited), or nonempty (not uninhabited), respectively. Clearly, is equivalent to both the proposition , and also . Likewise, is equivalent to and, equivalently, also . So, here, being detachable from exactly means . In the model of the naturals, if is a number, also expresses that is smaller than . The union that is part of the successor operation definition above may be used to express the excluded middle statement as . In words, is decidable if and only if the successor of is larger than the smallest ordinal . The proposition is decided either way through establishing how is smaller: By already being smaller than , or by being 's direct predecessor. Yet another way to express excluded middle for is as the existence of a least number member of the inhabited class .
If one's separation axiom allows for separation with , then is a subset, which may be called the truth value associated with . Two truth values can be proven equal, as sets, by proving an equivalence. In terms of this terminology, the collection of proof values can a priori be understood to be rich. Unsurprisingly, decidable propositions have one of a binary set of truth values. The excluded middle disjunction for that is then also implied by the global statement .
No universal set
When using the informal class terminology, any set is also considered a class. At the same time, there do arise so called proper classes that can have no extension as a set. When in a theory there is a proof of , then must be proper. (When taking up the perspective of on sets, a theory which has full Separation, proper classes are generally thought of as those that are "too big" to be a set. More technically, they are subclasses of the cumulative hierarchy that extend beyond any ordinal bound.)
By a remark in the section on merging sets, a set cannot consistently ruled out to be a member of a class of the form . A constructive proof that it is in that class contains information. Now if is a set, then the class is provably proper. The following demonstrates this in the special case when is empty, i.e. when the right side is the universal class. Being negative results, it reads as in the classical theory.
The following holds for any relation . It gives a purely logical condition such that two terms and cannot be related to one another.
Most important here is the rejection of the final disjunct, . The expression does not involve unbounded quantification and is thus allowed in Separation.
In a theory further adopting the axiom of regularity, like , provenly is false for any set . There, this then means that the subset is equal to itself, and that the class is the empty set.
For any and , the special case in the formula above gives
This already implies that no set equals the subclass of the universal class is, i.e. that subclass is a proper one as well. But even in without Regularity it is consistent for there to be a proper class of singletons which each contain exactly themselves.
As an aside, in a theory with stratification like Intuitionistic New Foundations, the syntactic expression may be disallowed in Separation. In turn, the above proof of negation of the existence of a universal set cannot be performed, in that theory.
Predicativity
The axiom schema of Predicative Separation is also called Separation or Bounded Separation, as in Separation for setbounded quantifiers only. (Warning note: The Lévy hierarchy nomenclature is in analogy to in the arithmetical hierarchy, albeit comparison can be subtle: 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. A similar distinction is not relevant on the level or higher. Finally note that a classification of a formula may be expressed up to equivalence in the theory.)
The schema is also the way in which
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 denotes some 2ary predicate, one should not generally expect a subclass of to be a set, in case that it is defined, for example, as in
 ,
or via a similar definitions involving any quantification over the sets . Note that if this subclass of is provenly a set, then this subset itself is also in the unbounded scope of set variable . In other words, as the subclass property is fulfilled, this exact set , defined using the expression , would play a role in its own characterization.
While predicative Separation leads to fewer given class definitions being sets, it may be emphasized that many class definitions that are classically equivalent are not so when restricting oneself to the weaker logic. Due to the potential undecidability of general predicates, the notion of subset and subclass is automatically more elaborate in constructive set theories than in classical ones. So in this way one has obtained a broader theory. This remains true if full Separation is adopted, such as in the theory , which however spoils the
Replacement
Next consider the
Axiom schema of Replacement: For any predicate with set variable not free in it, 
It is granting existence, as sets, of the range of functionlike 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.
Via Replacement, the existence of any pair also follows from that of any other particular pair, such as . But as the binary union used in already made use of the Pairing axiom, this approach then necessitates postulating the existence of over that of . In a theory with the impredicative Powerset axiom, the existence of can also be demonstrated using Separation.
With the Replacement schema, the theory outlined thus far proves that the
Replacement is relevant for function comprehension and can be seen as a form of comprehension more generally. Only when assuming does Replacement already imply full Separation. In , Replacement is mostly important to prove the existence of sets of high rank, namely via instances of the axiom schema where relates relatively small set to bigger ones, .
Constructive set theories commonly have Axiom schema of Replacement, sometimes restricted to bounded formulas. However, when other axioms are dropped, this schema is actually often strengthened  not beyond , but instead merely to gain back some provability strength. Such stronger axioms exist that do not spoil the strong
If is provenly a function on and it is equipped with a codomain (all discussed in detail below), then the image of is a subset of . In other approaches to the set concept, the notion of subsets is defined in terms of "operations", in this fashion.
Hereditarily finite sets
Pendants of the elements of the class of
A sort of blend between pairing and union, an axiom more readily related to the successor is the Axiom of adjunction.^{[14]}^{[15]} Such principles are relevant for the standard modeling of individual Neumann ordinals. Axiom formulations also exist that pair Union and Replacement in one. While postulating Replacement is not a necessity in the design of a weak constructive set theory that is biinterpretable with Heyting arithmetic , some form of induction is. 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.
The discussion now proceeds with axioms granting existence of objects which, in different but related form, are also found in
ECST
For some fixed predicate and a set , the statement expresses that is the smallest (in the sense of "") among all sets for which holds true, and that it is always a subset of such . The aim of the axiom of infinity is to eventually obtain unique smallest inductive set.
In the context of common set theory axioms, one statement of infinitude is to state that a class is inhabited and also includes a chain of membership (or alternatively a chain of supersets). That is,
 .
More concretely, denote by the inductive property,
 .
In terms of a predicate underlying the class so that , the latter translates to .
Write for the general intersection . (A variant of this definition may be considered which requires , but we only use this notion for the following auxiliary definition.)
One commonly defines a class , the intersection of all inductive sets. (Variants of this treatment may work in terms of a formula that depends on a set parameter so that .) The class exactly holds all fulfilling the unbounded property . The intention is that if inductive sets exist at all, then the class shares each common natural number with them, and then the proposition , by definition of "", implies that holds for each of these naturals. While bounded separation does not suffice to prove to be the desired set, the language here forms the basis for the following axiom, granting natural number induction for predicates that constitute a set.
The elementary constructive Set Theory has the axiom of as well as the postulate

Going on, one takes the symbol to denote the now unique smallest inductive set, an unbounded
Symbols called zero and successor are in the
For some predicate of sets , the statement claims holds for all subsets of the set of naturals. And the axiom now proves such sets do exist. Such quantification is also possible in secondorder arithmetic.
The pairwise order "" on the naturals is captured by their membership relation "". The theory proves the order as well as the equality relation on this set to be decidable. Not only is no number smaller than , but induction implies that among subsets of , it is exactly the empty set which has no least member. The contrapositive of this proves the doublenegated
Weaker formulations of infinity
Should it need motivation, the handiness of postulating an unbounded set of numbers in relation to other inductive properties becomes clear in the discussion of arithmetic in set theory further below. But as is familiar from classical set theory, also weak forms of Infinity can be formulated. For example, one may just postulate the existence of some inductive set,  such an existence postulate suffices when full Separation may then be used to carve out the inductive subset of natural numbers, the shared subset of all inductive classes. Alternatively, more specific mere existence postulates may be adopted. Either which way, the inductive set then fulfills the following predecessor existence property in the sense of the von Neumann model:
Without making use of the notation for the previously defined successor notation, the extensional equality to a successor is captured by . This expresses that all elements are either equal to or themselves hold a predecessor set which shares all other members with .
Observe that through the expression "" on the right hand side, the property characterizing by its members here syntactically again contains the symbol itself. Due to the bottomup nature of the natural numbers, this is tame here. Assuming set induction on top of , no two different sets have this property. Also note that there are also longer formulations of this property, avoiding "" in favor unbounded quantifiers.
Number bounds
Adopting an Axiom of Infinity, the setbounded quantification legal in predicates used in Separation then explicitly permits numerically unbounded quantifiers  the two meanings of "bounded" should not be confused. With at hand, call a class of numbers bounded if the following existence statement holds
This is a statements of finiteness, also equivalently formulated via . Similarly, to reflect more closely the discussion of functions below, consider the above condition in the form . For decidable properties, these are statements in arithmetic, but with the Axiom of Infinity, the two quantifiers are setbound.
For a class , the logically positive unboundedness statement
is now also one of infinitude. It is 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 .
Moderate induction in ECST
In the following, an initial segment of the natural numbers, i.e. for any and including the empty set, is denoted by . This set equals and so at this point "" is mere notation for its predecessor (i.e. not involving subtraction function).
It is instructive to recall the way in which a theory with set comprehension and extensionality ends up encoding predicate logic. Like any class in set theory, a set can be read as corresponding to predicates on sets. For example, an integer is even if it is a member of the set of even integers, or a natural number has a successor if it is a member of the set of natural numbers that have a successor. For a less primitive example, fix some set and let denote the existential statement that the function space on the finite ordinal into exist. The predicate will be denoted below, and here the existential quantifier is not merely one over natural numbers, nor is it bounded by any other set. Now a proposition like the finite exponentiation principle and, less formally, the equality are just two ways of formulating the same desired statement, namely an indexed conjunction of existential propositions where ranges over the set of all naturals. Via extensional identification, the second form expresses the claim using notation for subclass comprehension and the bracketed object on the right hand side may not even constitute a set. If that subclass is not provably a set, it may not actually be used in many set theory principles in proofs, and establishing the universal closure as a theorem may not be possible. The set theory can thus be strengthened by more set existence axioms, to be used with predicative bounded Separation, but also by just postulating stronger statements.
The second universally quantified conjunct in the strong axiom of Infinity expresses mathematical induction for all in the universe of discourse, i.e. for sets. This is because the consequent of this clause, , states that all fulfill the associated predicate. Being able to use predicative separation to define subsets of , the theory proves induction for all predicates involving only setbounded quantifiers. This role of setbounded quantifiers also means that more set existence axioms impact the strength of this induction principle, further motivating the function space and collection axioms that will be a focus of the rest of the article. Notably, already validates induction with quantifiers over the naturals, and hence induction as in the firstorder arithmetic theory . The so called axiom of full mathematical induction for any predicate (i.e. class) expressed through set theory language is far stronger than the bounded induction principle valid in . The former induction principle could be directly adopted, closer mirroring secondorder arithmetic. In set theory it also follows from full (i.e. unbounded) Separation, which says that all predicates on are sets. Mathematical induction is also superseded by the (full) Set induction axiom.
Warning note: In naming induction statements, one must take care not to conflate terminology with arithmetic theories. The firstorder induction schema of natural number arithmetic theory claims induction for all predicates definable in the language of
Functions
General note on programs and functions
Naturally, the meaning of existence claims is a topic of interest in constructivism, be it for a theory of sets or any other framework. Let express a property such that a mathematical framework validates what amounts to the statement
A constructive proof calculus may validate such a judgement in terms of programs on represented domains and some object representing a concrete assignment , providing a particular choice of value in (a unique one), for each input from . Expressed through the rewriting , this function object may be understood as witnessing the proposition. Consider for example the notions of proof in through realizability theory or function terms in a type theory with a notion of quantifiers. The latter captures proof of logical proposition through programs via the Curry–Howard correspondence.
Depending on the context, the word "function" may be used in association with a particular
A theory in firstorder logic, such as the axiomatic set theories discussed here, comes with a joint notion of total and functional for a binary predicate , namely . Such theories relate to programs only indirectly. If denotes the successor operation in a formal language of a theory being studied, then any number, e.g. (the number three), may metalogically be related to the standard numeral, e.g. . Similarly, programs in the partial recursive sense may be unrolled to predicates and weak assumptions suffice so that such a translation respects equality of their return values. Among finitely axiomizable subtheories of , classical Robinson arithmetic exactly fulfills this. Its existence claims are intended to only concern natural numbers and instead of using the full mathematical induction schema for arithmetic formulas, the theories' axioms postulate that every number is either zero or that there exists a predecessor number to it. Focusing on total recursive functions here, it is a metatheorem that the language of arithmetic expresses them by predicates encoding their graph such that represents them, in the sense that it correctly proves or rejects for any inputoutput pair of numbers and in the metatheory. Now given a correctly representing , the predicate defined by represents the recursive function just as well, and as this explicitly only validates the smallest return value, the theory also proves functionality for all inputs in the sense of . Given a representing predicate, then at the cost of making use of , one can always also systematically (i.e. with a ) prove the graph to be total functional.^{[18]}
Which predicates are provably functional for various inputs, or even total functional on their domain, generally depends on the adopted axioms of a theory and proof calculus. For example, for the diagonal halting problem, which cannot have a total index, it is independent whether the corresponding graph predicate on (a decision problem) is total functional, but implies that it is. Proof theoretical function hierarchies provide examples of predicates proven total functional in systems going beyond . Which sets proven to exist do constitute a total function, in the sense introduced next, also always depends on the axioms and the proof calculus. Finally, note that the soundness of halting claims is a metalogical property beyond consistency, i.e. a theory may be consistent and from it one may prove that some program will eventually halt, despite this never actually occurring when said program is run. More formally, assuming consistency of a theory does not imply it is also arithmetically sound.
Total functional relations
In set theory language here, speak of a function class when and provenly
 .
Notably, this definition involves quantifier explicitly asking for existence  an aspect which is particularly important in the constructive context. In words: For every , it demands the unique existence of a so that . In the case that this holds one may use function application bracket notation and write . The above property may then be stated as . This notation may be extended to equality of function values. Some notational conveniences involving function application will only work when a set has indeed been established to be a function. Let (also written ) denote the class of sets that fulfill the function property. This is the class of functions from to in a pure set theory. Below the notation is also used for , for the sake of distinguishing it from ordinal exponentiation. When functions are understood as just function graphs as here, the membership proposition is also written . The Booleanvalued are among the classes discussed in the next section.
By construction, any such function respects equality in the sense that , for any inputs from . This is worth mentioning since also more broader concepts of "assignment routines" or "operations" exist in the mathematical literature, which may not in general respect this. Variants of the functional predicate definition using
If both the domain and considered codomain are sets, then the above function predicate only involves bounded quantifiers. Common notions such as
Whether a subclass (or predicate for that matter) can be judged to be a function set, or even total functional to begin with, will depend on the strength of the theory, which is to say the axioms one adopts. And notably, a general class could also fulfill the above defining predicate without being a subclass of the product , i.e. the property is expressing not more or less than functionality w.r.t. the inputs from . Now if the domain is a set, the function comprehension principle, also called axiom of unique choice or nonchoice, says that a function as a set, with some codomain, exists well. (And this principle is valid in a theory like . Also compare with the
Finitude
One defines three distinct notions involving surjections. For a general set to be (
Terminology for conditions of finiteness and infinitude may vary. Notably, subfinitely indexed sets (a notion necessarily involving surjections) are sometimes called subfinite (which can be defined without functions). The property of being finitely indexed could also be denoted "finitely countable", to fit the naming logic, but is by some authors also called finitely enumerable (which might be confusing as this suggest an injection in the other direction). Relatedly, the existence of a bijection with a finite set has not established, one may say a set is not finite, but this use of language is then weaker than to claim the set to be nonfinite. The same issue applies to countable sets (not proven countable vs. proven noncountable), et cetera. A surjective map may also be called an enumeration.
Infinitude
The set itself is clearly unbounded. In fact, for any surjection from a finite range onto , one may construct an element that is different from any element in the functions range. Where needed, this notion of infinitude can also be expressed in terms of an apartness relation on the set in question. Being not Kuratowskifinite implies being nonfinite and indeed the naturals shall not be finite in any sense. Commonly, the word infinite is used for the negative notion of being nonfinite. Further, observe that , unlike any of its members, can be put in bijection with some of its proper unbounded subsets, e.g. those of the form for any . This validates the formulations of
Call an inhabited set countable if there exists a surjection from onto it and
There are also various ways to characterize logically negative notion. The notion of uncountability, in the sense of being not countable, is also discussed in conjunction with the exponentiation axiom further below. Another notion of uncountability of is given when one can produce a member in the compliment of any of 's countable subsets. More properties of finiteness may be defined as negations of such properties, et cetera.
Characteristic functions
Separation lets us cut out subsets of products , at least when they are described in a bounded fashion. Given any , one is now led to reason about classes such as
Since , one has
and so
 .
But be aware that in absence of any nonconstructive axioms may in generally not be decidable, since one requires an explicit proof of either disjunct. Constructively, when cannot be witnessed for all the , or uniqueness of the terms associated with each cannot be proven, then one cannot judge the comprehended collection to be total functional. Case in point: The classical derivation of Schröder–Bernstein relies on case analysis  but to constitute a function, particular cases shall actually be specifiable, given any input from the domain. It has been established that Schröder–Bernstein cannot have a proof on the base of plus constructive principles.^{[19]} So to the extent that intuitionistic inference does not go beyond what is formalized here, there is no generic construction of a bijection from two injections in opposing directions.
But being compatible with , the development in this section still always permits "function on " to be interpreted as a completed object that is also 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, even if many predictions can also be expressed in terms of spreads.
If indeed one is given a function , it is the characteristic function actually deciding membership in some detachable subset and
Per convention, the detachable subset , as well as any equivalent of the formulas and (with free) may be referred to as a decidable property or set on .
One may call a collection searchable for if existence is actually decidable,
Now consider the case . If , say, then the range of is an inhabited, counted set, by Replacement. However, the need not be again a decidable set itself, since the claim is equivalent to the rather strong . Moreover, is also equivalent to and so one can state undecidable propositions about also when membership in is decidable. This also plays out like this classically in the sense that statements about may be independent, but any classical theory then nonetheless claims the joint proposition . Consider the set of all indices of proofs of an inconsistency of the theory at hand, in which case the universally closed statement is a consistency claim. In terms of arithmetic principles, assuming decidability of this would be  or arithmetic . This and the stronger related , or arithmetic , is discussed below.
Witness of apartness
The identity of indiscernibles, which in the firstorder context is a higher order principle, holds that the equality of two terms and necessitates that all predicates agree on them. And so if there exists a predicate that distinguishes two terms and in the sense that , then the principle implies that the two terms do not coincide. A form of this may be expressed set theoretically: may be deemed apart if there exists a subset such that one is a member and the other is not. Restricted to detachable subsets, this may also be formulated concisely using characteristic functions . Indeed, the latter does not actually depend on the codomain being a binary set: Equality is rejected, i.e. is proven, as soon it is established that not all functions on validate , a logically negative condition.
One may on any set define the logically positive apartness relation
As the naturals are discrete, for these functions the negative condition is equivalent to the (weaker) doublenegation of this relation. Again in words, equality of and implies that no coloring can distinguish them  and so to rule out the former, i.e. to prove , one must merely rule out the latter, i.e. merely prove .
Computable sets
Going back to more generality, given a general predicate on the numbers (say one defined from Kleene's T predicate), let again
Given any natural , then
In classical set theory, by and so excluded middle also holds for subclass membership. If the class has no numerical bound, then successively going through the natural numbers , and thus "listing" all numbers in by simply skipping those with , classically always constitutes an increasing surjective sequence . There, one can obtain a bijective function. In this way, the class of functions in typical classical set theories is provenly rich, as it also contains objects that are beyond what we know to be
In computability theory, the computable sets are ranges of nondecreasing total functions in the recursive sense, at the level 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 is computably decidable, also the theory alone will not claim (prove) that all unbounded are the range of some bijective function with domain . See also Kripke's schema. Note that bounded Separation nonetheless proves the more complicated arithmetical predicates to still constitute sets, the next level being the computably enumerable ones at .
There is a large corpus of computability theory notions regarding how general subsets of naturals relate to one another. For example, one way to establish a bijection of two such sets is by relating them through a computable isomorphism, which is a computable permutation of all the naturals. The latter may in turn be established by a pair of particular injections in opposing directions.
Boundedness criteria
Any subset injects into . If is decidable and inhabited with , the sequence
i.e.
is surjective onto , making it a counted set. That function also has the property .
Now consider a countable set that is bounded in the sense defined previously. Any sequence taking values in is then numerically capped as well, and in particular eventually does not exceed the identity function on its input indices. Formally,
A set such that this loose bounding statement holds for all sequences taking values in (or an equivalent formulation of this property) is called pseudobounded. The intention of this property would be to still capture that is eventually exhausted, albeit now this is expressed in terms of the function space (which is bigger than in the sense that always injects into ). The related notion familiar from topological vector space theory is formulated in terms of ratios going to zero for all sequences ( in the above notation). For a decidable, inhabited set, validity of pseudoboundedness, together with the counting sequence defined above, grants a bound for all the elements of .
The principle that any inhabited, pseudobounded subset of that is just countable (but not necessarily decidable) is always also bounded is called . The principle also holds generally in many constructive frameworks, such as the Markovian base theory , which is a theory postulating exclusively lawlike sequences with nice number search termination properties. However,  is independent of .
Choice functions
Not even classical proves each union of a countable set of twoelement sets to be countable again. Indeed, models of have been
A choice principle postulates that certain selections can always be made in a joint fashion in the sense that they are also manifested as a single set function in the theory. As with any independent axiom, this raises the proving capabilities while restricting the scope of possible (modeltheoretic) interpretations of the (syntactic) theory. A function existence claim can often be translated to the existence of inverses, orderings, and so on. Choice moreover implies statements about cardinalities of different sets, e.g. they imply or rule out countability of sets. Adding full choice to does not prove any new theorems, but it is strictly nonconstructive, as shown below. The development here proceeds in a fashion agnostic to any of the variants described next.^{[20]}
 Axiom of countable choice (or ): If , one can form the onetomany relationset . The axiom of countable choice would grant that whenever , one can form a function mapping each number to a unique value. The existence of such sequences is not generally provable on the base of and countable choice is not conservative over that theory. Countable choice into general sets can also be weakened further. One common consideration is to restrict the possible cardinalities of the range of , giving the weak countable choice into countable, finite or even just binary sets (). One may consider the version of countable choice for functions into (called or ), as is implied by the constructive Church's thesis principle, i.e. by postulating that all total arithmetical relations are recursive. in arithmetic may be understood as a form of choice axiom. Another means of weakening countable choice is by restricting the involved definitions w.r.t. their place in the syntactic hierarchies (say ). The weak Kőnig's lemma , which breaks strictly recursive mathematics as further discussed below, is stronger than  and is itself sometimes viewed as capturing a form of countable choice. In the presence of a weak form of countable choice, the lemma becomes equivalent to the nonconstructive principle of more logical flavor, . Constructively, a weak form of choice is required for wellbehaved Cauchy reals. 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 sequence in an inhabited , given any entire relation . In set theory, this sequence is again an infinite set of pairs, a subset of . So one is granted to pass from several existence statements to function existence, itself granting uniqueexistence statements, for every natural. An appropriate formulation of dependent choice is adopted in several constructive frameworks, e.g., by some schools that understand unending sequences as ongoing constructions instead of completed objects. At least those cases seem benign where, for any , next value existence can be validated in a computable fashion. The corresponding recursive function , if it exists, is then conceptualized as being able to return a value at infinitely many potential inputs , but these do not have to be evaluated all together at once. It also holds in many realizability models. In the condition of the formally similar recursion theorem, one is already given a unique choice at each step, and that theorem lets one combine them to a function on . So also with one may consider forms of the axiom with restrictions on . Via the bounded separation axiom in , the principle also is equivalent to a schema in two bounded predicate variables: Keeping all quantifiers ranging over , one may further narrow this set domain using a unary predicate variable, while also using any 2ary predicate instead of the relation set .
 Relativized dependent choice : This is the schema just using two general classes, instead of requiring and be sets. The domain of the choice function granted to exist is still just . Over , it implies full mathematical induction, which, in turn allows for function definition on through the recursion schema. When is restricted to definitions, it still implies mathematical induction for predicates (with an existential quantifier over sets) as well as . In , the schema is equivalent to .
 : A family of sets is better controllable if it comes indexed by a function. A set is a base if all indexed families of sets over it, have a choice function , i.e. . A collection of sets holding and its elements and which is closed by taking indexed sums and products (see dependent type) is called closed. While the axiom that all sets in the smallest closed class are a base does need some work to formulate, it is the strongest choice principle over that holds in the type theoretical interpretation .
 Axiom of choice : This is the "full" choice function postulate concerning domains that are general sets containing inhabited sets, with the codomain given as their general union. Given a collection of sets such that the logic allows to make a choice in each, the axiom grants that there exists a set function that jointly captures a choice in all. It is typically formulated for all sets but has also been studied in classical formulations for sets only up to any particular cardinality. A standard example is choice in all inhabited subsets of the reals, which classically equals the domain . For this collection there can be no uniform element selection prescription that provably constitutes a choice function on the base of . Also, when restricted to the Borel algebraof the reals, alone does not prove the existence of a function selecting a member from each nonempty such Lebesguemeasurable subset. (The set is the σalgebra generated by the intervals . It strictly includes those intervals, in the sense of , but in also only has the cardinality of the reals itself.) Striking existence claims implied by the axiom are abound. proves exists and then the axiom of choice also implies dependent choice. Critically in the present context, it moreover also implies instances of via Diaconescu's theorem. For or theories extending it, this means full choice at the very least proves for all formulas, a nonconstructive consequence not acceptable, for example, from a computability standpoint. Note that constructively, Zorn's lemma does not imply choice: When membership in function domains fails to be decidable, the extremal function granted by that principle is not provably always a choice function on the whole domain.
Diaconescu's theorem
To highlight the strength of full Choice and its relation to matters of intentionality, one should consider the classes
from the proof of Diaconescu's theorem. They are as contingent as the proposition involved in their definition and they are not proven finite. Nonetheless, the setup entails several consequences. Referring back to the introductory elaboration on the meaning of such convenient class notation, as well as to the principle of distributivity, . So unconditionally, as well as , and in particular they are inhabited. As in any model of Heyting arithmetic, using the disjunctive syllogism both and each imply . The two statements are indeed equivalent to the proposition, as clearly . The latter also says that validity of means and share all members, and there are two of these. As are are then sets, also by extensionality. Conversely, assuming they are equal means for any , validating all membership statements. So both the membership statements as well as the equalities are found to be equivalent to . Using the
In the following assume a context in which are indeed established to be sets, and thus subfinite sets. The general axiom of choice claims existence of a function with . It is important that the elements of the function's domain are different than the natural numbers in the sense that a priori less is known about the former. When forming then union of the two classes, is a necessary but then also sufficient condition. Thus and one is dealing with functions into a set of two distinguishable values. With choice come the conjunction in the codomain of the function, but the possible function return values are known to be just or . Using the distributivity, there arises a list of conditions, another disjunction. Expanding what is then established, one finds that either both as well as the sets equality holds, or that the return values are different and can be rejected. The conclusion is that the choice postulate actually implies whenever a Separation axiom allows for set comprehension using undecidable proposition .
Analysis of Diaconescu's theorem
So full choice is nonconstructive in set theory as defined here. The issue is that when propositions are part of set comprehension (like when is used to separate, and thereby define, the classes and from ), the notion of their truth values are ramified into set terms of the theory. Equality defined by the set theoretical axiom of extensionality, which itself is not related to functions, in turn couples knowledge about the proposition to information about function values. To recapitulate the final step in terms function values: On the one hand, witnessing implies and and this conclusion independently also applies to witnessing . On the other hand, witnessing