Axiomatic 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 set bounded, motivated by results tied to impredicativity.
YouTube Encyclopedic

1/5Views:15 2208 128134 96736 89038 438

Five Stages of Accepting Constructive Mathematics  Andrej Bauer

Intuitionism and Constructive Mathematics 1/19

Lecture 1: Sets, Set Operations and Mathematical Induction

How To Figure Out Math Proofs On Your Own

Set Representation
Transcription
Introduction
Constructive outlook
Preliminary on the use of intuitionistic logic
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 claim decidability of such (and/or ) in the sense that they prove excluded middle for (resp. the statement using the quantifier above) without demonstrating the truth of either side of the disjunction(s). This is often the case in classical logic. In contrast, axiomatic theories deemed constructive tend to not permit many classical proofs of statements involving properties that are provenly computationally undecidable.
The law of noncontradiction is a special case of the propositional form of modus ponens. Using the former with any negated statement , 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.
The intuitionistic logic underlying the set theories discussed here, unlike 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.
For any only classically valid , or even , it is worth trying to establish it in its classically equivalent form . For a special case, the counterexample existence claim 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.
More generally, constructive mathematical theories tend to prove classically equivalent reformulations of classical theorems. For example, in constructive analysis, one cannot prove the intermediate value theorem in its textbook formulation, but one can prove theorems with algorithmic content that, as soon as double negation elimination and its consequences are assumed legal, are at once classically equivalent to the classical statement. The difference is that the constructive proofs are harder to find.
Imposed restrictions on a set theory
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 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 extensionality, 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 the development of a genuinely intuitionistic set theory also requires reconsideration of choice principles and the rewording of some standard axioms to classically equivalent ones. Apart from demands for computability and reservations regrading of impredicativity, technical question regarding which nonlogical axioms effectively extend the underlying logic of a theory is also a research subject in its own right.
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 or . Also the real line may be taken to be indecomposable in this sense. Undecidability of disjunctions also affects the claims about total orders such as that of all ordinal numbers, expressed by the provability and rejection of the clauses in the order defining disjunction . This determines whether the relation is trichotomous. A weakened theory of ordinals in turn affects the proof theoretic strength defined in ordinal analysis.
In exchange, constructive set theories can exhibit attractive disjunction and existence properties, as is familiar from the study of constructive arithmetic theories. These are features of a fixed theory which metalogically relate judgements of propositions provable in the theory. Particularly 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.^{[1]}
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 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 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
To motivate the discussion, here one must carefully distinguish between provable implications between two propositions, , and metalogical properties of the form . For an example of the latter that was mentioned above, a constructive theory may exhibit the numerical existence property, , for some number and where denotes the corresponding numeral in the formal theory. More broadly, 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, here captured via and , one established the existence of a number so that . When adopting any such schema as an inference rule and nothing new can be proven, one says the theory is closed under that rule.
Coming back to just , adjoining the excluded middle principle to , the theory obtained in that way may prove new, strictly classical statements for some , 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 (in the sense of "") 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 . To name an example for this circumstance: Church's rule is an admissible rule in firstorder Heyting arithmetic and the corresponding Church's thesis principle may be adopted. The same is not possible in , also known as Peano arithmetic .
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 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 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 (in the set theory sense) do exist that cannot be captured by a Turing machine. Taking the computable world seriously as ontology, a prime example of an 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 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 decision problems. Motivated by provenly computably undecidable problems, one may reject the possibility of decidability of a predicate without also making any existence claim in . 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 strictly 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.
History and overview
Historically, the subject of constructive set theory (often also "") begun with John Myhill's work on the theories also called and .^{[2]} 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 ,^{[3]} 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.^{[4]} 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.
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 .
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,^{[5]} as also 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.
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.
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.^{[6]}^{[7]} Realizability models of within the effective topos have been identified, which, say, at once validate full Separation and Markov's principle , as well as relativized dependent choice , but also the subcountability of all sets and Church's thesis in the formulation for all predicates.^{[8]}
Subtheories of ZF
Notation
Language
The propositional connective symbols used to form syntactic formulas are standard. The axioms of set theory give a means to prove equality "" 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 "". However, in a context with apartness relations, for example when dealing with sequences, the latter symbol is also used for something different.
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 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.
Two ways to express disjointness capture many of the intuitionistically valid negation rules: . Using the above notation, this is a purely logical equivalence and below the proposition will furthermore be expressible as .
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 .
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.
Classes
As is also common in the study of set theories, one makes use set builder notation for classes, which, in most contexts, are not part of the object language but used for concise discussion. In particular, one may introduce notation declarations of the corresponding class via "", for the purpose of expressing 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 . Further extensions of such notation are in common used in set theory, giving meaning to statements like "", and so on.
For a predicate , trivially . And so follows that .
Through the use of a 2ary predicate , a set may be characterized as holding for all , where the right hand side may depend on the actual variable , and possibly even on membership in itself. The convenient notational relation between and functions akin to a simpler, special case of this.
Equality
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.
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 predicate 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.
Merging sets
Define class notation for a few given elements via disjunctions, e.g. says . Denote by the standard ordered pair model , so that e.g. denotes another bounded formula in the formal language of the theory.
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 minimal such set is the union. With predicative Separation below, the two axioms together imply the existence of a binary union of two classes and , when they have been established to be sets, denoted by or . The two axioms may also be formulated stronger in terms of "". In the context of this is not necessary.
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 notation is also used for classes. Let . Given , the decidability of membership in , i.e. the potentially independent statement , can also be expressed as . This goes to show that partitioning is also a more involved notion, constructively. But as for any excluded middle statement, is not uninhabited by .
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 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.
For a set , define the successor set as and write for . Its interplay with the membership relation has a recursive clause, in the sense that . By reflexivity of equality, , and in particular is always inhabited. A sort of blend between pairing and union, an axiom more readily related to the successor is the Axiom of adjunction.^{[9]}^{[10]} This is all 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.
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 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 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 . 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 (also denoted ). 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.
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 the proposition (in the model of the naturals this means being smaller than because, equivalently, ), while is equivalent to (so that, equivalently, ). 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. Another way to express excluded middle for is as the existence of a least number member of the inhabited class . If ones 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 understood to be rich. Unsurprisingly, decidable propositions have one of a binary set of truth values.
The axiom schema of Predicative Separation is also called Bounded Separation, as in Separation for setbounded quantifiers only. The scope of specified subsets that can be proven to exist is enriched with further set existence postulate. Bounded Separation is a schema that takes into account syntactic aspects of set defining predicates, up to provable equivalence. The permitted formulas are 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. 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 Mac Lane weakens a system close to Zermelo set theory , for mathematical foundations related to topos theory. See also KripkePlatek set theory.
No universal set
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 on the right is not a set. The following demonstrates this in the special case when is empty, i.e. when the right side is the universal class.
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.
Predicativity
The restriction in the axiom is also gatekeeping impredicative definitions: Existence should at best not be claimed for objects that are not explicitly describable, or whose definition involves themselves or reference to a proper class, such as when a property to be checked involves a universal quantifier. So in a constructive theory without Axiom of power set, when 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.
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.
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 is relevant for function comprehension 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 existence properties of a theory, as discussed further below.
The discussion now proceeds with axioms granting existence of objects which, in different but related form, are also found in dependent type theories, namely products and the collection of natural numbers as a completed set. Infinite sets are particularly handy to reason about operations applied to sequences defined on unbounded domains, say the formal differentiation of a generating function or the addition of two Cauchy sequences.
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 to denote the now unique smallest inductive set, an unbounded 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. That said, existence of a least element for the inhabited subset implies excluded middle for , and a constructive theory will therefore not prove to be wellordered.
Weaker formulations of infinity
Should it need motivation, the handyness 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, no two 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 or the 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
 .
