Constructive set theory
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.
Introduction[edit]
Constructive outlook[edit]
Preliminary on the use of intuitionistic logic[edit]
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.
More generally, constructive mathematical theories tend to prove classically equivalent reformulations of classical theorems. For example, in constructive analysis, one cannot prove the intermediate value theorem in its textbook formulation, but one can prove theorems with algorithmic content that, as soon as double negation elimination and its consequences are assumed legal, are at once classically equivalent to the classical statement. The difference is that the constructive proofs are harder to find.
The intuitionistic logic underlying the set theories discussed here, unlike minimal logic, still permits double negation elimination for individual propositions for which excluded middle holds. In turn the theorem formulations regarding finite objects tends to not differ from their classical counterparts. Given a model of all natural numbers, the equivalent for predicates, namely Markov's principle, does not automatically hold, but may be considered as an additional principle.
In an inhabited domain and using explosion, the disjunction implies the existence claim , which in turn implies . Classically, these implications are always reversible. If one of the former is classically valid, it can be worth trying to establish it in the latter form. For the special case where is rejected, one deals with a counterexample existence claim , which is generally constructively stronger than a rejection claim : Exemplifying a such that is contradictory of course means it is not the case that holds for all possible . But one may also demonstrate that holding for all would logically lead to a contradiction without the aid of a specific counterexample, and even while not being able to construct one. In the latter case, constructively, here one does not stipulate an existence claim.
Imposed restrictions on a set theory[edit]
Compared to the classical counterpart, one is generally less likely to prove the existence of relations that cannot be realized. A restriction to the constructive reading of existence apriori leads to stricter requirements regarding which characterizations of a set involving unbounded collections constitute a (mathematical, and so always meaning total) function. This is often because the predicate in a casewise wouldbe definition may not be decidable. 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 existence claim, as shown below. The latter has a classically equivalent inductive substitute. So a genuinely intuitionistic development of set theory requires the rewording of some standard axioms to classically equivalent ones. Apart from demands for computability and reservations regrading of impredicativity, technical question regarding which nonlogical axioms effectively extend the underlying logic of a theory is also a research subject in its own right.
Metalogic[edit]
With computably undecidable propositions already arising in Robinson arithmetic, even just Predicative separation lets one define elusive subsets easily. In stark contrast to the classical framework, constructive set theories may be closed under the rule that any property that is decidable for all sets is already equivalent to one of the two trivial ones, or . Also the real line may be taken to be 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[edit]
As mentioned above, a constructive theory may exhibit the numerical existence property, , for some number and where denotes the corresponding numeral in the formal theory. Here one must carefully distinguish between provable implications between two propositions, , and metalogical properties of the form . When adopting an established proof theoretical schema of the latter type as an inference rule and nothing new can be proven, one says the theory is closed under that rule.
One may instead consider adjoining the rule corresponding to the metatheoretical property as an implication (in the sense of "") to , as a schema or in quantified form. A situation commonly studied is that of a fixed exhibiting the metatheoretical property of the following type: For an instance from some collection of formulas of a particular form, here captured via and , one established the existence of a number so that . Here one may then postulate , where the bound is a number variable in language of the theory. For example, Church's rule is an admissible rule in firstorder Heyting arithmetic and, furthermore, the corresponding Church's thesis principle may consistently be adopted as an axiom. The new theory with the principle added is anticlassical, in that it may not be consistent anymore to also adopt . Similarly, adjoining the excluded middle principle to some theory , the theory thus obtained may prove new, strictly classical statements, and this may spoil some of the metatheoretical properties that were previously established for . In such a fashion, may not be adopted in , also known as 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 here read
Kleene's T predicate together with the result extraction expresses that any input number being mapped to the number is, through , witnessed to be a computable mapping. Here now denotes a set theory model of the standard natural numbers and is an index with respect to a fixed program enumeration. Stronger variants have been used, which extend this principle to functions defined on domains of low complexity. The principle rejects decidability for the predicate defined as , expressing that is the index of a computable function halting on its own index. Weaker, double negated forms of the principle may be considered too, which do not require the existence of a recursive implementation for every , but which still make principles inconsistent that claim the existence of functions which provenly have no recursive realization. Some forms of a Church's thesis as principle are even consistent with the classical, weak so called secondorder arithmetic theory , a subsystem of the twosorted firstorder theory .
The collection of computable functions is classically 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[edit]
Historically, the subject of constructive set theory (often also "") begun with John Myhill's work on the theories also called and .^{[2]}^{[3]} 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 ,^{[4]} 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.^{[5]} 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[edit]
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,^{[6]} 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.^{[7]}^{[8]} Realizability models of within the effective topos have been identified, which, say, at once validate full Separation, relativized dependent choice , independence of premise for sets, but also the subcountability of all sets, Markov's principle and Church's thesis in the formulation for all predicates.^{[9]}
Subtheories of ZF[edit]
Notation[edit]
Language[edit]
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[edit]
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[edit]
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. Axioms of the form postulate that the class of all sets for which holds actually forms a set, and this is sometimes less formally expressed as .
Equality[edit]
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[edit]
Define class notation for the pairing of a few given elements via disjunctions. E.g. is the quantifierfree statement , and likewise says , and so on.
Two other basic existence postulates given some other sets are as follows. Firstly,

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

