Constructive set theory is an approach to mathematical constructivism following the program of axiomatic set theory. The same firstorder language with "" and "" of classical set theory is usually used, so this is not to be confused with a constructive types approach. On the other hand, some constructive theories are indeed motivated by their interpretability in type theories.
In addition to rejecting the principle of excluded middle (), constructive set theories often require some logical quantifiers in their axioms to be bounded, motivated by results tied to impredicativity.
The logic of the set theories discussed here is constructive in that it rejects the principle of excluded middle , i.e. that the disjunction automatically holds for all propositions . As a rule, to prove the excluded middle for a proposition , i.e. to prove the particular disjunction , either or needs to be explicitly proven. When either such proof is established, one says the proposition is decidable, and this then logically implies the disjunction holds. Similarly, a predicate for in a domain is said to be decidable when the more intricate statement is provable. Nonconstructive axioms may enable proofs that formally decide such (and/or ) in the sense that they prove excluded middle for (resp. the statement using the quantifier above) without demonstrating the truth of any of the disjuncts, as is often the case in classical logic. In contrast, axiomatic theories deemed constructive tend to not permit many classical proofs of statements involving properties that are provenly computationally undecidable. Similarly, a counterexample existence claim is generally constructively stronger than a rejection claim .
The intuitionistic logic underlying the set theories discussed here, unlike the more conservative minimal logic, still permits double negation elimination for individual propositions for which excluded middle holds. In turn the theorem formulations regarding finite objects tends to not differ from their classical counterparts. Given a model of all natural numbers, the equivalent for predicates, namely Markov's principle, does not automatically hold, but may be considered as an additional principle.
Expressing the instance for of the valid law of noncontradiction and using a valid De Morgan's law, already minimal logic does prove for any given proposition . So in words, intuitionistic logic still posits: It is impossible to rule out a proposition and rule out its negation both at once, and thus the rejection of any instantiated excluded middle statement for an individual proposition is inconsistent. More generally, constructive mathematical theories tend to prove classically equivalent reformulations of classical theorems. For example, in constructive analysis, one cannot prove the intermediate value theorem in its textbook formulation, but one can prove theorems with algorithmic content that, as soon as double negation elimination and its consequences are assumed legal, are at once classically equivalent to the classical statement. The difference is that the constructive proofs are harder to find.
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 implying total) function. This is often because the predicate in a casewise wouldbe definition may not be decidable. Compared to the classical counterpart, one is generally less likely to prove the existence of relations that cannot be realized. Adopting the standard definition of set equality via extentionality, the full Axiom of Choice is such a nonconstructive principle that implies for the formulas permitted in one's adopted Separation schema, by Diaconescu's theorem. Similar results hold for the Axiom of Regularity in its standard form, as shown below. So at the very least, the development of constructive set theory requires rejection of strong choice principles and the rewording of some standard axioms to classically equivalent ones. Undecidability of disjunctions also affects the claims about total orders such as that of all ordinal numbers, expressed by the provability and rejection of the clauses in the order defining disjunction . This determines whether the relation is trichotomous. And this in turn affects the proof theoretic strength defined in ordinal analysis.
As in the study of constructive arithmetic theories, constructive set theories can exhibit attractive disjunction and existence properties. These are features of a fixed theory which relate metalogical judgements and propositions provable in the theory. Particularly wellstudied are those such features that can be expressed in Heyting arithmetic, with quantifiers over numbers and which can often be realized by numerals, as formalized in proof theory. In particular, those are the numerical existence property and the closely related disjunctive property, as well as being closed under Church's rule, witnessing any given function to be computable.
A set theory does not only express theorems about numbers, and so one may consider a more general 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 numerals in arithmetic is played here by defined sets proven to exist according to the theory, and so this is a subtle question concerning term construction and the theories strength. While many theories discussed tend have all the various numerical properties, the existence property can easily be spoiled, as will be discussed. Weaker forms of existence properties have been formulated.
Some classical theories can in fact also be constrained so as to exhibit the strong existence property. Zermelo–Fraenkel set theory with the constructible universe postulate, , or with sets all taken to be ordinaldefinable, , do have the existence property. For contrast, consider the theory given by plus the full axiom of choice existence postulate. Recall that this set of axioms implies the wellordering theorem, which in particular means that relations that establish the wellordering of formally provably exist (i.e. the theory claims the existence of a least element for all subsets of with respect to those relations). This is despite that fact that definability of such an ordering is known to be independent of . The latter implies that for no particular formula 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.
A situation commonly studied is that of a fixed theory exhibiting the following metatheoretical property: For an instance from some collection of formulas, here captured via and , one established the existence of a numeral constant so that . When adopting such a schema as an inference rule and nothing new can be proven, one says the theory is closed under that rule. Adjoining excluded middle to , the new theory may then prove new, strictly classical statements for and this may spoil the metatheoretical property that was previously established for . One may instead consider adjoining the rule corresponding to the metatheoretical property as an implication to , as a schema or in quantified form. That is to say, to postulate that any such implies such that holds, where the bound is a number variable in language of the theory. The new theory with the principle added might be anticlassical, in that it may not be consistent anymore to also adopt . For example, Church's rule is an admissible rule in Heyting arithmetic and the corresponding Church's thesis principle may be adopted, but the same is not possible in , also known as Peano arithmetic .
Now for a context of set theories with quantification over a fully formal notion of an infinite sequences space, i.e. function spaces, as will be defined below. A translation of Church's rule into the language of the theory itself may then read
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 weak classical second order arithmetic .
The collection of total, computable functions is classically subcountable, which classically is the same as being countable. But classical set theories will generally claim that holds also other functions than the computable ones. For example there is a proof in that total functions do exist that cannot be captured by a Turing machine. Taking the computable world seriously as ontology, a prime example of an anticlassical conception related the Markovian school is the permitted subcountability of various uncountable collections. Adopting the subcountability of the collection of all unending sequences of natural numbers () as an axiom 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 anticlassical axioms and so stay agnostic towards either possibility.
Constructive principles already prove 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. 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 . One may reject the possibility of decidability of some predicate on an infinite domain without making any existence claim in . As another example, such a situation is enforced in Brouwerian intuitionistic analysis, in a case where the quantifier ranges over infinitely many unending binary sequences and states that a sequence is everywhere zero. Concerning this property, of being conclusively identified as the sequence which is forever constant, adopting Brouwer's continuity principle rules out that this could be proven decidable for all the sequences.
So in a constructive context with a 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.
Historically, the subject of constructive set theory (often also "") begun with John Myhill's work on the theories also called and .^{[1]} 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 sequence of theories in the same language as , leading up to Peter Aczel's well studied ,^{[2]} and beyond. Many modern results trace back to Rathjen and his students. is also characterized by the two features present also in Myhill's theory: On the one hand, it is using the Predicative Separation instead of the full, unbounded Separation schema, see also Lévy hierarchy. Boundedness can be handled as a syntactic property or, alternatively, the theories can be conservatively extended with a higher boundedness predicate and its axioms. Secondly, the impredicative Powerset axiom is discarded, generally in favor of related but weaker axioms. The strong form is very casually used in classical general topology. Adding to a theory even weaker than recovers , as detailed below.^{[3]} The system, which has come to be known as Intuitionistic Zermelo–Fraenkel set theory (), is a strong set theory without . It is similar to , but less conservative or predicative. The theory denoted is the constructive version of , the classical Kripke–Platek set theory without a form of Powerset and where even the Axiom of Collection is bounded.
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 described below. In this way, set theory theorems provable in and weaker theories are candidates for a computer realization.
For a set theory context without infinite sets, constructive firstorder arithmetic can also be taken as an apology for most axioms adopted in : The arithmetic theory is biinterpretable with a weak constructive set theory, as described in the article on Heyting arithmetic. One may arithmetically characterize a membership relation "" and with it prove  instead of the existence of a set of natural numbers  that all sets in its theory are in bijection with a (finite) von Neumann natural, a principle denoted . This context further validates Extensionality, Pairing, Union, Binary Intersection (which is related to the Axiom schema of predicative separation) and the Set Induction schema. Taken as axioms, the aforementioned principles constitute a set theory that is already identical with the theory given by minus the existence of but plus as axiom. All those axioms are discussed in detail below. Relatedly, also proves that the hereditarily finite sets fulfill all the previous axioms. This is a result which persists when passing on to and minus Infinity.
Many theories studied in constructive set theory are mere restrictions of Zermelo–Fraenkel set theory () with respect to their axiom as well as their underlying logic. Such theories can then also be interpreted in any model of .
More recently, presheaf models for constructive set theories have been introduced. These are analogous to presheaf models for intuitionistic set theory developed by Dana Scott in the 1980s.^{[4]}^{[5]}^{[6]}
The propositional connective symbols used to form syntactic formulas are standard. The axioms of set theory give a means to prove equality "" of sets and that symbol may, by abuse of notation, be used for classes. Negation "" of elementhood "" is often written "", and usually the same goes for nonequality "", although in constructive mathematics the latter symbol is also used in the context with apartness relations.
Below the Greek denotes a predicate variable in axiom schemas and or is used for particular predicates. The word "predicate" is often used interchangeably with "formulas" as well, even in the unary case.
Quantifiers range over sets and those are denoted by lower case letters. As is common, one may use argument brackets to express predicates, for the sake of highlighting particular free variables in their syntactic expression, as in "".
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 below.
Express the subclass claim , i.e. , by . The similar notion of subsetbounded quantifiers, as in , has been used in set theoretical investigation as well, but will not be further highlighted here.
Unique existence here means .
As is also common in the study of set theories, one makes use set builder notation for classes, which, in most contexts, are not part of the object language but used for concise discussion. In particular, one may introduce notation declarations of the corresponding class via "", for the purpose of expressing as . Logically equivalent predicates can be used to introduce the same class. One also writes as shorthand for . For a property , trivially . And so follows that .
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.
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 holds automatically.
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 be not decidable for all elements in , the two classes must a priori be distinguished.
Consider a property that provenly holds for all elements of a set , so that , and assume that the class on the left hand side is established to be a set. Note that, even if this set on the left informally also ties to proofrelevant information about the validity of for all the elements, the Extensionality axiom postulates that, in our set theory, the set on the left hand side is judged equal to the one on the right hand side. While often adopted, this axiom has been criticized in constructive thought, as it effectively collapses differently defined properties, or at least the sets viewed as the extension of these properties, a Fregian notion.
Modern type theories may instead aim at defining the demanded equivalence "" 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. Even then, the above definition can be used to characterize equality of subsets and . Note that adopting "" as a symbol in a predicate logic theory makes equality of two terms a quantifierfree expression.
Two other basic axioms are as follows. Firstly,