For a class , the 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 .
Functions
Finiteness
The function concept will be specified right below. Tying in with the previous section first, here are some definitions.
One defines three distinct notions involving surjections. For a general set to be (Bishop)finite shall mean there is a bijective function to a natural. If the existence of such a bijection is proven impossible, the set is called nonfinite. Secondly, for a notion weaker than finite, to be finitely indexed (or Kuratowskifinite) shall mean that there is a surjection from a von Neumann natural number onto it. Call a set subfinite if it is the subset of a finite set, which thus injects into that finite set. Thirdly, for a notion even weaker than finitely indexed, to be subfinitely indexed means to be in the surjective image of a subfinite set, and in this just means to be the subset of a finitely indexed set, meaning the subset can also be taken on the image side instead of the domain side. A set exhibiting either of those three notions can be understood to be majorized by a finite set, but in the second case the relation between the sets members is not necessarily fully understood, and in the third not even membership with respect to some superset it is necessary fully understood. The claim that being finite is equivalent to being subfinite, for all sets, is equivalent to . More finiteness properties can be defined, e.g. one expressing the existence of some large enough natural such that all functions into a set fail to be injective, for some notion of noninjectivity.
More generally than the property of infinitude above, call a set infinite if one can inject into it. Call an inhabited set countable if there exists a surjection from onto it and subcountable if this can be done from a subsets of . Call a set enumerable if there exists an injection to , which renders the set discrete. Notably, all of these are function existence claims. The empty set is not inhabited but generally deemed countable too, and note that the successor set of any countable set is countable. The set itself is clearly unbounded and not finite in any sense. It is also trivially infinite, countable and enumerable, as witnessed by the identity function. An infinite, countable sets is equinumeros to . Observe that , unlike any of its members, is equinumeros to infinitely many of its proper unbounded subsets, e.g. those of the form . This makes the set Dedekindinfinite. More properties of finiteness may be defined as negations of such properties, et cetera.
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, et cetera. A surjective map may also be called an enumeration.
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 maybe 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 model of computation, and this is a priori narrower than what is discussed in the present set theory context. One notion of program is formalized by partial recursive "functions" in computability theory. But beware that here the word "function" is used in a way that also comprises partial functions. The scare quotes are used for clarity here, as in a set theory context there is technically no need to speak of total functions, because this requirement is part of the definition of a set theoretical function and partial function spaces can be modeled via unions. At the same time, when combined with a formal arithmetic, this notion provides one particularly sharp notion of totality for functions. By Kleene's normal form theorem, each partial recursive function on the naturals computes, for the values where it terminates, the same as , for some function index , and any index will constitute some partial function. A program can be associated with a and may be said to be total whenever a theory proves , where amounts to a primitive recursive program and is related to the execution of . Kreisel proved that the class of partial recursive functions proven total by is not enriched when is added.^{[11]} As a predicate in , this totality constitutes an undecidable subset indices, highlighting that that the recursive world of functions between the naturals is already captured by a set dominated by . As a third warning, note that this notion is really about programs and several indices will in fact constitute the same function, in the extensional sense.
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. And given a correctly representing , the predicate defined by represents the recursive function just as well, and as this 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 prove the graph to be total functional.^{[12]}
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.
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 . By construction, such functions respect equality in the sense that , for any inputs from . This is worth mentioning since also more broader concepts of "operations" exist in the literature, which may not respect this. And as noted, 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. Variants of the functional predicate definition using apartness relations on setoids have been defined as well. 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. Some notational conveniences involving function application will only work when a set has indeed been established to be a function.
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 Replacement axiom.) That is, the mapping information exists as set and it has a pair for each element in the domain. Of course for any set from some class, there is always the unique element of the singleton , and so merely a chosen range being a set does not suffice to be granted a function set. In summary, in the set theory context the focus is on capturing particular total relations that are functional. To delineate the notion of function in the theories of the previous subsection (a 2ary logical predicate defined to express a functions graph, together with a proposition that it is total and functional) from the "material" set theoretical notion here, one may explicitly call the latter graph of a function, anafunction or set function. The axiom schema of Replacement can also be formulated in terms of the ranges of such set functions.
If both domain and codomain are sets, then the above predicate only involves bounded quantifiers. Common notions such as injectivity and surjectivity can be expressed in a bounded fashion as well, and thus so is bijectivity. Both of these tie in to notions of size. Importantly, injection existence between any two sets provides a preorder. A power class does not inject into its underlying set and the latter does not map onto the former. Surjectivity is formally a more complex definition. Note that injectivity shall be defined positively, not by its contrapositive, which is common practice in classical mathematics. The version without negations is sometimes called weakly injective. The existence of value collisions is a strong notion of noninjectivity. And regarding surjectivity, similar considerations exist for outlierproduction in the codomain.
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 above, the membership proposition is also written . The booleanvalued are among the classes discussed next.
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 .^{[13]} 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 set so that
and then by convention and 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.
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 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, 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 .
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, bounded set . With as above, it follows that
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, pseudoboundedness using the above counting sequence provides a bound for all the elements .
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 defined that negate the countability of such a countable union of pairs. Assuming countable choice rules out that model as an interpretation of the resulting theory. This principle is independent of  A naive proof strategy for that statement fails at the accounting of infinitely many existential instantiations.
A choice principle postulates that certain selections can always be made in a joint fashion so that they are also manifested as a single set function in the theory. Such a function existence claim can then 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. As with any independent axiom, this raises the proving capabilities while restricting the scope of possible (modeltheoretic) interpretations of the (syntactic) theory. The constructive development here proceeds in a fashion agnostic to any discussed choice principles, but here are well studied variants:^{[14]}
 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. This is not provable on the base of . Countable choice into general sets can also be weakened further. One may consider the version of countable choice for functions into (called ), as is implied by , i.e. by postulating that all total arithmetical relations are recursive. 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 (). Constructively, weak form of choice is required for wellbehaved Cauchy reals. 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, it become equivalent to the nonconstructive principle of more logical flavor, . Countable choice is not valid in the internal logic of a general topos, which can be seen as models of constructive set theories.
 Axiom of dependent choice : Countable choice is implied by the more general axiom of dependent choice, extracting a function from any entire relation on an inhabited set. Countable choice is akin to constructive Church's thesis principle and indeed dependent choice holds in many realizability models and it is thus adopted in many constructive schools.
 Relativized dependent choice : The stronger relativized dependent choice principle is a variant of it  a schema involving an extra predicate variable. Adopting this for just bounded formulas in , the theory already proves the induction.
 : 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 principle over that holds in the type theoretical interpretation .
 Axiom of choice : The 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. Striking existence claims beyond what could be defined in are abound: For example, applied to the Borel algebra of the reals, the axiom postulates the existence of a function selecting a member from each nonempty such Lebesguemeasurable subset. (The set is the σalgebra generated by the finite intervals . It strictly includes those intervals, in the sense of , but in also only has the cardinality of the reals itself.) The axiom of choice also implies Dependent choice. Critically in the present context, it moreover also implies instances of via Diaconescu's theorem. For theories extending this means full choice at the very least proves for all formulas, a nonconstructive consequence not acceptable from a computability standpoint.
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. 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 . But otherwise, the classes and are as contingent as the proposition involved in their definition and they are not proven finite. Nonetheless, the setup entails several consequences, when inspecting the provable case, starting with . So validity of means and share all members and there are two of them and indeed the equality is equivalent and decides . As are are then sets, and . Similarly, and, as provenly , one actually finds in which way the sets are then different. A contrapositive thus gives . One may moreover reason using the disjunctive syllogism that both and are each equivalent to . All together, this gives equivalence of disjuncts
 .