saying that for any set , there is at least one set , which holds all the members , of 's members . The minimal such set is the union.
The two axioms are commonly formulated stronger, in terms of "" instead of just "", although this is technically redundant in the context of : As the Separation axiom below is formulated with "", for statements the equivalence can be derived, given the theory allows for separation using . In cases where is an existential statement, like here in the union axiom, there is also another formulation using a universal quantifier.
Also using bounded Separation, the two axioms just stated together imply the existence of a binary union of two classes and , when they have been established to be sets, denoted by or . For a fixed set , to validate membership in the union of two given sets and , one needs to validate the part of the axiom, which can be done by validating the disjunction of the predicates defining the sets and , for . In terms of the associated sets, it is done by validating the disjunction .
The union and other set forming notations are also used for classes. For instance, the proposition is written . Let now . Given , the decidability of membership in , i.e. the potentially independent statement , can also be expressed as . But, as for any excluded middle statement, the doublenegation of the latter holds: That union isn't not inhabited by . This goes to show that partitioning is also a more involved notion, constructively.
Set existence[edit]
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. As is false for any , the axiom then reads .
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.^{[10]}^{[11]} 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[edit]
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[edit]
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 postulates Predicative Separation as well as the Replacement schema.
Axiom schema of predicative separation: For any bounded predicate , with parameters and with set variable not free in it, 
This axiom amounts to postulating the existence of a set obtained by the intersection of any set and any predicatively described class . For any proven to be a set, when the predicate is taken as , one obtains the binary intersection of sets and writes . Intersection corresponds to conjunction in an analog way to how union corresponds to disjunction.
When the predicate is taken as the negation , one obtains the difference principle, granting existence of any set . Note that sets like or are always empty. So, as noted, from Separation and the existence of at least one set (e.g. Infinity below) will follow the existence of the empty set (also denoted ). Within this conservative context of , the 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 be 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[edit]
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 like Intuitionistic New Foundations, a universal set may exist because use of the syntactic expression may be disallowed in proofs of existence by, essentially, separation.
Already the special case implies that the subclass of the universal class is proper as well.
Predicativity[edit]
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[edit]
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. In turn, for any fixed number, the corresponding product expression, say , can be constructed as a set. The axiomatic requirements for sets recursively defined in the language are discussed further below. Equality of elements inside a set is decidable if the corresponding relation as a subset of is decidable, in which case is sometimes called discrete.
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[edit]
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.
For some predicate of sets , the statement claims it for all subsets of the set of naturals, and the axiom now proves such sets do exist. Such quantification is also possible in secondorder arithmetic.
The pairwise order "" on the naturals is captured by their membership relation "". It is important to note that the theory proves the order as well as the equality relation on this set to be decidable. Not only is no number smaller than , but induction implies that among subsets of , it is exactly the empty set which has no least member. The contrapositive of this proves the doublenegated least number existence for all nonempty subsets of . Another valid principle also classically equivalent to it is least number existence for all inhabited decidable subsets. That said, the bare existence claim for the inhabited subset of is equivalent to excluded middle for , and a constructive theory will therefore not prove to be wellordered.
Weaker formulations of infinity[edit]
Should it need motivation, the handiness of postulating an unbounded set of numbers in relation to other inductive properties becomes clear in the discussion of arithmetic in set theory further below. But as is familiar from classical set theory, also weak forms of Infinity can be formulated. For example, one may just postulate the existence of some inductive set,  such an existence postulate suffices when full Separation may then be used to carve out the inductive subset of natural numbers, the shared subset of all inductive classes. Alternatively, more specific mere existence postulates may be adopted. Either which way, the inductive set then fulfills the following predecessor existence property in the sense of the von Neumann model:
Without making use of the notation for the previously defined successor notation, the extensional equality to a successor is captured by . This expresses that all elements are either equal to or themselves hold a predecessor set which shares all other members with .
Observe that through the expression "" on the right hand side, the property characterizing by its members here syntactically again contains the symbol itself. Due to the bottomup nature of the natural numbers, this is tame here. Assuming set induction, no two sets have this property. Also note that there are also longer formulations of this property, avoiding "" in favor unbounded quantifiers.
Number bounds[edit]
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 logically positive unboundedness statement
is now also one of infinitude. It is in the decidable arithmetic case. To validate infinitude of a set, this property even works if the set holds other elements besides infinitely many of members of .
Moderate induction in ECST[edit]
A set can be read as corresponding to predicates on sets. For example, an integer is even if it is a member of the set of even integers, or a natural number has a successor if it is a member of the set of natural numbers that have a successor.
The second universally quantified conjunct in the strong axiom of Infinity expresses mathematical induction for all in the universe of discourse, i.e. for sets. This is because the consequent of this clause, , states that all fulfill the associated predicate. Being able to use predicative separation to define subsets of , the theory proves induction for all predicates involving only setbounded quantifiers. It also means that more set existence axioms impact the strength of this induction principle, further motivating the function space and collection axioms that will be a focus of the rest of the article. Notably, already validates induction with quantifiers over the naturals, and hence induction as in the firstorder arithmetic theory .
It is instructive to analyze the way in which a theory with set comprehension ends up encoding predicate logic with an example. Consider a set , let denote the existential statement that the function space on the finite ordinal exist (which below will be denoted ). Here the existential quantifier is not merely one over natural numbers, nor is it bounded by any other set. A proposition like this finite exponentiation principle and the subclass claim are just two ways of formulating the same desired statement, namely an indexed conjunction of existential propositions where spans over the set of all naturals. The second form is expressed using notation for subclass comprehension and the right hand side may not constitute a set. If it is not already a set, many set axioms may not be used and establishing the universal closure as a theorem may not be possible. The predicative set theory with just bounded Separation can thus be strengthened not only by set existence axioms. The so called axiom of full mathematical induction for any predicate (i.e. class) expressed through set theory language is far stronger than the bounded induction principle valid in . The former principle could be directly adopted, closer mirroring secondorder arithmetic, but in set theory it also 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 the twosorted, first order theory of secondorder arithmetic in a form explicitly expressed for subsets of the naturals. That class of subsets can be taken to correspond to a richer collection of formulas than the firstorder arithmetic definable ones. In the program of reverse mathematics, all mathematical objects discussed are encoded as naturals or subsets of naturals. Subsystems of with very low complexity comprehension studied in that framework 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.^{[12]} shall moreover not be confused with the secondorder formulation of Peano arithmetic . 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.
Functions[edit]
General note on programs and functions[edit]
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, and not just "total 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, partial function programs 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 partial function program 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.^{[13]} As a predicate in , this totality constitutes an undecidable subset of indices, highlighting 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. Now 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 (i.e. with a ) prove the graph to be total functional.^{[14]}
Which predicates are provably functional for various inputs, or even total functional on their domain, generally depends on the adopted axioms of a theory and proof calculus. For example, for the diagonal halting problem, which cannot have a total index, it is independent whether the corresponding graph predicate on (a decision problem) is total functional, but implies that it is. Proof theoretical function hierarchies provide examples of predicates proven total functional in systems going beyond . Which sets proven to exist do constitute a total function, in the sense introduced next, also always depends on the axioms and the proof calculus. Finally, note that the soundness of halting claims is a metalogical property beyond consistency, i.e. a theory may be consistent and from it one may prove that some program will eventually halt, despite this never actually occurring when said program is ran. More formally, assuming consistency of a theory does not imply it is also arithmetically sound.
Total functional relations[edit]
In set theory language here, speak of a function class when and provenly
 .