saying that for any two sets and , there is at least one set , which hold at least those two sets ().
And then,

saying that for any set , there is at least one set , which holds all members , of 's members .
The two axioms may also be formulated stronger in terms of "". In the context of with Separation, this is not necessary.
Together, the two previous axioms imply the existence of the binary union of two classes and when they have been established to be sets, and this is 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 .
Define class notation for a few given elements via disjunctions, e.g. says . Denote by the standard ordered pair model .
The property that is false for any set corresponds to the empty class, which is denoted by or zero, 0. That the empty class is a set readily follows from other axioms, such as the Axiom of Infinity below. But if, e.g., one is explicitly interested in excluding infinite sets in one's study, one may at this point adopt the

This axiom would also readily be accepted, but is not relevant in the context of stronger axioms below. Introduction of the symbol (as abbreviating notation for expressions in involving characterizing properties) is justified as uniqueness for this set can be proven. If there provenly exists a set inside a set , then we call inhabited and it is then provenly not the empty set. While classically equivalent, constructively nonempty is a weaker notion with two negations. Unfortunately, the word for the more useful notion of 'inhabited' is rarely used in classical mathematics.
For a set , define the successor set as , for which . A sort of blend between pairing and union, an axiom more readily related to the successor is the Axiom of adjunction.^{[7]}^{[8]} It is relevant for the standard modeling of individual Neumann ordinals.
A simple and provenly false proposition then is, for example, , 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.
The following makes use of axiom schemas, i.e. axioms for some collection of predicates. Note that some of the stated axiom schemas are often presented with set parameters as well, i.e. variants with extra universal closures such that the 's may depend on the parameters.
Basic constructive set theory consists of several axioms also part of standard set theory, except the Separation axiom is weakened. Beyond the four axioms above, it the Predicative Separation as well as the Replacement schema.
Axiom schema of predicative separation: For any bounded predicate 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 . When the predicate is taken as for proven to be a set, one obtains the binary intersection of sets and writes . Intersection corresponds to conjunction in an analog way to how union corresponds to disjunction.
As noted, from Separation and the existence of at least one set (e.g. Infinity below) and a predicate that is false of any set, like , will follow the existence of the empty set. Within this conservative context of , the Bounded Separation schema is actually equivalent to Empty Set plus the existence of the binary intersection for any two sets. The latter variant of axiomatization does not make use of a formula schema.
The axiom schema is also called Bounded Separation, as in Separation for setbounded quantifiers only. It is a schema that takes into account syntactic aspects of predicates. The scope of legal formulas is enriched by further set existence postulates. The bounded formulas are also denoted by in the set theoretical Lévy hierarchy, in analogy to in the arithmetical hierarchy. (Note however that the arithmetic classification is sometimes expressed not syntactically but in terms of subclasses of the naturals. Also, the bottom level of the arithmetical hierarchy has several common definitions, some not allowing the use of some total functions. The distinction is not relevant on the level or higher.) The schema is also the way in which Mac Lane weakens a system close to Zermelo set theory , for mathematical foundations related to topos theory.
The following holds for any relation , giving a purely logical condition by which two terms and nonrelatable
The expression is a bounded one and thus allowed in separation. By virtue of the rejection of the final disjunct above, , Russel's construction shows that . So for any set , Predicative Separation alone implies that there exists a set which is not a member of . In particular, no universal set can exist in this theory. In a theory with the axiom of regularity, like , of course that subset can be proven to be equal to itself. As an aside, in a theory with stratification, a universal set may exist because use of the syntactic expression may be disallowed in proofs of existence by, essentially, separation.
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 must be emphasized that many class definitions that are classically equivalent are not so when restricting oneself to constructive logic. So in this way, one gets a broader theory, constructively. Due to the potential undecidability of general predicates, the notion of subset and subclass is more elaborate in constructive set theories than in classical ones. This remains true if full Separation is adopted, as in the theory , which however spoils the existence property as well as the standard type theoretical interpretations, and in this way spoils a bottomup view of constructive sets. As an aside, as subtyping is not a necessary feature of constructive type theory, constructive set theory can be said to quite differ from that framework.
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.
With the Replacement schema, this theory proves that the equivalence classes or indexed sums are sets. In particular, the Cartesian product, holding all pairs of elements of two sets, is a set. Equality of elements inside a set is decidable if the corresponding relation as a subset of is decidable.
Replacement is not necessary in the design of a weak constructive set theory that is biinterpretable with Heyting arithmetic . However, some form of induction is. Replacement together with Set Induction (introduced below) also suffices to axiomize hereditarily finite sets constructively and that theory is also studied without Infinity. For comparison, consider the very weak classical theory called General set theory that interprets the class of natural numbers and their arithmetic via just Extensionality, Adjunction and full Separation.
Replacement can be seen as a form of comprehension. Only when assuming does Replacement already imply full Separation. In , Replacement is mostly important to prove the existence of sets of high rank, namely via instances of the axiom schema where 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 existence properties of a theory, as discussed further below.
The discussion now proceeds with axioms granting existence of objects also found in dependent type theory, namely natural numbers and products.
Denote by the inductive property, . Here denotes a generic set variable. In terms of a predicate underlying the class so that , this translates to .
For some fixed predicate , the statement expresses that is the smallest (in the sense of "") set among all sets for which holds true, and that it is always a subset of such .
The elementary constructive Set Theory has the axiom of as well as the postulate of the existence of a smallest inductive set