In the following assume a context in which are indeed 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, but the possible function return values are known to be just or . Using the distributivity, there arises a list of conditions, 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 proposition .
Analysis of Diaconescu's theorem
So full choice is nonconstructive in set theory as defined here. The issue is that propositions, as part of set comprehension used to separate and define the classes and from , ramify the notion of truth values 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 predicate to information about function values. To recap 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 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. 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.
The surjection witnesses that is finitely indexed. To better understand why we cannot expect to be granted a definitive (total) choice function with domain , consider naive function candidates. It was noted that its members are subfinite and also inhabited, since regardless of it is the case that and . 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 explicitly 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 not proven finite. 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 (which is not proven finite either) with the subfinite wouldbe natural . In , the proposition (in the "ifclause") may be replaced by . As , postulating , or , or the classical principle here would indeed imply that is a natural, so that the latter set constitutes a choice function into . 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 . Such a had already been considered in the early section on the axiom of separation. Again, the latter here is a classical choice function either way also. Constructively, the domain and values of such dependent wouldbe functions are not understood enough to prove them to be a total functional relation into .
For computable semantics, set theory axioms postulating (total) function existence lead to the requirement for halting recursive functions. From their function graph in individual interpretations, one can infer the branches taken by the "ifclauses" that were undecided in the interpreted theory. But on the level of the synthetic frameworks, when they broadly become classical from adopting full choice, these extensional set theories theories contradict the constructive Church's rule.
Regularity implies PEM
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 assumes Separation applies to and uses , for which it was already explained that and for which by definition. This is defined using the clause , so that any given fulfills the disjunction . Now let be the postulated member with the empty intersection property. If , then , while otherwise . This establishes excluded middle for .
Demanding that the set of naturals is wellordered with respect to it standard order relation imposes the same condition on the inhabited set . So the least number principle has the same nonconstructive implication.
Arithmetic
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, for any quantifierfree formula on the naturals, such as ,
 .