Notably, this definition involves quantifier explicitly asking for existence  an aspect which is particularly important in the constructive context. In words: For every , it demands the unique existence of a so that . In the case that this holds one may use function application bracket notation and write . The above property may then be stated as . This notation may be extended to equality of function values. Some notational conveniences involving function application will only work when a set has indeed been established to be a function. Let (also written ) denote the class of sets that fulfill the function property. This is the class of functions from to in a pure set theory. Below the notation is also used for , for the sake of distinguishing it from ordinal exponentiation. When functions are understood as just function graphs as here, the membership proposition is also written . The booleanvalued are among the classes discussed in the next section.
By construction, any such function respects equality in the sense that , for any inputs from . This is worth mentioning since also more broader concepts of "operations" exist in the literature, which may not respect this. Variants of the functional predicate definition using apartness relations on setoids have been defined as well. A subset of a function is still a function and the function predicate may also be proven for enlarged chosen codomain sets. As noted, care must be taken with nomenclature "function", a word which sees use in most mathematical frameworks. When a function set itself is not tied to a particular codomain, then this set of pairs is also member of a function space with larger codomain. This do not happen when by the word one denotes the subset of pairs paired with a codomain set, i.e. a formalization in terms of . This is mostly a matter of bookkeeping, but affects how other predicates are defined, question of size. This choice is also just enforced by some mathematical frameworks.
If both the domain and considered 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.
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, one may always associate unique element of the singleton , which shows that merely a chosen range being a set does not suffice to be granted a function set. It is a metatheorem for theories containing that adding a function symbol for a provenly total class function is a conservative extension, despite this formally changing the scope of bounded Separation. 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.
Finitude[edit]
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 for a set can be defined, e.g. expressing the existence of some large enough natural such that a certain class of functions on the naturals always fail to map to distinct elements in . One definition considers some notion of noninjectivity into . Other definitions consider functions to a fixed superset of with more elements.
Terminology for conditions of finiteness and infinitude may vary. Notably, subfinitely indexed sets (a notion necessarily involving surjections) are sometimes called subfinite (which can be defined without functions). The property of being finitely indexed could also be denoted "finitely countable", to fit the naming logic, but is by some authors also called finitely enumerable (which might be confusing as this suggest an injection in the other direction). Relatedly, the existence of a bijection with a finite set has not established, one may say a set is not finite, but this use of language is then weaker than to claim the set to be nonfinite. The same issue applies to countable sets (not proven countable vs. proven noncountable), et cetera. A surjective map may also be called an enumeration.
Infinitude[edit]
The set itself is clearly unbounded. In fact, for any surjection from a finite range onto , one may construct an element that is different from any element in the functions range. Where needed, this notion of infinitude can also be expressed in terms of an apartness relation on the set in question. Being not Kuratowskifinite implies being nonfinite and indeed the naturals shall not be finite in any sense. Commonly, the word infinite is used for the negative notion of being nonfinite. Further, observe that , unlike any of its members, can be put in bijection with some of its proper unbounded subsets, e.g. those of the form for any . This validates the formulations of Dedekindinfinite. So more generally than the property of infinitude in the previous section on number bounds, one may call a set infinite in the logically positive sense if one can inject into it. A set that is even in bijection with may be called countably infinite. A set is Tarskiinfinite if there is some chain of subsets such that each has some new elements compared to its predecessor. There are indeed plenty of properties characterizing infinitude even in classical and that theory does not prove all nonfinite sets to be infinite in the injection existence sense, albeit it there holds when further assuming countable choice. without any choice even permits cardinals aside the aleph numbers, and there can then be sets that negate both of the above properties, i.e. they are both nonDedekindinfinite and nonfinite (also called Dedekindfinite infinite sets).
Call an inhabited set countable if there exists a surjection from onto it and subcountable if this can be done from some subset 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 is trivially infinite, countable and enumerable, as witnessed by the identity function. Also here, in strong classical theories many of these notions coincide in general and, as a result, the naming conventions in the literature are inconsistent. An infinite, countable set is equinumeros to .
There are also various ways to characterize logically negative notion. The notion of uncountability, in the sense of being not countable, is also discussed in conjunction with the exponentiation axiom further below. Another notion of uncountability of is given when one can produce a member in the compliment of any of 's countable subsets. More properties of finiteness may be defined as negations of such properties, et cetera.
Characteristic functions[edit]
Separation lets us cut out subsets of products , at least when they are described in a bounded fashion. Given any , one is now led to reason about classes such as
Since , one has
and so
 .