Write for , the general intersection. Define a class , the intersection of all inductive sets. Explicitly, this class has those sets as members which are members of all inductive sets. With the above axiom, is a uniquely characterized set, the smallest infinite von Neumann ordinal. It contains the empty set and, for each set in , another set in that contains one element more. Symbols called zero and successor are in the signature of the theory of Peano. In , the above defined successor of any number also being in the class follow directly from the characterization of the natural naturals by our von Neumann model. Since the successor of such a set contains itself, one also finds that no successor equals zero. So two of the Peano axioms regarding the symbols zero and the one regarding closedness of come easily. Fourthly, in , where is a set, can be proven to be an injective operation.
The pairwise order "" on the naturals is captured by their membership relation "". It is important to note that the theory proves the order as well as the equality relation on this set to be decidable. The value of formulating the axiom using the inductive property is explained in the discussion on arithmetic.
Weak forms of axioms of infinity can be formulated, all postulating that some set containing elements with the common natural number properties exist. Then full Separation may be used to obtain the "sparse" such set, the set of natural numbers. In the context of otherwise weaker axiom systems, an axiom of infinity should be strengthened so as to imply existence of such a sparse set on its own. One weaker form of Infinity is
where captures the predecessor membership relation in the von Neumann model
This weaker axioms characterizes the infinite set by expressing that all elements of it are either equal to or themselves hold a predecessor set which shares all other members with . This form can also be written more concisely using the successor notation . Note that in "", the defining expression here does again contain the symbol being characterized.
For a class of numbers , the statement
or the weaker contrapositive variant
are statements of finiteness. For decidable properties, these are statements in arithmetic, but with the axiom of Infinity, the two quantifiers are setbound. Denote an initial segment of the natural numbers, i.e. for any and including the empty set, by . This set equals and so at this point "" is mere notation for its predecessor (i.e. not involving subtraction function). To reflect more closely the discussion of functions below, write the above condition as
Now for a general set, to be finitely enumerable shall mean that there is a surjection from a von Neumann natural number onto it, which is a function existence claim. Further, to be finite means there is a bijective function to a natural. To be subfinite means to be a subset of a finite set. The claim that being a finite set is equivalent to being subfinite is equivalent to . Terminology for finiteness conditions varies with authors and there are many more related definitions.
For a class , the statement
is 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 . But more generally, call a set infinite if one can inject into it, which is again a function existence claim.
It is appropriate to discuss the function concept at this point.
Naturally, the logical meaning of existence claims is a topic of interest in intuitionistic logic, be it for a theory of sets or any other mathematical framework. A constructive proof calculus may validate statements as above,
in terms of programs on represented domains. Consider for example the notions of proof through type or realizability theory. Roughly, the task then is to provide a mapping and witness the rewriting .
It is a theorem that already Robinson arithmetic represents exactly the recursive functions in terms of particular predicates , which are then also proven total functional,
The weak classical arithmetic theory postulates, instead of using the full mathematical induction schema for arithmetic formulas, that every number is either zero or that there exists a predecessor number to it.
Finally, beware of a common ambiguity in related texts on recursion theory, where "function" needs to be understood in the computable sense, which is generally narrower than what is discussed further below. Similarly, below there is also no need to speak of "total functions", as this is part of the definition of a set theoretical function.
Now in the current set theoretical approach, speak of a function 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, define the expression , involving the function application brackets, as . With this notation, the above property may be stated as
So one studies sets capturing particular total relations. Whether a subclass can be judged to be a function will depend on the strength of the theory, which is to say the axioms one adopts. Notably, a general class could fulfill the above predicate without being a subclass of the product , i.e. the property is expressing not more or less than functionality w.r.t. inputs from . If the domain is a set, then the function has a pair for each of its elements and so the mapping information exists as set. If domain and codomain are sets, then the above predicate only involves bounded quantifiers.
Let (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. When functions are understood as just function graphs as above, the membership proposition is also written . Below the notation is also used for , for the sake of distinguishing it from ordinal exponentiation.
Common notions such as surjectivity and injectivity can be expressed in a bounded fashion as well. Note that injectivity shall be defined positively, not by its contrapositive, which is common practice in classical mathematics.
The axiom scheme of Replacement can also be formulated in terms of the ranges of such set functions. It is a metatheorem for theories containing that adding a function symbol for a provenly total class function is a conservative extension, despite this changing the scope of bounded Separation.
Separation lets us cut out subsets of products , at least when they are described in a bounded fashion. Write for . Given any , one is now led to reason about classes such as
The booleanvalued characteristic functions are among such classes. But be aware that may in generally not be decidable. That is to say, in absence of any nonconstructive axioms, the disjunction may not be provable, since one requires an explicit proof of either disjunct. Constructively, when
cannot be witnessed for all , or uniqueness of a term associated with not be proven, then one cannot judge the comprehended collection to be total functional.
Variants of the functional predicate definition using apartness relations on setoids have been defined as well. A function will always be a set if its range is. Care must be taken with nomenclature "function", which sees use in most mathematical frameworks, also because some tie a function term itself to a particular codomain.
Given Infinity and any propositions , let . Given any natural , then
In classical set theory, as is formally decidable just by , so is subclass membership. If the class is not finite, then successively going through the natural numbers , and thus "listing" all numbers in by simply skipping those with , classically constitutes an increasing surjective sequence . There, one can obtain a bijective function. In this way, the classical class of functions is provenly rich, as it also contains objects that are beyond what we know to be effectively computable, or programmatically listable in praxis.
In computability theory, the computable sets are ranges of 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, the theory alone will not claim (prove) that all infinite are the range of some bijective function with domain . See also Kripke's schema.
But being compatible with , the development in this section still always permits "function on " to be interpreted as an object not necessarily given as lawlike sequence. Applications may be found in the common models for claims about probability, e.g. statements involving the notion of "being given" an unending random sequence of coin flips.
Choice principles postulate the existence of functions. These can then be translated to claims of existence of inverses, ordering, and so on. Choice moreover implies statements about cardinalities of different sets, e.g. they imply or rule out countability of sets. The constructive development here proceeds in a fashion agnostic to any discussed choice principles, but here are well studied variants:^{[9]}
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. Referring back to the introductory elaboration on the meaning of such convenient class notation, as well as to the principle of distributivity, . So unconditionally, , . But otherwise, the uncountable classes and are as contingent as the proposition involved in their definition. Nonetheless, the setup entails several consequences, when inspecting the provable case, starting with . So and indeed the equality is equivalent and decides . As are are then sets, also . A contrapositive gives , which is important for the proof of the theorem. In fact, as and, as , one finds in which way the sets are then different. One may moreover reason using the disjunctive syllogism that both and are each equivalent to .
In the following assume a context in which are established to be sets, and thus subfinite sets. Then for inhabited such 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 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. Using the distributivity, there arises a list of conditions on the possible function return values, a disjunction. Expanding what is then established, one finds that either both as well as the sets equality, 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 . Consider, for example, an undecidable membership claim inside a given set.
So full choice is generally nonconstructive. The issue is that propositions, as part of set comprehension used to separate and define the classes and from , ramify truth values into set terms. Equality defined by the set theoretical axiom of extensionality, which itself is not related to functions, in turn couples knowledge about the predicate to information about function values. Spoken in terms function values: On the one hand, witnessing implies and and this conclusion independently also applies to witnessing . On the other hand, witnessing implies the two function arguments are not equal and this rules out . There are really only three combinations, as the axiom of extensionality in the given setup makes inconsistent. The conclusion can be summarized by the already formally derived equivalence of disjuncts . So if the constructive reading of existence is to be preserved, full choice may be not adopted in the set theory, because the mere claim of function existence does not realize a particular function.
To better understand why we cannot expect to be granted a definitive (total) function, consider naive function candidates. It was noted that it is the case that and , regardless of . So without further analysis, this would seem to make
a contender for a choice function. Indeed, if can be rejected, this is the only option. But in the case of provability of , when , there is extensionally only one possible function input to a choice function. So in that situation, a choice function would have type , for example
and this would rule out the initial contender. For general , the domain of a wouldbe choice function is not concrete but contingent on and uncountable. When considering the above functional assignment , then neither unconditionally declaring nor is necessarily consistent. Having identified with , the two candidates described above can be represented simultaneously via the uncountable with the wouldbe natural . In , the proposition in the "ifclause" may be replaced by . As , postulating the classical here would indeed imply that this is a choice function no matter which of two truth values takes. And as in the constructive case, given a particular choice function  a set holding either exactly one or exactly two pairs  one could actually infer whether or whether does hold. Vice versa, the third and last candidate
can be captured as part of , where . This is a classical choice function either way as well. Constructively, the domain and values of such dependent wouldbe functions will be undecidable and as such one fails to prove functional totality. In computable interpretations, set theory axioms postulating (total) function existence lead to the requirement for recursive functions. From a function realization one can infer the branches taken by the "ifclauses" of the classical solutions, which were undecided in the interpreted theory.
The axiom of regularity states that for every inhabited set , there exists an element in , which shares no elements with . As opposed to the axiom of choice, this existence claim reaches for an element of every inhabited set, i.e. the "domain" are all inhabited sets. Its formulation does not involve a unique existence claim but instead guarantees a set with a specific property. As the axiom correlates membership claims at different rank, the axiom also ends up implying :
The proof from choice above had used a particular set from above. The proof in this paragraph also uses this , for which it was already established that . Also recall that when Separation applies to , the set is defined using the clause , so that any given has . Now let be the postulated member with the empty intersection property, which in particular means . Together, one finds , which also formally decides .
The four Peano axioms for and , characterizing as a model of the natural numbers in , have been discussed. The order "" of natural numbers is captured by membership "" in this von Neumann model and this set is discrete, i.e. also equality is decidable. Indeed, also Heyting arithmetic proves
The firstorder theory has the same nonlogical axioms as Peano arithmetic. An account of induction is given in the next paragraph. Then, it is clarified which set theory axiom must be asserted to prove existence of the binary functions addition "" and multiplication "" with their respective relation to zero and successor.
The second universally quantified conjunct in the axiom of Infinity expresses mathematical induction for all in the universe of discourse, i.e. for sets. This is because sets can be read as corresponding to predicates and the consequent states that all fulfill said predicate. So proves induction for all predicates involving only setbounded quantifiers. The much stronger axiom of full mathematical induction for any predicate expressed though set theory language could also be adopted at this point in our development. That induction principle follows from full (i.e. unbounded) Separation as well as from (full) Set induction.
Note: In naming induction statements, one must take care not to conflate terminology with arithmetic theories. The firstorder induction schema of natural number arithmetic claims induction for all predicates definable in the language of firstorder arithmetic, namely predicates of just numbers. So to interpret the axiom schema of , one interprets these arithmetical formulas. One may also speak about the induction in secondorder arithmetic, explicitly expressed for subsets of the naturals. The class of subsets can be taken to correspond to a richer collection of formulas than the firstorder arithmetic definable ones. Typical set theories like the one discussed here are also firstorder, but those theories are not arithmetics and so formulas may also quantify over the subsets of the naturals. Finally, bounded quantification in that context here means quantification over the elements of whatever is established to be a set.
In , many mathematical statements can be proven per individual set, opposed to many formulas involving universal quantification, as would be possible, for example, with an induction principle for classes. With this, the set theory axioms listed so far suffice as formalized framework for a good portion of basic mathematics. That said, the constructive set theory does actually not even enable primitive recursion for function definitions of what would be . Indeed, despite having the Replacement axiom, the theory does not prove the addition function to be a set function. Going beyond with regards to arithmetic, the axiom granting definition of set functions via iterationstep set functions must be added: For any set , set and , there must also exist a function attained by making use of the former, namely such that and . This postulate is akin to the transfinite recursive theorem, except it is restricted to set functions and finite ordinals, i.e. there is no clause about limit ordinals. It functions as the set theoretical equivalent of a natural numbers object in category theory. This then enables a full interpretation of Heyting arithmetic in our set theory, including addition and multiplication functions.
With this, arithmetic of rational numbers can then also be defined and its properties, like uniqueness and countability, be proven. A set theory with this will also prove that, for any naturals and , the function spaces
are sets. (As an aside, note that, moreover, a bounded variant of this iteration schema that grants the existence of a unique such , proves the existence of a transitive closure for every set with respect to .)
Now conversely, a proof of the spelled out, model enabling iteration principle can be based on the collection of functions one would want to write as the union . The existence of this becomes provable when asserting that the individual function spaces on finite domains into sets form sets themselves. That principle may be written as
This should further motivate the adoption of an even stronger axiom of more set theoretical flavor, instead of just directly embedding arithmetic principles into our theory. This more set theoretical exponentiation axiom will, however, still not prove the full induction schema for formulas with quantifiers over sets.
Before discussing (even classically) uncountable sets, here taking a step back to the strength of , note that induction schemas may be adopted in conjunction with a natural number sort, without ever postulating that the collection of naturals exists as a set. And it is worth noting that in the program of predicative arithmetic, even the mathematical induction schema has been criticized as possibly being impredicative, when natural numbers are defined as the object which fulfill this schema, which itself is defined in terms of all naturals. The minimal assumptions necessary to obtain theories of natural number arithmetic are thoroughly studied in proof theory and are naturally framed as insights into first and secondorder arithmetic theories.
The classical theories starting with bounded arithmetic adopt different conservative induction schemas and may add symbols for particular functions. On the firstorder side, this leads to theories between the Robinson arithmetic and Peano arithmetic : The theory does not have any induction. has full mathematical induction for arithmetical formulas and has ordinal , meaning the theory lets one encode ordinals of weaker theories as recursive relation on just the naturals. Many of the well studied arithmetic theories are weak regarding proof of totality for some more fast growing functions. Some of the most basic examples of arithmetics include elementary function arithmetic , which includes induction for just bounded arithmetical formulas, here meaning with quantifiers over finite number ranges. The theory has a proof theoretic ordinal (the least not provenly recursive wellordering) of . The induction schema for arithmetical existential formulas allows for induction for those properties of naturals a validation of which is computable via a finite search with unbound (any, but finite) runtime. The schema is also classically equivalent to the induction schema. The relatively weak classical firstorder arithmetic which adopts that schema is denoted and proves the primitive recursive functions total. The theory is conservative over primitive recursive arithmetic . Note that the induction is also part of the secondorder reverse mathematics base system , its other axioms being plus comprehension of subsets of naturals. The theory is conservative over . Those last mentioned arithmetic theories all have ordinal .
Let us mention one more step beyond the induction schema. Lack of stronger induction schemas means, for example, that some infinite versions of the pigeon hole principle are unprovable. One relatively weak one being the Ramsey theorem type claim here expressed as follows: For any and coding of a coloring map , associating each with a color , it is not the case that for every color there exists a threshold input number beyond which is not ever the mappings return value anymore. Higher indirection as in induction for mere existential statements is needed to rewrite such a negation and prove it. Namely to rewrite it as the negation of the existence of a joint threshold number, depending on all the hypothetical 's, beyond which the function would still have to attain some color value. More specifically, the strength of the required bounding principle is strictly between the induction schema in and . For properties in terms of return values of functions on finite domains, brute force verification through checking all possible inputs has computational overhead which is larger the larger the size of the domain, but always finite. Acceptance of an induction schema as in validates the former so called infinite pigeon hole principle, which concerns unbounded domains, and so is about mappings with infinitely many inputs. In the classical context, this claim about coloring may be phrased positively, in terms of sets, as saying that there always exists at least one return value such that, in effect, for some infinite domain it holds that . In words, when provides infinite enumerated assignments, each being of one of different possible colors, then a particular coloring infinitely many numbers is claimed to exist and that the set can be specified. When read constructively, one would want to be concretely specifiable.
Higherorder classical arithmetics with low complexity comprehension are a relevant reference point for weaker set theories insofar as their language does not merely express arithmetical sets, while all sets of naturals particular such theories prove to exist are just computable sets. Constructive reverse mathematics, which lacks double negation elimination for undecidable sentences, exists as a field but is less developed than its classical counterpart.
Classical without the Powerset axiom is still consistent with all existing sets of reals being subcountable, and there even countable.^{[10]} Possible choice principles were discussed, a weakened form of the Separation schema was already adopted, and more of the standard axioms shall be weakened for a more predicative and constructive theory. The first one of those is the Powerset axiom, which is adopted in the form of the space of characteristic functions, itself tied to exactly the decidable subclasses. So consider the axiom .
Exponentiation 
The formulation here uses the convenient notation for function spaces. Otherwise the axiom is lengthier, characterizing using bounded quantifiers in the total function predicate. In words, the axiom says that given two sets , the class of all functions is, in fact, also a set. This is certainly required, for example, to formalize the object map of an internal homfunctor like .
Existence statements like Exponentiation, i.e. function spaces being sets, enable the derivation of more sets via bounded Separation. Adopting the axiom, quantification over the elements of certain classes of functions only ranges over a set, also when such function spaces are even classically uncountable. E.g. the collection of all functions where , i.e. the set of points underlying the Cantor space, is uncountable, by Cantor's diagonal argument, and can at best be taken to be a subcountable set. (In this section and beyond, the symbol for the semiring of natural numbers in expressions like is used, or written , just to avoid conflation of cardinal with ordinal exponentiation.) Roughly, classically uncountable sets tend to not have computably decidable equality.
Enumerable forms of the pigeon hole principle can now be proven, e.g. that on a finitely enumerable set, every injection is also a surjection. At last, all finitely enumerable sets are finite. The finitely enumerable union of a family of subfinite resp. subcountable sets is itself subfinite resp. subcountable.
For any countable family of counting functions together with their ranges, the theory proves the union of those ranges to be countable. Recall that not even classical (without countable choice) proves a countable union of countable sets to be countable, as this requires infinitely many existential instantiations of functions. With Exponentiation, the union of all finite sequences over a countable set is now a countable set.
With function spaces with the finite von Neumann ordinals as domains, we can model as discussed and can thus encode ordinals in the arithmetic. One then furthermore obtains the ordinalexponentiated number as a set, which may be characterized as . Relatedly, the set theory then also proves the existence of any primitive recursive function on the naturals , as set functions in the uncountable set .
As far as comprehension goes, the dependent or indexed products are now sets. The theory now proves the collection of all the countable subsets of any set (the collection is a subclass of the powerclass) to be a set.
The characterization of the class of all subsets of a set involves unbounded universal quantification, namely . Here has been defined in terms of the membership predicate above. So in a mathematical set theory framework, the power class is defined not in a bottomup construction from its constituents (like an algorithm on a list, that e.g. maps ) but via a comprehension over all sets. If is a set, that defining quantification even ranges over , which makes the axiom of powerset impredicative. The statement itself is .
The richness of the powerclass in a theory without excluded middle can best be understood by considering small classically finite sets. For any proposition , the class equals when can be rejected and (i.e. ) when can be proven, but may also not be decidable at all. Consider three different undecidable proposition, none of which provenly imply another. They can ben used to define three subclasses of the singleton , none of which are provenly the same. In this view, the powerclass of the singleton, usually denoted by , is called the truth value algebra and does not necessarily provenly have only two elements. The set of valued functions on a set injects into the function space and corresponds to just its decidable subsets.
It has been pointed out that the empty set and the set itself are of course two subsets of . Whether also is true in a theory is contingent on a simple disjunction:
So assuming for just bounded formulas, predicative Separation then lets one demonstrate that the powerclass is a set. With exponentiation, being a set already implies Powerset for sets in general. The proof is via replacement for the association of to , and an argument why all subsets are covered. So in this context, also full Choice proves Powerset. Moreover, with bounded excluded middle, is in bijection with . See also .
Full Separation is equivalent to just assuming that each individual subclass of is a set. Assuming full Separation, both full Choice and Regularity prove .
Relatedly, assuming in this theory, Set induction becomes equivalent to Regularity and Replacement becomes capable of proving full Separation.
While the theory does not exceed the consistency strength of Heyting arithmetic, adding Excluded Middle gives a theory proving the same theorems as classical minus Regularity! Thus, adding Regularity as well as either or full Separation to gives full classical . Adding full Choice and full Separation gives minus Regularity.
So this would thus lead to a theory beyond the strength of typical type theory.
So in this context with Exponentiation, function spaces are more accessible than classes of subsets, as is the case with exponential objects resp. subobjects in category theory. In category theoretical terms, the theory essentially corresponds to constructively wellpointed Cartesian closed Heyting pretoposes with (whenever Infinity is adopted) a natural numbers object. Existence of powerset is what would turn a Heyting pretopos into an elementary topos. Every such topos that interprets is of course a model of these weaker theories, but locally Cartesian closed pretoposes have been defined that e.g. interpret theories with Exponentiation but reject full Separation and Powerset. A form of corresponds to any subobject having a complement, in which case we call the topos Boolean. Diaconescu's theorem in its original topos form says that this hold iff any coequalizer of two nonintersecting monomorphisms has a section. The latter is a formulation of choice. Barr's theorem states that any topos admits a surjection from a Boolean topos onto it, relating to classical statements being provable intuitionistically.
In type theory, the expression "" exists on its own and denotes function spaces, a primitive notion. These types (or, in set theory, classes or sets) naturally appear, for example, as the type of the currying bijection between and , an adjunction. A typical type theory with general programming capability  and certainly those that can model , which is considered a constructive set theory  will have a type of integers and function spaces representing , and as such also include types that are not countable. This is just to say, or implies, that among the function terms , none have the property of being a bijection.
Constructive set theories are also studied in the context of applicative axioms.
In this section the strength of is elaborated on. For context, possible further principles are mentioned, which are not necessarily classical and also not generally considered constructive. Here a general warning is in order: When reading proposition equivalence claims in the computable context, one shall always be aware which choice, induction and comprehension principles are silently assumed. See also the related constructive analysis, feasible analysis and computable analysis.
Exponentiation implies recursion principles and so in , one can comfortably reason about sequences , their regularity properties such as , or about shrinking intervals in . So this enables speaking of Cauchy sequences and their arithmetic.
Any Cauchy real number is a collection of sequences, i.e. subset of a set of functions on . More axioms are required to always grant completeness of equivalence classes of such sequences and strong principles need to be postulated to imply the existence of a modulus of convergence for all Cauchy sequences. Weak countable choice is generally the context for proving uniqueness of the Cauchy reals as complete (pseudo)ordered field. The prefix "pseudo" here highlights that the order will, in any case, constructively not always be decidable.^{[11]}
As in the classical theory, Dedekind cuts are characterized using subsets of algebraic structures such as : The properties of being inhabited, numerically bounded above, "closed downwards" and "open upwards" are all bounded formulas with respect to the given set underlying the algebraic structure. A standard example of a cut, the first component indeed exhibiting these properties, is the representation of given by
(Depending on the convention for cuts, either of the two parts or neither, like here, may makes use of the sign .)
The theory given by the axioms so far validates that a pseudoordered field that is also Archimedean and Dedekind complete, if it exists at all, is in this way characterized uniquely, up to isomorphism. However, the existence of just function spaces such as does not grant to be a set, and so neither is the class of all subsets of that do fulfill the named properties. What is required for the class of Dedekind reals to be a set is an axiom regarding existence of a set of subsets and this is discussed further below in the section on Binary refinement. In a context without or Powerset, countable choice into finite sets is commonly assumed to prove the uncountability of the Dedekind reals.
Whether Cauchy or Dedekind reals, fewer statements about the arithmetic of the reals are decidable, compared to the classical theory.
Nonconstructive claims valuable in the study of constructive analysis are commonly formulated as concerning all binary sequences, i.e. functions . That is to say claims which are now set bound via "".
A most prominent example is the limited principle of omniscience , postulating a disjunctive property, like at the level of sentences or functions. (Example functions can be constructed in raw such that, if is consistent, the competing disjuncts are unprovable.) The principle is independent of e.g. introduced below. In that constructive set theory, implies its "weaker" version, itself implying the "lesser" version, denoted and . moreover implies Markov's principle , a form of proof by contradiction motivated by (unbound memory capacity) computable search, as well as the version of the fan theorem. Mention of such principles holding for sentences generally hint at equivalent formulations in terms of sequences, deciding apartness of reals. In a constructive analysis context with countable choice, is e.g. equivalent to the claim that every real is either rational or irrational  again without the requirement to witness either disjunct. The three omniscience principles are each equivalent to theorems of the apartness, equality or order of two reals in this way.
Here a list of some propositions employed in theories of constructive analysis that are not provable using just base intuitionistic logic. For example, see or even the anticlassical constructive Church's thesis principle for numbertheoretic functions as a postulate in the theory, or some of its consequences on the recursive mathematics side (variously called , or ). This is discussed below. On another end, there are Kripke's schema (turning all subclasses of countable), bar induction, the decidable fan theorem (which contradicts strong forms of Church's thesis), or even Brouwer's anticlassical continuity principle determining functions on unending sequences through finite initial segments, on the Brouwerian intuitionist side (). Both mentioned schools contradict , so that choosing to adopt certain of its laws makes the theory inconsistent with theorems in classical analysis. Those two schools are moreover not consistent with one another.
Through the relation between computability and the arithmetical hierarchy, insights in this classical study are also revealing for constructive considerations. A basic insight of reverse mathematics concerns computable infinite finitely branching binary trees. Such a tree may e.g. be encoded as an infinite set of finite sets
with decidable membership, and those trees then provenly contain elements of arbitrary big finite size. The so called Weak Kőnigs lemma states: For such , there always exists an infinite path in , i.e. an infinite sequence such that all its initial segments are part of the tree. In reverse mathematics, the secondorder arithmetic does not prove . To understand this, note that there are computable trees for which no computable such path through it exists. To prove this, one enumerates the partial computable sequences and then diagonalizes all total computable sequences in one partial computable sequences . One can then roll out a certain tree , one exactly compatible with the still possible values of everywhere, which by construction is incompatible with any total computable path.
In , the principle implies the nonconstructive lesser limited principle of omniscience . In a more conservative context, they are equivalent assuming  (a very weak countable choice). It is also equivalent to the Brouwer fixed point theorem and other theorems regarding values of continuous functions on the reals. The fixed point theorem in turn implies the intermediate value theorem, but be aware that the classical theorems can translate to different variants when expressed in a constructive context.^{[12]}
The concerns infinite graphs and so its contrapositive gives a condition for finiteness. Again to connect to analysis, over the classical arithmetic theory , the claim of is for example equivalent to the Borel compactness regarding finite subcovers of the real unit interval. A closely related existence claim involving finite sequences in an infinite context is the decidable fan theorem . Over , they are actually equivalent. In those are distinct, but, after again assuming some choice, here then implies .
In the following short remark function and claims made about them is again meant in the sense of computability theory: The μ operator enables all partial general recursive functions (or programs, in the sense that they are Turing computable), including ones e.g. nonprimitive recursive but total, such as the Ackermann function. The definition of the operator involves predicates over the naturals and so the theoretical analysis of functions and their totality depends on the formal framework and proof calculus at hand. This is highlighted because of the concern with axioms in theories other than arithmetic.
The predicate expressing a program to be total is famously computably undecidable. An anticlassical constructive Church's principle , expressed in the language of the theory, concerns those set functions and it postulates that they corresponds to computable programs. The natural numbers which are thought of as indices (for the computable functions which are total) in computability theory are in the arithmetical hierarchy. Which is to say it is still a subclass of the naturals and so this is, when put in relation to some classical function spaces, a conceptually small class. In this sense, adopting the postulate makes into a "sparse" set, as viewed from classical set theory. Subcountability of sets can also be postulated independently. is still consistent with some choice, but it contradicts classically valid principles such as and , which are amongst the weakest often discussed principles.
In set language, induction principles can read , with the antecedent defined as further above, and with meaning where is always the set of naturals. Via the strong axiom of Infinity and bounded Separation, the validity of induction for bounded definitions was already established.
At this point it is instructive to recall how set comprehension was encoding statements in predicate logic. For an example, given set , let denote the existential statement that a certain function space set exist, . Here the existential quantifier is not merely one over natural numbers or bounded by any other set. Now a proposition like this exponentiation claim, the claim and the subclass claim are just two ways of formulating the same desired statement, namely an indexed conjunction of existential propositions where spans over the set of all naturals. The second form is expressed using class notation involving a subclass comprehension that may not constitute a set, in which case many set axioms will not apply, so that establishing it as a theorem may not be possible. A set theory with just bounded Separation can thus also be strengthened by adopting arithmetical induction schemas for predicates beyond just the bounded ones.
The iteration principle for set functions mentioned in the section dedicated to arithmetic is also implied by the full induction schema over one's structure modeling the naturals (e.g. ). So for that theorem, granting a model of Heyting arithmetic, it represents an alternative to Exponentiation. The schema is often formulated in terms of predicates as follows:
Axiom schema of full mathematical induction: For any predicate on , 
Here the 0 denotes as above, and the set denotes the successor set of , with . By Axiom of Infinity above, it is again a member of .
The full induction schema is implied by the full Separation schema. As elaborated in the section on induction from infinity, here formulas in schemas are to be understood as formulas in firstorder set theory. And as stated in the section on Choice, induction principles are also implied by various forms of choice principles.
Full Set Induction in proves induction in transitive sets and so for transitive sets of transitive sets (which are the ordinals). This enables ordinal arithmetic. In particular, it proves full mathematical induction. Replacement is not required to prove induction over the set of naturals, but it is for their arithmetic modeled within the set theory.
It then reads as follows:
Axiom schema of Set induction: For any predicate , 
Here holds trivially and so this covers to the "bottom case" in the standard framework. The variant of the axiom just for bounded formulas is also studied independently and may be derived from other axioms.
The axiom allows definitions of class functions by transfinite recursion. The study of the various principles that grant set definitions by induction, i.e. inductive definitions, is a main topic in the context of constructive set theory and their comparatively weak strengths. This also holds for their counterparts in type theory.
The axiom of regularity is a single statement with universal quantifier over sets and not a schema. As show, it implies , and so is nonconstructive. Now for taken to be the negation of some predicate and writing for the class , induction reads
Via the contrapositive, set induction implies all instances of regularity but only with doublenegated existence in the conclusion. In the other direction, given enough transitive sets, regularity implies each instance of set induction.
This now covers variants of all of the eight Zermelo–Fraenkel axioms. Extensionality, Pairing, Union and Replacement are indeed identical. Infinity is stated in a strong formulation and implies Emty Set, as in the classical case. Separation, classically stated redundantly, is constructively not implied by Replacement. Without the Law of Excluded Middle, the theory here is lacking, in its classical form, full Separation, Powerset as well as Regularity. Adding at this point would already give . Replacement and Exponentiation can be further strengthened without losing a type theoretical interpretation and in a way that is not going beyond . Those two alterations are discussed next.
Like the axiom of regularity, set induction restricts the possible models of the membership relation "" and thus that of a set theory, as was the motivation for the principle in the 20's. The added prooftheoretical strength attained with Induction in the constructive context is significant, even if dropping Regularity in the context of does not reduce the prooftheoretical strength. Aczel was also one of the main developers or Nonwellfounded set theory, which rejects this last axiom.
Having discussed all the weakened form of axioms of , one can reflect upon the strength of the axiom of replacement, also in the context of the classical set theory. For any set and any natural , there exists the product recursively given by , which have ever deeper rank. Induction for unbound predicates proves that these sets exist for all of the infinitely many naturals. Replacement "for " now moreover states that this infinite class of products can be turned into the infinite set, . This is also not a subset of any previously established set.
Going beyond those axioms also seen in Myhill's typed approach, consider the discussed constructive theory with Exponentiation and Induction, but now strengthened by the collection schema. This is an alternative to the Replacement schema and indeed supersedes it, due to not requiring the binary relation definition to be functional, but possibly multivalued. The principle may be used in the constructive study of larger sets beyond the everyday need of analysis.
Axiom schema of Strong Collection: For any predicate , 
The axiom concerns a property for relations, giving rise to a somewhat repetitive format in its firstorder formulation. The antecedent states that one considers relation between sets and that are total over a certain domain set , that is, has at least one "image value" for every element in the domain. This is more general than an inhabitance condition in a choice axiom, but also more general than the condition of Replacement, which demands unique existence . In the consequent, firstly, the axioms states that then there exists a set which contains at least one "image" value under , for every element of the domain. Secondly, in this axioms formulation it then moreover states that only such images are elements of that new codomain set . It is guaranteeing that does not overshoot the codomain of and thus the axiom is also expressing some power akin to a Separation procedure. The axiom may be expressed as saying that for every total relation, there exists a set such that the relation is total in both directions.
This theory without , without unbounded separation and without "naive" Power set enjoys various nice properties. For example, as opposed to with its subset collection schema below, it has the existence property.
One may approach Power set further without losing a type theoretical interpretation. The theory known as is the axioms above plus a stronger form of Exponentiation. It is by adopting the following alternative, which can again be seen as a constructive version of the Power set axiom:
Axiom schema of Subset Collection: For any predicate , 
An alternative that is not a schema is elaborated on below.
For given and , let be the class of all total relations between and . This class is given as
As opposed to the function definition, there is no unique existence quantifier in . The class represents the space of "nonuniquevalued functions" or "multivalued functions" from to , but as set of individual pairs with right projection in , and only those.
One does not postulate to be a set, since with Replacement one can use this collection of relations between a set and the finite , i.e. the "bivalued functions on ", to extract the set of all its subsets. In other words being a set would imply the Powerset axiom.
Over , there is a single, somewhat clearer alternative axiom to the Subset Collection schema. It postulates the existence of a sufficiently large set of total relations between and .
Axiom of Fullness: 
This says that for any two sets and , there exists a set which among its members inhabits a still total relation for any given total relation .
On a given domain , the functions are exactly the sparsest total relations, namely the unique valued ones. Therefore, the axiom implies that there is a set such that all functions are in it. In this way, Fullness implies Exponentiation. The Fullness axiom is in turn also implied by the socalled Presentation Axiom about sections, which can also be formulated category theoretically.
The so called binary refinement axiom says that for any there exists a set such that for any covering , the set holds two subsets and that also do this covering job, . It is a weakest form of the powerset axiom and at the core of some important mathematical proofs. Fullness for relations between the set and the finite implies that this is indeed possible.
Taking another step back, plus Recursion and plus Binary refinement already proves that there exists an Archimedean, Dedekind complete pseudoordered field. That set theory also proves that the class of left Dedekind cuts is a set, not requiring Induction or Collection. And it moreover proves that function spaces into discrete sets are sets (there e.g. ), without assuming . Already over the weak theory (which is to say without Infinity) does binary refinement prove that function spaces into discrete sets are sets, and therefore e.g. the existence of all characteristic function spaces .
The bounded notion of a transitive sets of transitive sets is a good way to define ordinals and enables induction on ordinals. With this, in , assuming that membership of is decidable in all successor ordinals proves for bounded formulas. Also, neither linearity of ordinals, nor existence of power sets of finite sets are derivable in this theory, as assuming either implies Power set. The theory does not prove that all function spaces formed from sets in the constructible universe are sets inside , and this holds even when assuming Powerset instead of the weaker Exponentiation axiom. So such theories do not prove to be a model of