The firstorder theory of Heyting arithmetic has the same signature and nonlogical axioms as Peano arithmetic. In contrast, the signature of set theory does not contain addition "" or multiplication "". Next, it is clarified which set theory axiom may be asserted to prove existence of the latter as a function set, together with their desired relation to zero and successor.
Recursion
The set theory axioms listed so far suffice as formalized framework for a good portion of basic mathematics. Even without an induction principle for general classes, many universally quantified statements can still be proven per particular set term (e.g. some particular function). That said, the constructive set theory does actually not even enable primitive recursion in for function definitions of what would be (where "" here denotes the Cartesian product of set, not to be confused with multiplication above). 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, and are wellfounded, in the sense of the inductive subsets formulation. Further, 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 form sets themselves, which may be written as
This is modest, insofar as a collection of functions from finite domains into sets are e.g. countable in . Notably, adoption of such axioms has genuine set theoretical flavor, in contrast to a direct embedding arithmetic principles into our theory. It may further motivate the discussion of a stronger such exponentiation axiom below. This more set theoretical axiom will, however, still not prove the full induction schema for formulas with quantifiers over sets.
Moderate induction in ECST
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 sets can be read as corresponding to predicates and the consequent states that all fulfill said predicate. Defining subsets of , the theory proves induction for all predicates involving only setbounded quantifiers, and so with it also induction as in .
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.
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 firstorder arithmetic, namely predicates of just numbers. So to interpret the axiom schema of , one interprets these arithmetical formulas. In that context, the bounded quantification specifically means quantification over a finite range of numbers. 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. When discussing the strength of axioms concerning numbers, it is also important to keep in mind that the arithmetical and the set theoretical framework do not share a common signature. Likewise, care must always be taken with insights about totality of functions. In 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.
In the program of reverse mathematics, all mathematical objects discussed are encoded as naturals or subsets of naturals. Secondorder arithmetic theories with very low complexity comprehension have a language that does not merely express arithmetical sets, while all sets of naturals particular such theories prove to exist are just computable sets. Theorems therein can be a relevant reference point for weak set theories with a set of naturals, predicative separation and only some further restricted form of induction. Constructive reverse mathematics exists as a field but is less developed than its classical counterpart.^{[15]}
Induction without infinite sets
Before discussing even classically uncountable sets, this last section takes a step back to a context more akin to . The addition of numbers, considered as relation on triples, is an infinite collection, just like collection of natural numbers themselves. But note that induction schemas may be adopted (for sets, ordinals or in conjunction with a natural number sort), without ever postulating that the collection of naturals exists as a set. As noted, Heyting arithmetic is biinterpretable with such a constructive set theory, in which all sets are postulated to be in bijection with an ordinal. The BIT predicate is a common means to encode sets in arithmetic.
This paragraph lists a few weak natural number induction principles studied in the proof theory of arithmetic theories with addition and multiplication in their signature. This is the framework where these principles are most well understood. The theories may be defined via bounded formulations or variations on induction schemas that may furthermore only allow for predicates of restricted complexity. On the classical 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. Theories may also include additional symbols for particular functions. 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. (In the classical context and in terms of sets, this claim about coloring may be phrased positively, 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, it is claimed that a particular coloring infinitely many numbers always exists and that the set can thus be specified, without even having to inspect properties of . When read constructively, one would want to be concretely specifiable and so that formulation is a stronger claim.) Higher indirection, than in induction for mere existential statements, is needed to formally reformulate such a negation (the Ramsey theorem type claim in the original formulation above) and prove it. Namely to restate the problem in terms of the negation of the existence of one 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.
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.
Exponentiation
Classical without the Powerset axiom is still consistent with all existing sets of reals being subcountable, and there even countable.^{[16]} 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. Roughly, classically uncountable sets tend to not have computably decidable equality. Vanilla intuitionistic mathematics does not prove a function space like to be not enumerable. (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.)
On countable sets
Enumerable forms of the pigeon hole principle can now be proven, e.g. that on a finitely indexed set, every autoinjection is also a surjection. At last, the finitely indexed discrete sets are just the finite sets. In particular, finitely indexed subsets of are finite. Cartesian products of finitely indexed sets is finitely indexed. The finitely indexed union of a family of subfinitely indexed resp. subcountable sets is itself subfinitely indexed resp. subcountable. These do not hold in , but not all of these need full Exponentiation to be validated.
With Exponentiation, the union of all finite sequences over a countable set is now a countable set. For any countable family of counting functions together with their ranges, the theory proves the union of those ranges to be countable. In contrast, not assuming countable choice, even is consistent with the uncountable set being the union of a countable set of countable sets.
The set theory now proves the existence of any primitive recursive function in , and in particular in the uncountable function spaces out of . Indeed, with function spaces and the finite von Neumann ordinals as domains, we can model as discussed, and thus encode ordinals in the arithmetic. One then furthermore obtains the ordinalexponentiated number as a set, which may be characterized as , the counted set of words over an infinite alphabet.
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 class of subsets of 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 , consider the subclass of (i.e. or ). It equals when can be rejected and it equals (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.
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.
The set , of functions taking values in (i.e. ) on a set , injects into the function space and corresponds to just the decidable subsets of . If the theory proves above a set (as for example unconditionally does), then the subset of is a function with . To claim that is to claim that excluded middle holds for .
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. And so in this context, also full Choice proves Powerset. Moreover, with bounded excluded middle, is in bijection with . See also the discussion of below.
Full Separation is equivalent to just assuming that each individual subclass of is a set. Assuming full Separation, both full Choice and Regularity prove .
Assuming in this theory, Set induction becomes equivalent to Regularity and Replacement becomes capable of proving full Separation.
Metalogic
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.
Category and type theoretic notions
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 surjection.
Constructive set theories are also studied in the context of applicative axioms.
Analysis
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.
The theory proves uniqueness of Archimedean, Dedekind complete (pseudo)ordered fields, with equivalence by a unique isomorphism. The prefix "pseudo" here highlights that the order will, in any case, constructively not always be decidable. This result is relevant assuming complete such models exist as sets.
Cauchy sequences
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. This is also the approach to analysis taken in secondorder arithmetic.
Cauchy reals
Any Cauchy real number is a collection of sequences, i.e. subset of a set of functions on constructed with respect to an equivalence relation. Even in the strong theory with a strengthened form of Collection, the Cauchy reals are poorly behaved when not assuming a form of countable choice, and suffices for most results. This concerns completeness of equivalence classes of such sequences, existence of a modulus of convergence for all Cauchy sequences and the preservation of such a modulus when taking limits.^{[17]}An alternative approach that is slightly better behaved is to work a collection of Cauchy reals together a choice of modulus, i.e. not with just the real numbers but with a set of pairs, or even with a fixed modulus shared by all real numbers.
Towards the Dedekind reals
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 Pseudoorderpseudoordered 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 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.
Constructive schools
Most schools for constructive analysis validate some choice and also , as defined in the second section on number bounds. Here are some other propositions employed in theories of constructive analysis that are not provable using just base intuitionistic logic:
 On the recursive mathematics side (the "Russian" or "Markovian" constructive framework with many abbreviations, e.g. ), first one has Markov's principle , which is a form of proof by contradiction motivated by (unbound memory capacity) computable search. This has notable impact on statements about real numbers, as touched upon below. In this school one further even has the anticlassical constructive Church's thesis principle , generally adopted for numbertheoretic functions. Church's thesis principle expressed in the language of set theory and formulated for set functions postulates that these all correspond to computable programs that eventually halt on any argument. In computability theory, the natural numbers corresponding to indices of codes of the computable functions which are total are in the arithmetical hierarchy, meaning membership of any index is affirmed by validating a proposition. This is to say that such a collection of functions is still a mere subclass of the naturals and so is, when put in relation to some classical function spaces, conceptually small. In this sense, adopting postulate makes into a "sparse" set, as viewed from classical set theory. Subcountability of sets can also be postulated independently.
 So on another end, on the Brouwerian intuitionist side (), there are bar induction, the decidable fan theorem saying decidable bars are uniform, which are amongst the weakest often discussed principles, Kripke's schema (with countable choice turning all subclasses of countable), or even Brouwer's anticlassical continuity principle, determining return values of what is established a function on unending sequences already through just finite initial segments.
Certain laws in both of those schools contradict , so that choosing to adopt all principles from either school disproves theorems from classical analysis. is still consistent with some choice, but contradicts the classical and , explained next. The independence of premise rule with set existence premises is not fully understood, but as a number theoretic principle it is in conflict with the Russian school axioms in some frameworks. Notably, also contradicts , meaning the constructive schools also cannot be combined in full. Indeed, some of the principles cannot be combined constructively simply because they together imply forms of , for example plus the countability of all subsets of the naturals. These combinations are then naturally also not consistent with further anticlassical principles.
Nonconstructive principles
Of course and many principles defining intermediate logics are nonconstructive. and , which is for just negated propositions, can be presented as De Morgan's rules. This section shall instead be concerned with statements in terms of predicates  especially weaker ones, expressed in terms of a few quantifiers over sets, on top of decidable predicates on numbers. Referring back to the section on characteristic functions, one may call a collection searchable if it is searchable for all its decidable subsets . This is a form of  for . Note that in the context of Exponentiation, such proposition on sets are now setbound.
Nonconstructive claims particularly valuable in the study of constructive analysis are commonly formulated as concerning all binary sequences, the characteristic functions on the arithmetic domain . Examples of famous sentences that are of Goldbach type, i.e. can be written down in this fashion, are the Goldbach conjecture, Fermat's last theorem but also the Riemann hypothesis. In raw , example functions can be defined on such that if is consistent, the competing  disjuncts, of low complexity, are unprovable.
More generally, the arithmetic , a most prominent nonconstructive, essentially logical statement goes by the name limited principle of omniscience . In the constructive set theory introduced below, it implies , , the version of the fan theorem, but also discussed below. postulates a disjunctive property, as does the weaker decidability statement for functions being constant (sentences) , the arithmetic . The two are related in a similar way as is versus and they essentially differ by . in turn implies the socalled "lesser" version . This is the (arithmetic) version of the nonconstructive De Morgan's rule for a negated conjunction. There are, for example, models of the strong set theory which separate such statements, in the sense that they may validate but reject .
Disjunctive principles about sentences generally hint at equivalent formulations deciding apartness in analysis in a context with mild choice or . The claim expressed by translated to real numbers is equivalent to the claim that either equality or apartness of any two reals is decidable (it in fact decides the trichotomy). It is then also equivalent to the statement that every real is either rational or irrational  without the requirement for or construction of a witness for either disjunct. Likewise, the claim expressed by for real numbers is equivalent that the ordering of any two reals is decidable (dichotomy). It is then also equivalent to the statement that if the product of two reals is zero, then either of the reals is zero  again without a witness. Indeed, formulations of the three omniscience principles are then each equivalent to theorems of the apartness, equality or order of two reals in this way. Yet more can be said about the Cauchy sequences that are augmented with a modulus of convergence.
A famous source of computable undecidability  and in turn also of a broad range of undecidable propositions  is the predicate expressing a computer program to be total.
Infinite trees
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őnig's 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 constr