But be aware that in absence of any nonconstructive axioms may in generally not be decidable, since one requires an explicit proof of either disjunct. Constructively, when cannot be witnessed for all the , or uniqueness of the terms associated with each cannot be proven, then one cannot judge the comprehended collection to be total functional. Case in point: The classical derivation of Schröder–Bernstein relies on case analysis  but to constitute a function, particular cases shall actually be specifiable, given any input from the domain. It has been established that Schröder–Bernstein cannot have a proof on the base of plus constructive principles.^{[15]} 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[edit]
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 .
There is a large corpus of computability theory notions regarding how general subsets of naturals relate to one another. For example, one way to establish a bijection of two such sets is by relating them through a computable isomorphism, which is a computable permutation of all the naturals. The latter may in turn be established by a pair of particular injections in opposing directions.
Boundedness criteria[edit]
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, validity of pseudoboundedness, together with the counting sequence defined above, grants a bound for all the elements of .
The principle that any inhabited, pseudobounded subset of that is just countable (but not necessarily decidable) is always also bounded is called . The principle also holds generally in many constructive frameworks, such as the Markovian base theory , which is a theory postulating exclusively lawlike sequences with nice number search termination properties. However,  is independent of .
Choice functions[edit]
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. As with any independent axiom, this raises the proving capabilities while restricting the scope of possible (modeltheoretic) interpretations of the (syntactic) theory. A function existence claim can often be translated to the existence of inverses, orderings, and so on. Choice moreover implies statements about cardinalities of different sets, e.g. they imply or rule out countability of sets. Adding full choice to does not prove any new theorems, but it is strictly nonconstructive, as shown below. The development here proceeds in a fashion agnostic to any of the variants described next.^{[16]}
 Axiom of countable choice (or ): If , one can form the onetomany relationset . The axiom of countable choice would grant that whenever , one can form a function mapping each number to a unique value. The existence of such sequences is not generally provable on the base of and countable choice is not conservative over that theory. Countable choice into general sets can also be weakened further. One common consideration is to restrict the possible cardinalities of the range of , giving the weak countable choice into countable, finite or even just binary sets (). One may consider the version of countable choice for functions into (called or ), as is implied by the constructive Church's thesis principle, i.e. by postulating that all total arithmetical relations are recursive. in arithmetic may be understood as a form of choice axiom. Another means of weakening countable choice is by restricting the involved definitions w.r.t. their place in the syntactic hierarchies (say ). The weak Kőnig's lemma , which breaks strictly recursive mathematics as further discussed below, is stronger than  and is itself sometimes viewed as capturing a form of countable choice. In the presence of a weak form of countable choice, the lemma becomes equivalent to the nonconstructive principle of more logical flavor, . Constructively, weak form of choice is required for wellbehaved Cauchy reals. Countable choice is not valid in the internal logic of a general topos, which can be seen as models of constructive set theories.
 Axiom of dependent choice : Countable choice is implied by the more general axiom of dependent choice, extracting a sequence in an inhabited , given any entire relation . In set theory this is again an infinite set of pairs, a subset of and one is granted to pass from several existence statements to a unique existence statement for every natural. An appropriate formulation of dependent choice is adopted in several constructive frameworks, e.g., by some schools that understand unending sequences as ongoing constructions instead of completed objects. At least those cases seem benign where, for any , next value existence can be validated in a computable fashion. The corresponding recursive function , if it exists, is then conceptualized as being able to return a value at infinitely many potential inputs , but these do not have to be evaluated all together at once. It also holds in many realizability models. In the condition of the formally similar recursion theorem, one is already given a unique choice at each step, and that theorem lets one combine them to a function on . So also with one may consider forms of the axiom with restrictions on . Via the bounded separation axiom in , the principle also is equivalent to a schema in two bounded predicate variables: Keeping all quantifiers ranging over , one may further narrow this set domain using a unary predicate variable, while also using any 2ary predicate instead of the relation set .
 Relativized dependent choice : This is the schema just using two general classes, instead of requiring and be sets. The domain of the choice function granted to exist is still just . Over , it implies full mathematical induction, which, in turn allows for function definition on through the recursion schema. When is restricted to definitions, it still implies mathematical induction for predicates (with an existential quantifier over sets) as well as . In , the schema is equivalent to .
 : A family of sets is better controllable if it comes indexed by a function. A set is a base if all indexed families of sets over it, have a choice function , i.e. . A collection of sets holding and its elements and which is closed by taking indexed sums and products (see dependent type) is called closed. While the axiom that all sets in the smallest closed class are a base does need some work to formulate, it is the strongest choice principle over that holds in the type theoretical interpretation .
 Axiom of choice : This is the "full" choice function postulate concerning domains that are general sets containing inhabited sets, with the codomain given as their general union. Given a collection of sets such that the logic allows to make a choice in each, the axiom grants that there exists a set function that jointly captures a choice in all. It is typically formulated for all sets but has also been studied in classical formulations for sets only up to any particular cardinality. A standard example is choice in all inhabited subsets of the reals, which classically equals the domain . For this collection there can be no uniform element selection prescription that provably consistutes a choice function on the base of . Also, when restricted to the Borel algebra of the reals, alone does not prove the existence of a function selecting a member from each nonempty such Lebesguemeasurable subset. (The set is the σalgebra generated by the finite intervals . It strictly includes those intervals, in the sense of , but in also only has the cardinality of the reals itself.) Striking existence claims implied by the axiom are abound. proves exists and then the axiom of choice also implies dependent choice. Critically in the present context, it moreover also implies instances of via Diaconescu's theorem. For or theories extending it, this means full choice at the very least proves for all formulas, a nonconstructive consequence not acceptable, for example, from a computability standpoint.
Diaconescu's theorem[edit]
To highlight the strength of full Choice and its relation to matters of intentionality, one should consider the classes
from the proof of Diaconescu's theorem. They are as contingent as the proposition involved in their definition and they are not proven finite. Nonetheless, the setup entails several consequences. Referring back to the introductory elaboration on the meaning of such convenient class notation, as well as to the principle of distributivity, . So unconditionally, as well as , and in particular they are inhabited. As in any model of Heyting arithmetic, using the disjunctive syllogism both and each imply . The two statements are indeed equivalent to the proposition, as clearly . The latter also says that validity of means and share all members, and there are two of these. As are are then sets, also by extensionality. Conversely, assuming they are equal means for any , validating all membership statements. So both the membership statements as well as the equalities are found to be equivalent to . Using the contrapositive results in the weaker equivalence of disjuncts . Of course, explicitly and so one actually finds in which way the sets can end up being different. As functions preserves equality by definition, indeed holds for any with domain .
In the following assume a context in which are indeed established to be sets, and thus subfinite sets. The general axiom of choice claims existence of a function with . It is important that the elements of the function's domain are different than the natural numbers in the sense that a priori less is known about the former. When forming then union of the two classes, is a necessary but then also sufficient condition. Thus and one is dealing with functions into a set of two distinguishable values. With choice come the conjunction in the codomain of the function, but the possible function return values are known to be just or . Using the distributivity, there arises a list of conditions, another disjunction. Expanding what is then established, one finds that either both as well as the sets equality holds, or that the return values are different and can be rejected. The conclusion is that the choice postulate actually implies whenever a Separation axiom allows for set comprehension using undecidable proposition .
Analysis of Diaconescu's theorem[edit]
So full choice is nonconstructive in set theory as defined here. The issue is that when propositions are part of set comprehension (like when is used to separate, and thereby define, the classes and from ), the notion of their truth values are ramified into set terms of the theory. Equality defined by the set theoretical axiom of extensionality, which itself is not related to functions, in turn couples knowledge about the proposition to information about function values. To recapitulate the final step in terms function values: On the one hand, witnessing implies and and this conclusion independently also applies to witnessing . On the other hand, witnessing 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.
To better understand why one cannot expect to be granted a definitive (total) choice function with domain , consider naive function candidates. Firstly, an analysis of the domain is in order. The surjection witnesses that is finitely indexed. It was noted that its members are subfinite and also inhabited, since regardless of it is the case that and . So naively, this would seem to make a contender for a choice function. When can be rejected, then this is indeed 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 "truth value of " given as . 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, where functions as a (potentially undecidable) "ifclause". 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[edit]
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 . The proof in this paragraph also assumes Separation applies to and uses , for which by definition. It was already explained that and so one wants to prove excluded middle for the latter. 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[edit]
The four Peano axioms for and , characterizing as a model of the natural numbers in the constructive set theory , 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 is decidable. But the theory does actually not 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.
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. Far beyond just the equality predicate, the obtained model of arithmetic then validates
for any quantifierfree formula. Indeed, is conservative over and doublenegation elimination is possible for any Harrop formula.
Arithmetic functions from recursion[edit]
Going a step beyond , 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 iteration or recursion principle is akin to the transfinite recursion theorem, except it is restricted to set functions and finite ordinal arguments, 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.
Recursion from set theory axioms[edit]
Recall that is short for , where is short for the total function predicate, a proposition in terms of uses bounded quantifiers. If both sides are sets, then by extensionality this is also equivalent to . (Although by slight abuse of formal notation, as with the symbol "", the symbol "" is also commonly used with classes anyhow.)
A set theory with the model enabling recursion principle, spelled out above, will also prove that, for any naturals and , the function spaces