View source for Constructive set theory

{{Short description|Axiomatic set theories based on the principles of mathematical constructivism}}
Axiomatic '''constructive set theory''' is an approach to [[constructivism (mathematics)|mathematical constructivism]] following the program of [[axiomatic set theory]].
The same [[first-order logic|first-order]] language with "<math>=</math>" and "<math>\in</math>" of classical set theory is usually used, so this is not to be confused with a [[constructive type theory|constructive types]] approach.
On the other hand, some constructive theories are indeed motivated by their interpretability in [[type theory|type theories]].

In addition to rejecting the [[principle of excluded middle]] (<math>{\mathrm {PEM}}</math>), constructive set theories often require some logical quantifiers in their axioms to be set [[Bounded quantifier#Bounded quantifiers in set theory|bounded]]. The latter is motivated by results tied to [[impredicativity]].

== Introduction ==
=== Constructive outlook ===
==== Preliminary on the use of intuitionistic logic ====
The logic of the set theories discussed here is [[constructive logic|constructive]] in that it rejects the principle of excluded middle <math>{\mathrm {PEM}}</math>, i.e. that the [[disjunction]] <math>\phi \lor \neg \phi</math> automatically holds for all propositions <math>\phi</math>. This is also often called the ''law'' of excluded middle (<math>{\mathrm {LEM}}</math>) in contexts where it is assumed. Constructively, as a rule, to prove the excluded middle for a proposition <math>P</math>, i.e. to prove the particular disjunction <math>P \lor \neg P</math>, either <math>P</math> or <math>\neg P</math> needs to be explicitly proven. When either such proof is established, one says the proposition is decidable, and this then logically implies the disjunction holds. Similarly and more commonly, a predicate <math>Q(x)</math> for <math>x</math> in a domain <math>X</math> is said to be decidable when the more intricate statement <math>\forall (x\in X). \big(Q(x) \lor \neg Q(x)\big)</math> is provable. Non-constructive axioms may enable proofs that formally claim decidability of such <math>P</math> (and/or <math>Q</math>) in the sense that they prove excluded middle for <math>P</math> (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 problem|undecidable]].

The [[law of noncontradiction]] is a special case of the propositional form of [[modus ponens]]. Using the former with any negated statement <math>\neg P</math>, one valid [[De Morgan's laws#In intuitionistic logic|De Morgan's law]] thus implies <math>\neg\neg(P \lor \neg P)</math> 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 double-negation captures that the disjunction statement now provenly can never be ruled out or rejected, even in cases where the disjunction may not be provable (for example, by demonstrating one of the disjuncts, thus deciding <math>P</math>) from the assumed axioms.

More generally, constructive mathematical theories tend to prove [[Double-negation translation|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 <math>P</math> 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 [[principle of explosion|explosion]], the disjunction <math>P\lor\exist(x\in X). \neg Q(x)</math> implies the existence claim <math>\exist(x\in X). (Q(x)\to P)</math>, which in turn implies <math>\big( \forall(x\in X). Q(x)\big)\to P</math>. 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 <math>P</math> is rejected, one deals with a counter-example existence claim <math>\exist(x\in X). \neg Q(x)</math>, which is generally constructively stronger than a rejection claim <math>\neg \forall(x\in X). Q(x)</math>: Exemplifying a <math>t</math> such that <math>Q(t)</math> is contradictory of course means it is not the case that <math>Q</math> holds for all possible <math>x</math>. But one may also demonstrate that <math>Q</math> holding for all <math>x</math> would logically lead to a contradiction without the aid of a specific counter-example, and even while not being able to construct one. In the latter case, constructively, here one does not stipulate an existence claim.

==== Imposed restrictions on a set theory ====
Compared to the classical counterpart, one is generally less likely to prove the existence of relations that cannot be realized. A restriction to the constructive reading of existence apriori leads to stricter requirements regarding which characterizations of a set <math>f\subset X\times Y</math> involving unbounded collections constitute a (mathematical, and so always meaning [[Partial function|total]]) function. This is often because the predicate in a case-wise would-be definition may not be decidable. Adopting the standard definition of set equality via extensionality, the full [[Axiom of Choice]] is such a non-constructive principle that implies <math>{\mathrm {PEM}}</math> 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 [[epsilon induction|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,<ref>{{citation|title=In the Light of Logic|last=Feferman|first=Solomon|publisher=Oxford University Press|year=1998|isbn=0-195-08030-0|location=New York|pages=280–283, 293–294|author-link=Solomon Feferman|url=https://books.google.com/books?id=1rjnCwAAQBAJ}}</ref> technical question regarding which non-logical 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 [[Axiom schema of predicative separation|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, <math>\top</math> or <math>\bot</math>. Also the real line may be taken to be [[Indecomposability (intuitionistic logic)|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 <math>(\alpha \in \beta) \lor (\alpha = \beta) \lor (\beta \in \alpha)</math>. This determines whether the relation is [[Law of trichotomy|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 [[Judgment (mathematical logic)|judgements]] of propositions provable in the theory. Particularly well-studied are those such features that can be expressed in [[Heyting arithmetic]], with quantifiers over numbers and which can often be [[Realizability|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 thesis (constructive mathematics)|Church's rule]], witnessing any given function to be [[computable function|computable]].<ref>Troelstra, A. S., van Dalen D., ''Constructivism in mathematics: an introduction 1''; Studies in Logic and the Foundations of Mathematics; Springer, 1988;</ref>

A set theory does not only express theorems about numbers, and so one may consider a more general so-called strong existence property that is harder to come by, as will be discussed. A theory has this property if the following can be established: For any property <math>\phi</math>, 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 <math>\psi</math> that [[Uniqueness quantification|uniquely]] describes such a set instance. More formally, for any predicate <math>\phi</math> there is a predicate <math>\psi</math> so that
:<math>{\mathsf T}\vdash\exists x.\phi(x)\implies{\mathsf T}\vdash\exists !x. \phi(x)\land\psi(x)</math>
The role analogous to that of realized numbers in arithmetic is played here by defined sets proven to exist by (or according to) the theory. Questions concerning the axiomatic set theory's strength and its relation to term construction are subtle. While many theories discussed tend have all the various numerical properties, the existence property can easily be spoiled, as will be discussed. Weaker forms of existence properties have been formulated.

Some theories with a classical reading of existence can in fact also be constrained so as to exhibit the strong existence property. In [[Zermelo–Fraenkel set theory]] with sets all taken to be [[Ordinal definable set|ordinal-definable]], a theory denoted <math>{\mathsf {ZF}}+({\mathrm {V}}={\mathrm {HOD}})</math>, no sets without such definability exist. The property is also enforced via the [[constructible universe]] postulate in <math>{\mathsf {ZF}}+({\mathrm {V}}={\mathrm {L}})</math>.
For contrast, consider the theory <math>{\mathsf {ZFC}}</math> given by <math>{\mathsf {ZF}}</math> plus the full [[axiom of choice]] ''existence postulate'': Recall that this collection of axioms proves the [[well-ordering theorem]], implying well-orderings exists for any set. In particular, this means that relations <math>W\subset{\mathbb R}\times{\mathbb R}</math> formally exist that establish the well-ordering of <math>{\mathbb R}</math> (i.e. the theory claims the existence of a least element for all subsets of <math>{\mathbb R}</math> with respect to those relations). This is despite the fact that definability of such an ordering is [[List of statements independent of ZFC|known]] to be [[Independence (mathematical logic)|independent]] of <math>{\mathsf {ZFC}}</math>. The latter implies that for no particular formula <math>\psi</math> in the language of the theory does the theory prove that the corresponding set is a well-ordering relation of the reals. So <math>{\mathsf {ZFC}}</math> formally ''proves the existence'' of a subset <math>W\subset{\mathbb R}\times{\mathbb R}</math> with the property of being a well-ordering relation, but at the same time no particular set <math>W</math> for which the property could be validated can possibly be defined.

==== Anti-classical principles ====
As mentioned above, a constructive theory <math> {\mathsf T} </math> may exhibit the numerical existence property, <math>{\mathsf T}\vdash \exists e.\psi(e)\implies{\mathsf T}\vdash \psi({\underline {\mathrm e}})</math>, for some number <math>{\mathrm e}</math> and where <math>{\underline {\mathrm e}}</math> denotes the corresponding numeral in the formal theory. Here one must carefully distinguish between provable implications between two propositions, <math>{\mathsf T}\vdash P\to Q</math>, and a theory's properties of the form <math>{\mathsf T}\vdash P\implies{\mathsf T}\vdash Q</math>. When adopting a metalogically established schema of the latter type as an inference rule of one's proof calculus and nothing new can be proven, one says the theory <math>{\mathsf T}</math> is closed under that rule.

One may instead consider adjoining the rule corresponding to the meta-theoretical property as an implication (in the sense of "<math>\to</math>") to <math>{\mathsf T}</math>, as an [[axiom schema]] or in quantified form. A situation commonly studied is that of a fixed <math>{\mathsf T}</math> exhibiting the meta-theoretical property of the following type: For an instance from some collection of formulas of a particular form, here captured via <math>\phi</math> and <math>\psi</math>, one established the existence of a number <math>{\mathrm e}</math> so that <math>{\mathsf T}\vdash \phi\implies{\mathsf T}\vdash \psi({\underline {\mathrm e}})</math>. Here one may then postulate <math> \phi \to \exists (e\in{\mathbb N}).\psi(e)</math>, where the bound <math>e</math> is a number variable in language of the theory. For example, Church's rule is an [[admissible rule]] in first-order Heyting arithmetic <math>{\mathsf {HA}}</math> and, furthermore, the [[Church's thesis (constructive mathematics)|corresponding Church's thesis principle]] <math>{\mathrm {CT}}_0</math> may consistently be adopted as an axiom. The new theory with the principle added is anti-classical, in that it may not be consistent anymore to also adopt <math>{\mathrm {PEM}}</math>. Similarly, adjoining the excluded middle principle <math>{\mathrm {PEM}}</math> to some theory <math>{\mathsf T}</math>, the theory thus obtained may prove new, strictly classical statements, and this may spoil some of the meta-theoretical properties that were previously established for <math>{\mathsf T}</math>. In such a fashion, <math>{\mathrm {CT}}_0</math> may not be adopted in <math>{\mathsf {HA}}+{\mathrm {PEM}}</math>, also known as [[Peano arithmetic]] <math>{\mathsf {PA}}</math>.

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
:<math>\forall (f\in{\mathbb N}^{\mathbb N}).\exists (e\in{\mathbb N}).\Big(\forall(n\in{\mathbb N}).\exists(w\in{\mathbb N}). T(e, n, w)\land U(w, f(n))\Big)</math>
[[Kleene's T predicate]] together with the result extraction expresses that any input number <math>n</math> being mapped to the number <math>f(n)</math> is, through <math>w</math>, witnessed to be a computable mapping. Here <math>{\mathbb N}</math> now denotes a set theory model of the standard natural numbers and <math>e</math> is an index with respect to a fixed program enumeration. Stronger variants have been used, which extend this principle to functions <math>f\in{\mathbb N}^X</math> defined on domains <math>X\subset{\mathbb N}</math> of low complexity. The principle rejects decidability for the predicate <math>Q(e)</math> defined as <math>\exists(w\in{\mathbb N}). T(e, e, w)</math>, expressing that <math>e</math> is the index of a computable function [[Halting problem|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 <math>f</math>, 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 [[Second-order arithmetic#Subsystems|second-order arithmetic]] theory <math>{\mathsf {RCA}}_0</math>, a subsystem of the [[Many-sorted logic|two-sorted]] first-order theory <math>{\mathsf {Z}}_2</math>.

The collection of computable functions is classically [[subcountable]], which classically is the same as being countable. But classical set theories will generally claim that <math>{\mathbb N}^{\mathbb N}</math> holds also other functions than the computable ones. For example there is a proof in <math>{\mathsf{ZF}}</math> 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 anti-classical conception related the Markovian school is the permitted subcountability of various uncountable collections. When adopting the subcountability of the collection of all unending sequences of natural numbers (<math>{\mathbb N}^{\mathbb N}</math>) as an axiom in a constructive theory, the "smallness" (in classical terms) of this collection, in some set theoretical realizations, is then already captured by the theory itself.
A constructive theory may also adopt neither classical nor anti-classical axioms and so stay agnostic towards either possibility.

Constructive principles already prove <math>\forall (x\in X).\neg\neg\big(Q(x) \lor \neg Q(x)\big)</math> for any <math>Q</math>. And so for any given element <math>x</math> of <math>X</math>, the corresponding excluded middle statement for the proposition cannot be negated. Indeed, for any given <math>x</math>, by noncontradiction it is impossible to rule out <math>Q(x)</math> 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 <math>\neg\forall (x\in X). \big(Q(x) \lor \neg Q(x)\big)</math>. Adopting this does not necessitate providing a particular <math>t\in X</math> witnessing the failure of excluded middle for the particular proposition <math>Q(t)</math>, i.e. witnessing the inconsistent <math>\neg\big(Q(t)\lor\neg Q(t)\big)</math>. Predicates <math>Q(x)</math> on an infinite domain <math>X</math> correspond to [[decision problems]]. Motivated by provenly [[List of undecidable problems|computably undecidable problems]], one may reject the possibility of decidability of a predicate without also making any existence claim in <math>X</math>.
As another example, such a situation is enforced in [[L. E. J. Brouwer|Brouwerian]] intuitionistic analysis, in a case where the quantifier ranges over infinitely many [[Choice sequence|unending binary sequences]] and <math>Q(x)</math> states that a sequence <math>x</math> is everywhere zero. Concerning this property, of being conclusively identified as the sequence which is forever constant, adopting Brouwer's continuity principle strictly rules out that this could be proven decidable for all the sequences.

So in a constructive context with a so-called [[non-classical logic]] as used here, one may consistently adopt axioms which are both in contradiction to quantified forms of excluded middle, but also non-constructive in the computable sense or as gauged by meta-logical existence properties discussed previously. In that way, a constructive set theory can also provide the framework to study non-classical theories, say rings modeling [[smooth infinitesimal analysis]].

=== History and overview ===
Historically, the subject of constructive set theory (often also "<math>{\mathsf {CST}}</math>") begun with [[John Myhill]]'s work on the theories also called <math>{\mathsf {IZF}}</math> and <math>{\mathsf {CST}}</math>.<ref>Bridges D., Ishihara H., Rathjen M., Schwichtenberg H. (Editors), ''Handbook of Constructive Mathematics''; Studies in Logic and the Foundations of Mathematics; (2023) pp. 20-56</ref><ref>{{cite book | chapter-url=https://link.springer.com/content/pdf/10.1007/BFb0066775.pdf | doi=10.1007/BFb0066775 | chapter=Some properties of intuitionistic zermelo-frankel set theory | title=Cambridge Summer School in Mathematical Logic | series=Lecture Notes in Mathematics | date=1973 | last1=Myhill | first1=John | volume=337 | pages=206–231 | isbn=978-3-540-05569-3 }}</ref><ref>Crosilla, Laura; [https://plato.stanford.edu/entries/set-theory-constructive ''Set Theory: Constructive and Intuitionistic ZF'']; Stanford Encyclopedia of Philosophy; 2009</ref>
In 1973, he had proposed the former as a first-order set theory based on intuitionistic logic, taking the most common foundation <math>{\mathsf {ZFC}}</math> 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 <math>{\mathsf {ZFC}}</math> axioms which are equivalent in the classical setting are inequivalent in the constructive setting, and some forms imply <math>{\mathrm {PEM}}</math>, as will be demonstrated. In those cases, the intuitionistically weaker formulations were consequently adopted. The far more conservative system <math>{\mathsf {CST}}</math> is also a first-order theory, but of several sorts and bounded quantification, aiming to provide a formal foundation for [[Errett Bishop]]'s program of constructive mathematics.

The main discussion presents a sequence of theories in the same language as <math>{\mathsf {ZF}}</math>, leading up to [[Peter Aczel]]'s well studied ''<math>{\mathsf {CZF}}</math>'',<ref>Peter Aczel and Michael Rathjen, [https://web.archive.org/web/20130619020751/https://www.mittag-leffler.se/preprints/files/IML-0001-40.pdf ''Notes on Constructive Set Theory''], Reports Institut Mittag-Leffler, Mathematical Logic - 2000/2001, No. 40</ref> and beyond. Many modern results trace back to Rathjen and his students.
<math>{\mathsf {CZF}}</math> is also characterized by the two features present also in Myhill's theory:
On the one hand, it is using the [[Axiom schema of predicative separation|Predicative Separation]] instead of the full, unbounded Separation schema. Boundedness can be handled as a syntactic property or, alternatively, the theories can be conservatively extended with a higher boundedness predicate and its axioms. Secondly, 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 <math>{\mathrm {PEM}}</math> to a theory even weaker than <math>{\mathsf {CZF}}</math> recovers <math>{\mathsf {ZF}}</math>, as detailed below.<ref>John L. Bell, [https://publish.uwo.ca/~jbell/INTBOOK(Repaired).pdf ''Intuitionistic Set Theorys''], 2018</ref>
The system, which has come to be known as Intuitionistic Zermelo–Fraenkel set theory (<math>{\mathsf {IZF}}</math>), is a strong set theory without <math>{\mathrm {PEM}}</math>. It is similar to <math>{\mathsf {CZF}}</math>, but less conservative or [[Impredicativity|predicative]].
The theory denoted <math>{\mathsf {IKP}}</math> is the constructive version of <math>{\mathsf {KP}}</math>, 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|Zermelo–Fraenkel set theory (<math>{\mathsf{ZF}}</math>)]] with respect to their axiom as well as their underlying logic. Such theories can then also be interpreted in any model of <math>{\mathsf{ZF}}</math>.

[[Peano arithmetic]] <math>{\mathsf{PA}}</math> is [[Interpretation (model theory)#Bi-interpretability|bi-interpretable]] with the theory given by <math>{\mathsf{ZF}}</math> minus Infinity and without infinite sets, plus the existence of all [[transitive closure]]s. (The latter is also implied after promoting [[Axiom of Foundation|Regularity]] to the [[Epsilon-induction|Set Induction schema]], which is discussed below.) Likewise, constructive arithmetic can also be taken as an apology for most axioms adopted in <math>{\mathsf{CZF}}</math>: [[Heyting arithmetic]] <math>{\mathsf{HA}}</math> is bi-interpretable with a weak constructive set theory,<ref>{{citation|first=Hanul|last=Jeon|arxiv=2010.04270|title=Constructive Ackermann's interpretation|journal=Annals of Pure and Applied Logic |year=2022|volume=173 |issue=5 |page=103086 |doi=10.1016/j.apal.2021.103086 |s2cid=222271938 }}</ref><ref>Shapiro, S., McCarty, C. & Rathjen, M., [https://link.springer.com/article/10.1007/s00153-024-00935-4 ''Intuitionistic sets and numbers: small set theory and Heyting arithmetic''], https://doi.org/10.1007/s00153-024-00935-4, Arch. Math. Logic (2024)</ref> as also described in the article on <math>{\mathsf{HA}}</math>. One may arithmetically characterize a membership relation "<math>\in</math>" and with it prove - instead of the existence of a set of natural numbers <math>\omega</math> - that all sets in its theory are in bijection with a (finite) [[Set-theoretic definition of natural numbers|von Neumann natural]], a principle denoted <math>{\mathrm{V}}={\mathrm{Fin}}</math>. 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 <math>{\mathsf{CZF}}</math> minus the existence of <math>\omega</math> but plus <math>{\mathrm{V}}={\mathrm{Fin}}</math> as axiom. All those axioms are discussed in detail below.
Relatedly, <math>{\mathsf{CZF}}</math> also proves that the [[hereditarily finite sets]] fulfill all the previous axioms. This is a result which persists when passing on to <math>{\mathsf{PA}}</math> and <math>{\mathsf{ZF}}</math> minus Infinity.

As far as constructive realizations go there is a relevant [[realizability]] theory. Relatedly, Aczel's theory constructive Zermelo-Fraenkel <math>{\mathsf {CZF}}</math> has been interpreted in a [[Intuitionistic type theory|Martin-Löf type theories]], as sketched in the section on <math>{\mathsf {CZF}}</math>. In this way, theorems provable in this and weaker set theories are candidates for a computer realization.

[[Presheaf (category theory)|Presheaf]] models for constructive set theories have also been introduced. These are analogous to presheaf models for intuitionistic set theory developed by [[Dana Scott]] in the 1980s.<ref>{{Cite book| last1 = Gambino | first1 = N. | chapter = Presheaf models for constructive set theories | doi = 10.1093/acprof:oso/9780198566519.003.0004 | title = From Sets and Types to Topology and Analysis | pages = 62–96 | year = 2005 | isbn = 9780198566519 | chapter-url = http://www.math.unipa.it/~ngambino/Research/Papers/presheaf.pdf| editor = Laura Crosilla and Peter Schuster | url = http://eprints.whiterose.ac.uk/113160/1/presheaf.pdf }}</ref><ref>Scott, D. S. (1985). Category-theoretic models for Intuitionistic Set Theory. Manuscript slides of a talk given at Carnegie-Mellon University</ref> Realizability models of <math>{\mathsf{CZF}}</math> within the [[effective topos]] have been identified, which, say, at once validate full Separation, relativized dependent choice <math>{\mathrm{RDC}}</math>, [[independence of premise]] <math>{\mathrm{IP}}</math> for sets, but also the subcountability of all sets, Markov's principle <math>{\mathrm{MP}}</math> and Church's thesis <math>{\mathrm{CT}_0}</math> in the formulation for all predicates.<ref>Benno van den Berg, [https://staff.fnwi.uva.nl/b.vandenberg3/thesis/mythesis.pdf ''Predicative topos theory and models for constructive set theory''], Netherlands University, PhD thesis, 2006</ref>

=== Notation ===
In an axiomatic [[List of first-order theories#Set theories|set theory]], sets are the entities exhibiting properties. But there is then a more intricate relation between the set concept and logic. For example, the ''property'' of being a natural number smaller than 100 may be reformulated as being a member of the ''set'' of numbers with that property. The set theory axioms govern set existence and thus govern which predicates can be materialized as entity in itself, in this sense. 
Specification is also directly governed by the axioms, as discussed below. For a practical consideration, consider for example the property of being a sequence of coin flip outcomes that overall show more heads than tails. This property may be used to separate out a corresponding subset of any set of finite sequences of coin flips. Relatedly, the [[measure theory|measure theoretic]] formalization of a [[Event (probability theory)|probabilistic event]] is explicitly based around sets and provides many more examples.

This section introduces the object language and auxiliary notions used to formalize this materialization.

==== Language ====
The [[Logical connective|propositional connective]] symbols used to form syntactic formulas are standard. The axioms of set theory give a means to prove [[logical equality|equality]] "<math>=</math>" of sets and that symbol may, by [[abuse of notation]], be used for classes. A set in which the equality predicate is decidable is also called ''discrete''. Negation "<math>\neg</math>" of equality is sometimes called the denial of equality, and is commonly written "<math>\neq</math>". However, in a context with [[apartness relations]], for example when dealing with sequences, the latter symbol is also sometimes used for something different.

The common treatment, as also adopted here, formally only extends the underlying logic by one primitive binary predicate of set theory, "<math>\in</math>". As with equality, negation of elementhood "<math>\in</math>" is often written "<math>\notin</math>".

==== Variables ====
Below the Greek <math>\phi</math> denotes a proposition or predicate variable in [[axiom schema]]s and <math>P</math> or <math>Q</math> is used for particular such predicates. The word "predicate" is sometimes used interchangeably with "formulas" as well, even in the [[arity|unary case]].

Quantifiers only ever range over sets and those are denoted by lower case letters.
As is common, one may use argument brackets to express predicates, for the sake of highlighting particular free variables in their syntactic expression, as in "<math>Q(z)</math>".
[[Uniqueness quantification|Unique existence]] <math>\exists!x. Q(x)</math> here means <math>\exists x. \forall y. \big(y=x \leftrightarrow Q(y)\big)</math>.

==== Classes ====
As is also common, one makes use set builder notation for [[Class (set theory)|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 "<math>A=\{z\mid Q(z)\}</math>", for the purpose of expressing any <math>Q(a)</math> as <math>a\in A</math>. Logically equivalent predicates can be used to introduce the same class.
One also writes <math>\{z\in B\mid Q(z)\}</math> as shorthand for <math>\{z\mid z\in B\land Q(z)\}</math>. For example, one may consider <math>\{z\in B\mid z\notin C\}</math> and this is also denoted <math>B\setminus C</math>.

One abbreviates <math>\forall z. \big(z\in A\to Q(z)\big)</math> by <math>\forall (z\in A). Q(z)</math> and <math>\exists z. \big(z\in A\land Q(z)\big)</math> by <math>\exists (z\in A). Q(z)</math>. The syntactic notion of bounded quantification in this sense can play a role in the formulation of axiom schemas, as seen in the discussion of axioms below. 
Express the '''subclass''' claim <math>\forall (z\in A). z\in B</math>, i.e. <math>\forall z. (z\in A\to z\in B)</math>, by <math>A\subset B</math>.
For a predicate <math>Q</math>, trivially <math>\forall z.\big((z\in B\land Q(z))\to z\in B\big)</math>. And so follows that <math>\{z\in B\mid Q(z)\}\subset B</math>.
The notion of subset-bounded quantifiers, as in <math>\forall (z\subset A). z\in B</math>, has been used in set theoretical investigation as well, but will not be further highlighted here.

If there provenly ''exists'' a set inside a class, meaning <math>\exists z. (z\in A)</math>, then one calls it ''[[Inhabited set|inhabited]]''. One may also use quantification in <math>A</math> to express this as <math>\exists(z\in A).(z = z)</math>. The class <math>A</math> is then provenly not the empty set, introduced below. While classically equivalent, constructively ''non-empty'' is a weaker notion with two negations and ought to be called ''not uninhabited''. Unfortunately, the word for the more useful notion of 'inhabited' is rarely used in classical mathematics.

Two ways to express that classes are ''[[Disjoint sets|disjoint]]'' does capture many of the intuitionistically valid negation rules: <math>\big(\forall(x\in A). x\notin B\big) \leftrightarrow \neg\exists(x\in A). x\in B</math>. Using the above notation, this is a purely logical equivalence and in this article the proposition will furthermore be expressible as <math>A\cap B=\{\}</math>.

A subclass <math>A\subset B</math> is called ''detachable'' from <math>B</math> if the relativized membership predicate is decidable, i.e. if <math>\forall(x\in B). x\in A \lor x\notin A</math> holds. It is also called decidable if the superclass is clear from the context - often this is the set of natural numbers.

==== Extensional equivalence ====
Denote by <math>A\simeq B</math> the statement expressing that two classes have exactly the same elements, i.e. <math>\forall z. (z\in A \leftrightarrow z\in B)</math>, or equivalently <math>(A\subset B)\land (B\subset A)</math>. This is not to be conflated with the concept of [[equinumerosity]] also used below.

With <math>A</math> standing for <math>\{z\mid Q(z)\}</math>, the convenient notational relation between <math>x \in A</math> and <math>Q(x)</math>, axioms of the form <math>\exists a. \forall z. \big(z\in a\leftrightarrow Q(z)\big)</math> postulate that the ''class'' of all sets for which <math>Q</math> holds actually forms a ''set''. Less formally, this may be expressed as <math>\exists a. a\simeq A</math>. Likewise, the proposition <math>\forall a.(a\simeq A)\to P(a)</math> conveys "<math>P(A)</math> when <math>A</math> is among the theory's sets." For the case where <math>P</math> is the trivially false predicate, the proposition is equivalent to the negation of the former existence claim, expressing the non-existence of <math>A</math> as a set.

Further extensions of class comprehension notation as above are in common used in set theory, giving meaning to statements such as "<math>\{f(z)\mid Q(z)\}\simeq\{\langle x, y, z \rangle\mid T(x, y, z) \}</math>", and so on.

Syntactically more general, a set <math>w</math> may also be characterized using another 2-ary predicate <math>R</math> trough <math>\forall x. x \in w \leftrightarrow R(x, w)</math>, where the right hand side may depend on the actual variable <math>w</math>, and possibly even on membership in <math>w</math> itself.

== Subtheories of ZF ==
Here a series of familiar axioms is presented, or the relevant slight reformulations thereof. It is emphasized how the absence of <math>{\mathrm{PEM}}</math> in the logic affects what is provable and it is highlighted which non-classical axioms are, in turn, consistent.

===Equality===
Using the notation introduced above, the following axiom gives a means to prove equality "<math>=</math>" of two ''sets'', so that through substitution, any predicate about <math>x</math> translates to one of <math>y</math>.
By the logical properties of equality, the converse direction of the postulated implication holds automatically.
{| border=1 style="border:0px"
| style="border:1px solid #000000; padding:1.0em; background-color:#F8F9FA" |
[[Axiom of Extensionality|Extensionality]]
; <math>\forall x. \forall y.\ \ x\simeq y \to x = y</math>
|}
In a constructive interpretation, the elements of a subclass <math>A=\{z\in B\mid Q(z)\lor\neg Q(z)\}</math> of <math> B</math> may come equipped with more information than those of <math>B</math>, in the sense that being able to judge <math>b\in A</math> is being able to judge <math>Q(b)\lor\neg Q(b)</math>. And (unless the whole disjunction follows from axioms) in the [[Brouwer–Heyting–Kolmogorov interpretation]], this means to have proven <math>Q(b)</math> or having rejected it.
As <math>\{z\in B\mid Q(z)\}</math> may not be detachable from <math>B</math>, i.e. as <math>Q</math> [[Undecidable problem|may be not decidable]] for all elements in <math>B</math>, the two classes <math>A</math> and <math>B</math> must a priori be distinguished.

Consider a predicate <math>Q</math> that provenly holds for all elements of a set <math>y</math>, so that <math>y\simeq \{z\in y\mid Q(z)\}</math>, and assume that the class on the right hand side is established to be a set. Note that, even if this set on the right informally also ties to proof-relevant information about the validity of <math>Q</math> for all the elements, the Extensionality axiom postulates that, in our set theory, the set on the right hand side is judged equal to the one on the left hand side.
This above analysis also shows that a statement of the form <math>\forall(x\in w). Q(x)</math>, which in informal class notation may be expressed as <math>w\subset \{x\mid Q(x)\}</math>, is then equivalently expressed as <math>\{x\in w\mid Q(x)\} = w</math>. This means that establishing such <math>\forall</math>-theorems (e.g. the ones provable from full mathematical induction) enables substituting the subclass of <math>w</math> on the left hand side of the equality for just <math>w</math>, in any formula.

Note that adopting "<math>=</math>" as a symbol in a predicate logic theory makes equality of two terms a quantifier-free expression.

====Alternative approaches====
While often adopted, this axiom has been criticized in constructive thought, as it effectively collapses differently defined properties, or at least the sets viewed as the extension of these properties, a [[Gottlob Frege#Work as a logician|Fregian]] notion.

Modern type theories may instead aim at defining the demanded equivalence "<math>\simeq</math>" in terms of functions, see e.g. [[Homotopy type theory#Type equivalence|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 relation|apartness]] come for the elements <math>z\in x</math> of each and every set <math>x</math> discussed. But also in an approach to sets emphasizing apartness may the above definition in terms of subsets be used to characterize a notion of equality "<math>\simeq</math>" of those subsets.
Relatedly, a loose notion of complementation of two [[subsets]] <math>u\subset x</math> and <math>v\subset x</math> is given when any two members <math>s\in u</math> and <math>t\in v</math> are provably apart from each other. The collection of complementing pairs <math>\langle u,v\rangle</math> is [[algebra of sets|algebraically]] well behaved.

===Merging sets===
Define class notation for the pairing of a few given elements via disjunctions. E.g. <math>z\in\{a,b\}</math> is the quantifier-free statement <math>(z=a)\lor(z=b)</math>, and likewise <math>z\in\{a,b,c\}</math> says <math>(z=a)\lor(z=b)\lor(z=c)</math>, and so on.

Two other basic existence postulates given some other sets are as follows. Firstly,
{| border=1 style="border:0px"
| style="border:1px solid #000000; padding:1.0em; background-color:#F8F9FA" |
[[Axiom of pairing|Pairing]]
; <math>\forall x. \forall y.\ \ \exists p. \{x,y\}\subset p </math>
|}
Given the definitions above, <math>\{x,y\}\subset p </math> expands to <math>\forall z. (z=x\lor z=y) \to z\in p</math>, so this is making use of equality and a disjunction. The axiom says that for any two sets <math>x</math> and <math>y</math>, there is at least one set <math>p</math>, which hold at least those two sets.

With bounded Separation below, also the class <math>\{x,y\}</math> exists as a set. Denote by <math>\langle x, y\rangle</math> the standard [[ordered pair]] model <math>\{\{x\},\{x,y\}\}</math>, so that e.g. <math>q=\langle x, y\rangle</math> [[Kripke–Platek set theory#Cartesian products exist|denotes another bounded formula]] in the formal language of the theory.

And then, using existential quantification and a conjunction,
{| border=1 style="border:0px"
| style="border:1px solid #000000; padding:1.0em; background-color:#F8F9FA" |
[[Axiom of union|Union]]
; <math>\forall x.\ \ \exists u. \forall z. \Big(\big(\exists (y\in x). z\in y\big)\to z\in u\Big)</math>
|}
saying that for any set <math>x</math>, there is at least one set <math>u</math>, which holds all the members <math>z</math>, of <math>x</math>'s members <math>y</math>.
The minimal such set is the '''union'''.

The two axioms are commonly formulated stronger, in terms of "<math>\leftrightarrow</math>" instead of just "<math>\to</math>", although this is technically redundant in the context of <math>{\mathsf {BCST}}</math>: As the Separation axiom below is formulated with "<math>\leftrightarrow</math>", for statements <math>\exists t.\forall z.\phi(z)\to z\in t</math> the equivalence can be derived, given the theory allows for separation using <math>\phi</math>. In cases where <math>\phi</math> is an existential statement, like here in the union axiom, there is also [[Axiom of union#Relation to Separation|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 <math>a</math> and <math>b</math>, when they have been established to be sets, denoted by <math>\bigcup\{a,b\}</math> or <math>a\cup b</math>. For a fixed set <math>z</math>, to validate membership <math>z\in a\cup b</math> in the union of two given sets <math>y=a</math> and <math>y=b</math>, one needs to validate the <math>z\in y</math> part of the axiom, which can be done by validating the disjunction of the predicates defining the sets <math>a</math> and <math>b</math>, for <math>z</math>. In terms of the associated sets, it is done by validating the disjunction <math>z\in a \lor z\in b</math>.

The union and other set forming notations are also used for classes. For instance, the proposition <math>z\in A\land z\notin C</math> is written <math>z\in A\setminus C</math>. Let now <math>B\subset A</math>. Given <math>z\in A</math>, the decidability of membership in <math>B</math>, i.e. the potentially independent statement <math>z\in B \lor z\notin B</math>, can also be expressed as <math>z\in B\cup(A\setminus B)</math>. But, as for any excluded middle statement, the double-negation of the latter holds: That union isn't not inhabited by <math>z</math>. This goes to show that partitioning is also a more involved notion, constructively.

===Set existence===
The property that is false for any set corresponds to the '''empty''' class, which is denoted by <math>\{\}</math> or zero, <math>0</math>. That the empty class is a set readily follows from other existence axioms, such as the Axiom of Infinity below. But if, e.g., one is explicitly interested in excluding infinite sets in one's study, one may at this point adopt the
{| border=1 style="border:0px"
| style="border:1px solid #000000; padding:1.0em; background-color:#F8F9FA" |
[[Axiom of empty set]]:
; <math>\exists x. \forall y.\, \neg(y \in x)</math>
|}
Introduction of the symbol <math>\{\}</math> (as abbreviating notation for expressions in involving characterizing properties) is justified as uniqueness for this set can be proven. As <math>y\in\{\}</math> is false for any <math>y</math>, the axiom then reads <math>\exists x. x\simeq\{\}</math>.

Write <math>1</math> for <math>S0</math>, which equals <math>\{\{\}\}</math>, i.e. <math>\{0\}</math>. Likewise, write <math>2</math> for <math>S1</math>, which equals <math>\{\{\},\{\{\}\}\}</math>, i.e. <math>\{0,1\}</math>. A simple and provenly false proposition then is, for example, <math>\{\}\in\{\}</math>, corresponding to <math>0 < 0</math> in the standard arithmetic model.
Again, here symbols such as <math>\{\}</math> are treated as convenient notation and any proposition really translates to an expression using only "<math>\in</math>" and logical symbols, including quantifiers. Accompanied by a metamathematical analysis that the capabilities of the new theories are equivalent in an effective manner, [[Extension by definitions|formal extensions]] by symbols such as <math>0</math> may also be considered.

More generally, for a set <math>x</math>, define the '''[[Successor function|successor set]]''' <math>Sx</math> as <math>x\cup\{x\}</math>. The interplay of the successor operation with the membership relation has a recursive clause, in the sense that <math>(y\in Sx)\leftrightarrow (y\in x\lor y=x)</math>. By reflexivity of equality, <math>x\in Sx</math>, and in particular <math>Sx</math> is always inhabited.

=== BCST ===
The following makes use of [[axiom schema]]s, 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 <math>v_0, v_1, \dots, v_n</math>). That is, instantiations of the schema are permitted in which the predicate (some particular <math>\phi</math>) 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 <math>\forall v_0. \forall v_1. \cdots \forall v_n.</math>).

==== Separation ====
Basic constructive set theory <math>{\mathsf{BCST}}</math> consists of several axioms also part of standard set theory, except the so called "full" [[Axiom schema of specification|Separation]] axiom is weakened.
Beyond the four axioms above, it postulates Predicative Separation as well as the Replacement schema.
{| border=1 style="border:0px"
| style="border:1px solid #000000; padding:1.0em; background-color:#F8F9FA" |
[[Axiom schema of predicative separation]]: For any [[Bounded quantifier#Bounded quantifiers in set theory|bounded]] predicate <math>\phi</math>, with parameters and with set variable <math>y</math> not free in it,
; <math>\forall y.\,\exists s.\forall x.\big(x\in s\,\leftrightarrow\,(x\in y \land\phi(x))\big)</math>
|}
This axiom amounts to postulating the existence of a set <math>s</math> obtained by the '''intersection''' of any set <math>y</math> and any predicatively described class <math>\{x\mid \phi(x)\}</math>.
For any <math>z</math> proven to be a set, when the predicate is taken as <math>\phi(x):=x\in z</math>, one obtains the binary intersection of sets and writes <math>s=y\cap z</math>. Intersection corresponds to conjunction in an analog way to how union corresponds to disjunction.

When the predicate is taken as the negation <math>\phi(x):=x\notin z</math>, one obtains the difference principle, granting existence of any set <math>y\setminus z</math>. Note that sets like <math>y\setminus y</math> or <math>\{x\in y\mid \neg(x=x)\}</math> 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 <math>\{\}</math> (also denoted <math>0</math>).
Within this conservative context of <math>{\mathsf {BCST}}</math>, the Predicative Separation schema is actually equivalent to Empty Set plus the existence of the binary intersection for any two sets. The latter variant of axiomatization does not make use of a formula schema.

Predicative Separation is a schema that takes into account syntactic aspects of set defining predicates, up to provable equivalence. The permitted formulas are denoted by <math>\Delta_0</math>, the lowest level in the set theoretical [[Lévy hierarchy]].<ref>{{citation | last1=Jech | first1=Thomas | author1-link=Thomas Jech | title=Set Theory | edition= Third Millennium | publisher=[[Springer-Verlag]] | location=Berlin, New York | series=Springer Monographs in Mathematics | isbn=978-3-540-44085-7 | year=2003 | zbl=1007.03002 | page=642 | url=https://books.google.com/books?id=CZb-CAAAQBAJ&pg=PA642 }}</ref>
General predicates in set theory are never syntactically restricted in such a way and so, in praxis, generic subclasses of sets are still part of the mathematical language. As the scope of subclasses that are provably sets is sensitive to what sets already exist, this scope is expanded when further set existence postulates are added.

A class with at most one element is called a subsingleton. For a proposition <math>P</math>, a recurring trope in the constructive analysis of set theory is to view the predicate <math>x=0 \land P</math> as the subsingleton <math>B:=\{x\in 1\mid P\}</math>, which is subclass of the second ordinal <math>1:=S0=\{0\}</math>. 
If it is provable that <math>P</math> holds, or <math>\neg P</math>, or <math>\neg \neg P</math>, then <math>B</math> is inhabited, or empty (uninhabited), or non-empty (not uninhabited), respectively.
Clearly, <math>P</math> is equivalent to both the proposition <math>0\in B</math>, and also <math>B = 1</math>. Likewise, <math>\neg P</math> is equivalent to <math>B = 0</math> and, equivalently, also <math>\neg(0\in B)</math>. So, here, <math>B</math> being detachable from <math>1</math> exactly means <math>P\lor\neg P</math>.
In the model of the naturals, if <math>B</math> is a number, <math>0\in B</math> also expresses that <math>0</math> is smaller than <math>B</math>. The union that is part of the successor operation definition above may be used to express the excluded middle statement as <math>0\in SB</math>. In words, <math>P</math> is decidable if and only if the successor of <math>B</math> is larger than the smallest ordinal <math>0</math>. The proposition  <math>P</math> is decided either way through establishing ''how''  <math>0</math> is smaller: By <math>0</math> already being smaller than <math>B</math>, or by <math>0</math> being <math>SB</math>'s direct predecessor. Yet another way to express excluded middle for <math>P</math> is as the existence of a least number member of the inhabited class <math>b:=B\cup\{1\}</math>.

If one's separation axiom allows for separation with <math>P</math>, then <math>B</math> is a sub''set'', which may be called the [[truth value]] associated with <math>P</math>. Two truth values can be proven equal, as sets, by proving an equivalence. In terms of this terminology, the collection of proof values can a priori be understood to be rich. Unsurprisingly, decidable propositions have one of a binary set of truth values. The excluded middle disjunction for that <math>P</math> is then also implied by the global statement <math>\forall b. (0\in b)\lor (0\notin b)</math>.

==== No universal set ====
When using the informal class terminology, any set is also considered a class. At the same time, there do arise so called ''proper'' classes that can have no extension as a set. When in a theory there is a proof of <math>\neg\exists x. A\subset x</math>, then <math>A</math> must be proper. (When taking up the perspective of <math>{\mathsf {ZF}}</math> on sets, a theory which has full Separation, proper classes are generally thought of as those that are "too big" to be a set. More technically, they are subclasses of the [[cumulative hierarchy]] that extend beyond any ordinal bound.)

By a remark in the section on merging sets, a set cannot consistently ruled out to be a member of a class of the form <math>A\cup \{x\mid x\notin A\}</math>. A constructive proof that it is in that class contains information. Now if <math>A</math> is a set, then the class <math>\{x \mid x\notin A\}</math> is provably proper. The following demonstrates this in the special case when <math>A</math> is empty, i.e. when the right side is the universal class. Being negative results, it reads as in the classical theory.

The following holds for any relation <math>E</math>. It gives a purely logical condition such that two terms <math>s</math> and <math>y</math> cannot be <math>E</math>-related to one another.
:<math>\big(\forall x. xEs\leftrightarrow(xEy \land \neg xEx)\big) \to \neg(yEs\lor sEs\lor sEy)</math>
Most important here is the rejection of the final disjunct, <math>\neg sEy</math>. The expression <math>\neg(x\in x)</math> does not involve unbounded quantification and is thus allowed in Separation. [[Russel's paradox|Russel's construction]] in turn shows that <math>\{x\in y\mid x\notin x\}\notin y</math>. So for any set <math>y</math>, Predicative Separation alone implies that there exists a set which is not a member of <math>y</math>. In particular, no [[universal set]] can exist in this theory.

In a theory further adopting the [[axiom of regularity]], like <math>{\mathsf {ZF}}</math>, provenly <math>x\in x</math> is false for any set <math>x</math>. There, this then means that the subset <math>\{x\in y\mid x\notin x\}</math> is equal to <math>y</math> itself, and that the class <math>\{x\mid x\in x\}</math> is the empty set.

For any <math>E</math> and <math>y</math>, the special case <math>s=y</math> in the formula above gives 
:<math>\neg\big(\forall x. xEy\leftrightarrow \neg xEx\big)</math>
This already implies that no set <math>y</math> equals the subclass <math>\{x\mid x\notin x\}</math> of the universal class, i.e. that subclass is a proper one as well. But even in <math>{\mathsf {ZF}}</math> without Regularity it is consistent for there to be a proper class of singletons which each contain exactly themselves.

As an aside, in a theory with [[Stratification (mathematics)#In a specific set theory|stratification]] like [[New Foundations|Intuitionistic New Foundations]], the syntactic expression <math>x\in x</math> may be disallowed in Separation. In turn, the above proof of negation of the existence of a universal set cannot be performed, in that theory.

==== Predicativity ====
The axiom schema of Predicative Separation is also called <math>\Delta_0</math>-Separation or Bounded Separation, as in Separation for set-[[Bounded quantifier#Bounded quantifiers in set theory|bounded quantifiers]] only. (Warning note: The Lévy hierarchy nomenclature is in analogy to <math>\Delta_0^0</math> in the [[arithmetical hierarchy]], albeit comparison can be subtle: The arithmetic classification is sometimes expressed not syntactically but in terms of subclasses of the naturals. Also, the bottom level of the arithmetical hierarchy has several common definitions, some not allowing the use of some total functions. A similar distinction is not relevant on the level <math>\Sigma_1^0</math> or higher. Finally note that a <math>\Delta_0</math> 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]] <math>{\mathsf {Z}}</math>, for mathematical foundations related to [[topos theory]]. It is also used in the study of [[Absoluteness (logic)|absoluteness]], and there part of the formulation of [[Kripke-Platek set theory]].

The restriction in the axiom is also gatekeeping [[Impredicativity|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 <math>R</math> denotes some 2-ary predicate, one should not generally expect a subclass <math>s</math> of <math>y</math> to be a set, in case that it is defined, for example, as in
:<math>\{x\in y\mid \forall t. \big((t\subset y) \to R(x, t)\big)\}</math>,
or via a similar definitions involving any quantification over the sets <math>t\subset y</math>. Note that if this subclass <math>s</math> of <math>y</math> is provenly a set, then this subset itself is also in the unbounded scope of set variable <math>t</math>. In other words, as the subclass property <math>s\subset y</math> is fulfilled, this exact set <math>s</math>, defined using the expression <math>R(x, s)</math>, would play a role in its own characterization.

While predicative Separation leads to fewer given class definitions being sets, it may be emphasized that many class definitions that are classically equivalent are not so when restricting oneself to the weaker logic. Due to the potential [[Undecidable problem|undecidability]] of general predicates, the notion of subset and subclass is automatically more elaborate in constructive set theories than in classical ones. So in this way one has obtained a broader theory. This remains true if full Separation is adopted, such as in the theory <math>{\mathsf{IZF}}</math>, which however spoils the [[existence property]] as well as the standard type theoretical interpretations, and in this way spoils a bottom-up 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
{| border=1 style="border:0px"
| style="border:1px solid #000000; padding:1.0em; background-color:#F8F9FA" |
[[Axiom schema of replacement|Axiom schema of Replacement]]: For any predicate <math>\phi</math> with set variable <math>r</math> not free in it,
; <math>\forall d.\ \ \forall (x\in d). \exists! y. \phi(x,y) \to \exists r. \forall y. \big(y\in r \leftrightarrow \exists (x\in d). \phi(x,y)\big)</math>
|}
It is granting existence, as sets, of the range of function-like predicates, obtained via their domains. In the above formulation, the predicate is not restricted akin to the Separation schema, but this axiom already involves an existential quantifier in the antecedent. Of course, weaker schemas could be considered as well.

Via Replacement, the existence of any pair <math>\{x,y\}</math> also follows from that of any other particular pair, such as <math>\{0,1\}=2=SS0</math>. But as the binary union used in <math>S</math> already made use of the Pairing axiom, this approach then necessitates postulating the existence of <math>2</math> over that of <math>0</math>. In a theory with the impredicative Powerset axiom, the existence of <math>2\subset{\mathcal P}{\mathcal P}0</math> can also be demonstrated using Separation.

With the Replacement schema, the theory outlined thus far proves that the [[equivalence classes]] or [[Dependent type#Σ type|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 (in the metatheory), the corresponding product expression, say <math>x\times x\times x\times x</math>, can be constructed as a set. The axiomatic requirements for sets recursively defined in the language are discussed further below. A set <math>x</math> is discrete, i.e. equality of elements inside a set <math>x</math> is decidable, if the corresponding relation as a subset of <math>x\times x</math> is decidable.

Replacement is relevant for [[Axiom of non-choice|function comprehension]] and can be seen as a form of comprehension more generally. [[Axiom schema of replacement#Separation|Only when]] assuming <math>{\mathrm {PEM}}</math> does Replacement already imply full Separation. In <math>{\mathsf {ZF}}</math>, Replacement is mostly important to prove the existence of sets of high [[Von Neumann universe|rank]], namely via instances of the axiom schema where <math>\phi(x,y)</math> relates relatively small set <math>x</math> to bigger ones, <math>y</math>.

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 <math>{\mathsf {ZF}}</math>, but instead merely to gain back some provability strength. Such stronger axioms exist that do not spoil the strong [[existence property|existence properties]] of a theory, as discussed further below.

If <math>i_X</math> is provenly a function on <math>X</math> and it is equipped with a codomain <math>Y</math> (all discussed in detail below), then the [[Image (mathematics)#Image of a function|image]] of <math>i_X</math> is a subset of <math>Y</math>. In other approaches to the set concept, the notion of subsets is defined in terms of "operations", in this fashion.

==== Hereditarily finite sets ====
Pendants of the elements of the class of [[hereditarily finite sets]] <math>H_{\aleph_0}</math> can be implemented in any common programming language. The axioms discussed above abstract from common operations on the [[Set (abstract data type)|set data type]]: Pairing and Union are related to nesting and [[List (abstract data type)#The list monad|flattening]], or taken together concatenation. Replacement is related to [[List comprehension|comprehension]] and Separation is then related to the often simpler [[Filter (higher-order function)|filtering]]. Replacement together with [[Epsilon-induction|Set Induction]] (introduced below) suffices to axiomize <math>H_{\aleph_0}</math> constructively and that theory is also studied without Infinity.

A sort of blend between pairing and union, an axiom more readily related to the successor is the [[Axiom of adjunction]].<ref>Gert Smolka, [https://www.ps.uni-saarland.de/courses/cl2-ws16/tex/st.pdf ''Set Theory in Type Theory''], Lecture Notes, Saarland University, Jan. 2015</ref><ref>Gert Smolka and Kathrin Stark, [https://www.ps.uni-saarland.de/Publications/documents/SmolkaStark_2016_Hereditarily.pdf ''Hereditarily Finite Sets in Constructive Type Theory''], Proc. of ITP 2016, Nancy, France, Springer LNCS, May 2015</ref> Such principles are relevant for the standard modeling of individual [[Set-theoretic definition of natural numbers|Neumann ordinals]]. Axiom formulations also exist that pair Union and Replacement in one. While postulating Replacement is not a necessity in the design of a weak constructive set theory that is bi-interpretable with Heyting arithmetic <math>{\mathsf{HA}}</math>, some form of induction is. For comparison, consider the very weak classical theory called [[General set theory]] that interprets the class of natural numbers and their arithmetic via just Extensionality, Adjunction and full Separation.

The discussion now proceeds with axioms granting existence of objects which, in different but related form, are also found in [[dependent type theory|dependent type theories]], namely [[dependent type|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 index [[Domain of a function|domains]], say the formal differentiation of a [[generating function]] or the addition of two Cauchy sequences.

=== ECST ===
For some fixed predicate <math>I</math> and a set <math>a</math>, the statement <math>I(a)\land\big(\forall y. I(y)\to a\subset y\big)</math> expresses that <math>a</math> is the smallest (in the sense of "<math>\subset</math>") among all sets <math>y</math> for which <math>I(y)</math> holds true, and that it is always a subset of such <math>y</math>. 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,
:<math>\big(\exists z. z\in A\big) \land \forall (x\in A). \exists (s\in A). x \in s</math>.
More concretely, denote by <math>\mathrm{Ind}_A</math> the inductive property,
:<math>(0\in A)\land\forall (x\in A). Sx \in A</math>.
In terms of a predicate <math>Q</math> underlying the class so that <math>\forall x. (x\in A)\leftrightarrow Q(x)</math>, the latter translates to <math>Q(0) \land \forall x. \big(Q(x)\to Q(Sx)\big)</math>.

Write <math>\bigcap B</math> for the general intersection <math>\{x\mid\forall (y\in B). x\in y\}</math>. (A variant of this definition may be considered which requires <math>\cap B\subset\cup B</math>, but we only use this notion for the following auxiliary definition.)

One commonly defines a class <math>\omega=\bigcap\{y\mid \mathrm{Ind}_y\}</math>, the intersection of all inductive sets. (Variants of this treatment may work in terms of a formula that depends on a set parameter <math>w</math> so that <math>\omega\subset w</math>.) The class <math>\omega</math> exactly holds all <math>x</math> fulfilling the unbounded property <math>\forall y.\mathrm{Ind}_y\to x\in y</math>. The intention is that if inductive sets exist at all, then the class <math>\omega</math> shares each common natural number with them, and then the proposition <math>\omega\subset A</math>, by definition of "<math>\subset</math>", implies that <math>Q</math> holds for each of these naturals. While bounded separation does not suffice to prove <math>\omega</math> 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 <math>{\mathsf {ECST}}</math> has the axiom of <math>{\mathsf {BCST}}</math> as well as the postulate
{| border=1 style="border:0px"
| style="border:1px solid #000000; padding:1.0em; background-color:#F8F9FA" |
[[Axiom of infinity|Strong Infinity]]
; <math>\exists w. \Big( \mathrm{Ind}_w\, \land\, \big(\forall y. \mathrm{Ind}_y\to w\subset y\big) \Big)</math>
|}
Going on, one takes the symbol <math>\omega</math> to denote the now unique smallest inductive set, an unbounded [[von Neumann ordinal]]. It contains the empty set and, for each set in <math>\omega</math>, another set in <math>\omega</math> that contains one element more.

Symbols called zero and successor are in the [[Signature (logic)|signature]] of the theory of [[Peano arithmetic|Peano]]. In <math>{\mathsf {BCST}}</math>, the above defined successor of any number also being in the class <math>\omega</math> 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 <math>S</math> come easily. Fourthly, in <math>{\mathsf {ECST}}</math>, where <math>\omega</math> is a set, <math>S</math> on <math>\omega</math> can be proven to be an injective operation.

For some predicate of sets <math>P</math>, the statement <math>\forall S. (S\subset\omega\to P(S))</math> claims <math>P</math> holds for all subsets of the set of naturals. And the axiom now proves such sets do exist. Such quantification is also possible in [[second-order arithmetic]].

The pairwise order "<math><</math>" on the naturals is captured by their membership relation "<math>\in</math>". The theory proves the order as well as the equality relation on this set to be decidable. Not only is no ''number'' smaller than <math>0</math>, but induction implies that among subsets of <math>\omega</math>, it is exactly the empty set which has no least member. The contrapositive of this proves the double-negated [[least number principle|least number existence]] for all non-empty subsets of <math>\omega</math>. Another valid principle also classically equivalent to it is least number existence for all inhabited detachable subsets. That said, the bare existence claim for the inhabited subset <math>b:=\{z\in 1\mid P\}\cup\{1\}</math> of <math>\omega</math> is equivalent to excluded middle for <math>P</math>, and a constructive theory will therefore not prove <math>\omega</math> to be [[well-order]]ed.

==== Weaker formulations of infinity ====
Should it need motivation, the handiness of postulating an unbounded set of numbers in relation to other inductive properties becomes clear in the discussion of arithmetic in set theory further below. But as is familiar from classical set theory, also weak forms of Infinity can be formulated. For example, one may just postulate the existence of some inductive set, <math>\exists y. \mathrm{Ind}_y</math> - such an existence postulate suffices when full Separation may then be used to carve out the inductive subset <math>w</math> 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 <math>\Delta_0</math> predecessor existence property in the sense of the [[Set-theoretic definition of natural numbers|von Neumann model]]:
:<math>\forall m. (m \in w) \leftrightarrow \big(m=0 \lor \exists (p \in w). Sp = m\big)</math>
Without making use of the notation for the previously defined successor notation, the extensional equality to a successor <math>Sp = m</math> is captured by <math>\forall n. (n\in m) \leftrightarrow (n = p \lor n \in p)</math>. This expresses that all elements <math>m</math> are either equal to <math>0</math> or themselves hold a predecessor set <math>p\in w</math> which shares all other members with <math>m</math>.

Observe that through the expression "<math>\exists(p\in w)</math>" on the right hand side, the property characterizing <math>w</math> by its members <math>m</math> here syntactically again contains the symbol <math>w</math> itself. Due to the bottom-up nature of the natural numbers, this is tame here. Assuming <math>\Delta_0</math>-set induction on top of <math>{\mathsf{ECST}}</math>, no two different sets have this property.
Also note that there are also [[Axiom of infinity#Extracting the natural numbers from the infinite set|longer formulations]] of this property, avoiding "<math>\exists(p\in w)</math>" in favor unbounded quantifiers.

==== Number bounds ====
Adopting an Axiom of Infinity, the set-bounded quantification legal in predicates used in <math>\Delta_0</math>-Separation then explicitly permits numerically unbounded quantifiers - the two meanings of "bounded" should not be confused.
With <math>\omega</math> at hand, call a class of numbers <math>I\subset\omega</math> '''bounded''' if the following ''existence'' statement holds
:<math>\exists(m\in \omega).\forall(n\in\omega).(n\in I\to n<m)</math>
This is a statements of finiteness, also equivalently formulated via <math>m\le n\to n\notin I</math>. Similarly, to reflect more closely the discussion of functions below, consider the above condition in the form <math>\exists(m\in \omega).\forall(n\in I).(n<m)</math>.
For decidable properties, these are <math>\Sigma_2^0</math>-statements in arithmetic, but with the Axiom of Infinity, the two quantifiers are set-bound.

For a class <math>C</math>, the logically positive unboundedness statement
:<math>\forall(k\in\omega).\exists(j\in\omega).(k\le j\land j\in C)</math>
is now also one of infinitude. It is <math>\Pi_2^0</math> 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 <math>\omega</math>.

==== Moderate induction in ECST ====
In the following, an initial segment of the natural numbers, i.e. <math>\{n\in\omega\mid n<m\}</math> for any <math>m\in\omega</math> and including the empty set, is denoted by <math>\{0, 1, \dots, m-1\}</math>. This set equals <math>m</math> and so at this point "<math>m - 1</math>" is mere notation for its predecessor (i.e. not involving subtraction function).

It is instructive to recall the way in which a theory with set comprehension and extensionality ends up encoding predicate logic. Like any class in set theory, a set can be read as corresponding to predicates on sets. For example, an integer is even if it is a member of the set of even integers, or a natural number has a successor if it is a member of the set of natural numbers that have a successor. 
For a less primitive example, fix some set <math>y</math> and let <math>Q(n)</math> denote the existential statement that the function space on the finite ordinal into <math>y</math> exist. The predicate will be denoted <math>\exists h. h\simeq y^{\{0,1,\dots,n-1\}}</math> below, and here the existential quantifier is not merely one over natural numbers, nor is it bounded by any other set. Now a proposition like the finite exponentiation principle <math>\forall(n\in\omega). Q(n)</math> and, less formally, the equality <math>\omega = \{n\in \omega \mid Q(n)\}</math> are just two ways of formulating the same desired statement, namely an <math>n</math>-indexed conjunction of existential propositions where <math>n</math> ranges over the set of all naturals. Via extensional identification, the second form expresses the claim using notation for subclass comprehension and the bracketed object on the right hand side may not even constitute a set. If that subclass is not provably a set, it may not actually be used in many set theory principles in proofs, and establishing the universal closure <math>\forall(n\in\omega). Q(n)</math> as a theorem may not be possible. The set theory can thus be strengthened by more set existence axioms, to be used with predicative ''bounded'' Separation, but also by just postulating stronger <math>\forall</math>-statements.

The second universally quantified conjunct in the strong axiom of Infinity expresses mathematical induction for all <math>y</math> in the universe of discourse, i.e. for sets. This is because the consequent of this clause, <math>\omega\subset y</math>, states that all <math>n\in\omega</math> fulfill the associated predicate. Being able to use predicative separation to define subsets of <math>\omega</math>, the theory proves induction for all predicates <math>\phi(n)</math> involving only set-bounded quantifiers. This role of set-bounded quantifiers also means that more set existence axioms impact the strength of this induction principle, further motivating the function space and collection axioms that will be a focus of the rest of the article. Notably, <math>{\mathsf {ECST}}</math> already validates induction with quantifiers over the naturals, and hence induction as in the first-order arithmetic theory <math>{\mathsf {HA}}</math>. 
The so called axiom of [[mathematical induction|full mathematical induction]] for any predicate (i.e. class) expressed through set theory language is far stronger than the bounded induction principle valid in <math>{\mathsf {ECST}}</math>. The former induction principle could be directly adopted, closer mirroring second-order arithmetic. In set theory it also follows from full (i.e. unbounded) Separation, which says that all predicates on <math>\forall</math> are sets. Mathematical induction is also superseded by the (full) Set induction axiom.

Warning note: In naming induction statements, one must take care not to conflate terminology with arithmetic theories. The first-order induction schema of natural number arithmetic theory claims induction for all predicates definable in the language of [[first-order arithmetic]], namely predicates of just numbers. So to interpret the axiom schema of <math>{\mathsf {HA}}</math>, one interprets these arithmetical formulas. In that context, the [[Bounded quantifier|bounded quantification]] specifically means quantification over a finite range of numbers.
One may also speak about the induction in the first-order but two-sorted theory of so-called second-order arithmetic <math>{\mathsf {Z}}_2</math>, 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 first-order arithmetic definable ones. In the program of [[reverse mathematics]], all mathematical objects discussed are encoded as naturals or subsets of naturals. Subsystems of <math>{\mathsf {Z}}_2</math> with very low [[Arithmetical hierarchy|complexity]] comprehension studied in that framework have a language that does not merely express [[arithmetical set]]s, while all sets of naturals particular such theories prove to exist are just [[computable set]]s. 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.<ref>{{Cite arXiv|eprint=1804.05495|title=Constructive Reverse Mathematics|class=math.LO|last1=Diener|first1=Hannes|year=2020}}</ref> <math>{\mathsf {Z}}_2</math> shall moreover not be confused with the second-order formulation of Peano arithmetic <math>{\mathsf {PA}}_2</math>. Typical set theories like the one discussed here are also first-order, 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 (logic)|signature]]. Likewise, care must always be taken with insights about [[Total functional programming|totality]] of functions. In [[computability theory]], the [[μ operator]] enables all partial [[general recursive function]]s (or programs, in the sense that they are Turing computable), including ones e.g. non-primitive recursive but <math>{\mathsf {PA}}</math>-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 ===
==== 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 <math>R</math> express a property such that a mathematical framework validates what amounts to the statement
:<math>\forall (a\in A). \exists (c\in C). R(a, c)</math>
A constructive proof calculus may validate such a judgement in terms of programs on represented domains and some object representing a concrete assignment <math>a\mapsto c_a</math>, providing a particular choice of value in <math>C</math> (a ''unique'' one), for each input from <math>A</math>. Expressed through the [[Skolem normal form|rewriting]] <math>\forall (a\in A). R(a, c_a)</math>, this function object may be understood as [[Witness (mathematics)|witnessing]] the proposition. Consider for example the notions of proof in through [[Realizability|realizability theory]] or function terms in a [[Curry–Howard correspondence|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 function|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 T predicate#Normal form theorem|Kleene's normal form theorem]], each partial recursive function on the naturals computes, for the values where it terminates, the same as <math>a \mapsto U(\mu w. T_1(e, a, w))</math>, for some partial function program index <math>e\in{\mathbb N}</math>, and any index will constitute some partial function. A program can be associated with a <math>e</math> and may be said to be <math>T_1</math>-total whenever a theory proves <math>\forall a. \exists w. T_1(e, a, w)</math>, where <math>T_1</math> amounts to a primitive recursive program and <math>w</math> is related to the execution of <math>e</math>. [[Georg Kreisel|Kreisel]] proved that the class of partial recursive functions proven <math>T_1</math>-total by <math>{\mathsf {HA}}</math> is not enriched when <math>{\mathrm {PEM}}</math> is added.<ref>{{Citation|first1=Morten|last1=Sørenson|first2=Paweł|last2=Urzyczyn|title=Lectures on the Curry-Howard Isomorphism|citeseerx = 10.1.1.17.7385 |year=1998}}, p. 239</ref> As a predicate in <math>e</math>, this totality constitutes an [[Rice's theorem|undecidable]] subset of indices, highlighting that the recursive world of functions between the naturals is already captured by a set dominated by <math>{\mathbb N}</math>. As a third warning, note that this notion is really about programs and several indices will in fact constitute the same function, in the [[Extensionality|extensional]] sense.

A theory in [[first-order logic]], such as the axiomatic set theories discussed here, comes with a joint notion of [[total relation|total]] and [[Binary relation#Specific types of binary relations|functional]] for a binary predicate <math>R</math>, namely <math>\forall a. \exists! c. R(a, c)</math>. Such theories relate to programs only indirectly. If <math>S</math> denotes the successor operation in a formal language of a theory being studied, then any number, e.g. <math>{\mathrm {SSS0}}</math> (the number three), may [[metalogic]]ally be related to the standard numeral, e.g. <math>{\underline{\mathrm {SSS0}}}=SSS0</math>. 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 sub-theories of <math>{\mathsf {PA}}</math>, classical [[Robinson arithmetic]] <math>{\mathsf Q}</math> 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 <math>T_1</math>-total recursive functions here, it is a meta-theorem that the language of arithmetic expresses them by <math>\Sigma_1</math>-predicates <math>G</math> encoding their graph such that <math>{\mathsf Q}</math> ''represents'' them, in the sense that it correctly proves or rejects <math>G({\underline{\mathrm {a}}}, {\underline{\mathrm {c}}})</math> for any input-output pair of numbers <math>\mathrm {a}</math> and <math>\mathrm {c}</math> in the meta-theory. Now given a correctly representing <math>G</math>, the predicate <math>G_\mathrm{least}(a, c)</math> defined by <math>G(a, c) \land \forall(n < c). \neg G(a, n)</math> represents the recursive function just as well, and as this explicitly only validates the smallest return value, the theory also proves functionality for all inputs <math>{\mathrm a}</math> in the sense of <math>{\mathsf Q} \vdash \exists! c. G_\mathrm{least}(\underline{ {\mathrm a}}, c)</math>. Given a representing predicate, then at the cost of making use of <math>{\mathrm {PEM}}</math>, one can always also systematically (i.e. with a <math>\forall a.</math>) prove the graph to be total functional.<ref>{{cite book |last1=Smith |first1=Peter |title=An introduction to Gödel's Theorems |date=2007 |url=https://www.logicmatters.net/resources/pdfs/godelbook/GodelBookLM.pdf |publisher=Cambridge University Press |location=Cambridge, U.K. |isbn=978-0-521-67453-9 |mr=2384958}}, p. 297</ref>

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 [[halting problem|diagonal halting problem]], which cannot have a <math>T_1</math>-total index, it is <math>{\mathsf {HA}}</math>-independent whether the corresponding graph predicate on <math>{\mathbb N}\times\{0,1\}</math> (a [[decision problem]]) is total functional, but <math>{\mathrm {PEM}}</math> implies that it is. Proof theoretical [[Fast-growing hierarchy#Points of interest|function hierarchies]] provide examples of predicates proven total functional in systems going beyond <math>{\mathsf {PA}}</math>.
Which sets proven to exist do constitute a total function, in the sense introduced next, also always depends on the axioms and the proof calculus. Finally, note that the soundness of halting claims is a metalogical property beyond consistency, i.e. a theory may be consistent and from it one may prove that some program will eventually halt, despite this never actually occurring when said program is run. More formally, assuming consistency of a theory does not imply it is also arithmetically [[ω-consistent theory#Definition|<math>\Sigma_1</math>-sound]].

==== Total functional relations ====
In set theory language here, speak of a '''function''' class when <math>f\subset A\times C</math> and provenly
:<math>\forall (a\in A).\, \exists! (c\in C). \langle a, c\rangle \in f</math>.
Notably, this definition involves quantifier explicitly asking for existence - an aspect which is particularly important in the constructive context. In words: For every <math>a</math>, it demands the unique existence of a <math>c</math> so that <math>\langle a, c\rangle \in f</math>. 
In the case that this holds one may use [[function application]] bracket notation and write <math>f(a) = c</math>. The above property may then be stated as <math> \forall (a\in A).\, \exists! (c\in C). f(a) = c </math>. 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 <math>C^A</math> (also written <math>^AC</math>) denote the class of sets that fulfill the function property. This is the class of functions from <math>A</math> to <math>C</math> in a pure set theory. Below the notation <math>x\to y</math> is also used for <math>y^x</math>, for the sake of distinguishing it from ordinal exponentiation. When functions are understood as just function graphs as here, the membership proposition <math>f\in C^A</math> is also written <math>f\colon A\to C</math>. The Boolean-valued <math>\chi_B\colon A\to\{0,1\}</math> are among the classes discussed in the next section.

By construction, any such function respects equality in the sense that <math>(x = y) \to f(x) = f(y)</math>, for any inputs from <math>A</math>. This is worth mentioning since also more broader concepts of "assignment routines" or "operations" exist in the mathematical literature, which may not in general respect this. Variants of the functional predicate definition using [[apartness relations]] on [[setoid]]s 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 <math>(A\times C)\times\{C\}</math>. 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. Similar considerations apply to any treatment of [[partial function]]s and their domains.

If both the domain <math>A</math> and considered codomain <math>C</math> are sets, then the above function 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 '''[[Bijection#Inverses|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 non-injectivity. And regarding surjectivity, similar considerations exist for outlier-[[Subcountability#Subcountable and ω-productive are mutually exclusive|production]] 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 <math>A\times C</math>, i.e. the property is expressing not more or less than functionality w.r.t. the inputs from <math>A</math>.
Now if the domain is a set, the function comprehension principle, also called [[Axiom of non-choice|axiom of unique choice]] or non-choice, says that a function as a set, with some codomain, exists well. (And this principle is valid in a theory like <math>{\mathsf {CZF}}</math>. 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 <math>1</math>, 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 <math>{\mathsf{BCST}}</math> that adding a function symbol for a provenly total class function is a conservative extension, despite this formally changing the scope of [[Axiom schema of predicative separation|bounded Separation]].
In summary, in the set theory context the focus is on capturing particular [[total relation]]s that are functional. To delineate the notion of ''function'' in the theories of the previous subsection (a 2-ary 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 ====
One defines three distinct notions involving surjections. For a general set to be ([[Errett Bishop|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 '''non-finite'''. Secondly, for a notion weaker than finite, to be '''finitely indexed''' (or [[Kazimierz Kuratowski|Kuratowski]]-finite) shall mean that there is a surjection from a von Neumann natural number onto it. In programming terms, the element of such a set are accessible in a (ending) [[for-loop]], and only those, while it may not be decidable whether repetition occurred. Thirdly, call a set '''subfinite''' if it is the subset of a finite set, which thus injects into that finite set. Here, a for-loop will access all of the set's members, but also possibly others. For another combined notion, one weaker than finitely indexed, to be '''subfinitely indexed''' means to be in the surjective image of a subfinite set, and in <math>{\mathsf {ETCS}}</math> 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 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. In the third case, validating membership in the set is generally more difficult, and not even membership of its member with respect to some superset of the set is necessary fully understood.
The claim that being finite is equivalent to being subfinite, for all sets, is equivalent to <math>{\mathrm {PEM}}</math>.
More finiteness properties for a set <math>X</math> 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 <math>X</math>. One definition considers some notion of non-injectivity into <math>X</math>. Other definitions consider functions to a fixed superset of <math>X</math> 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 non-finite. The same issue applies to countable sets (not proven countable vs. proven non-countable), et cetera. A surjective map may also be called an enumeration.

==== Infinitude ====
The set <math>\omega</math> itself is clearly unbounded. In fact, for any surjection from a finite range onto <math>\omega</math>, 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 Kuratowski-finite implies being non-finite and indeed the naturals shall not be finite in any sense. Commonly, the word infinite is used for the negative notion of being non-finite. Further, observe that <math>\omega</math>, unlike any of its members, can be put in bijection with some of its proper unbounded subsets, e.g. those of the form <math>w_m:=\{k\in\omega\mid k > m\}</math> for any <math>m\in\omega</math>. This validates the formulations of '''[[Dedekind-infinite]]'''. 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 <math>\omega</math> into it. A set that is even in bijection with <math>\omega</math> may be called countably infinite. A set is '''Tarski-infinite''' if there is a chain of <math>\subset</math>-increasing subsets of it. Here each set has new elements compared to its predecessor and the definition does not speak of sets growing rank. There are indeed plenty of properties characterizing infinitude even in classical <math>{\mathsf {ZF}}</math> and that theory does not prove all non-finite sets to be infinite in the injection existence sense, albeit [[Dedekind-infinite set#Proof of equivalence to infinity, assuming axiom of countable choice|it there holds when]] further assuming countable choice. <math>{\mathsf {ZF}}</math> 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 non-Dedekind-infinite and non-finite (also called Dedekind-finite infinite sets).

Call an inhabited set '''countable''' if there exists a surjection from <math>\omega</math> onto it and '''[[subcountable]]''' if this can be done from some subset of <math>\omega</math>. Call a set '''enumerable''' if there exists an injection to <math>\omega</math>, 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 <math>\omega</math> 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 '''[[Equinumerosity|equinumeros]]''' to <math>\omega</math>.

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 <math>X</math> is given when one can produce a member in the compliment of any of <math>X</math>'s countable subsets. More [[finite set#Necessary and sufficient conditions for finiteness|properties of finiteness]] may be defined as negations of such properties, et cetera.

==== Characteristic functions ====
Separation lets us cut out subsets of products <math>A\times C</math>, at least when they are described in a bounded fashion. Given any <math>B\subset A</math>, one is now led to reason about classes such as
:<math>X_B:=\big\{\langle x, y\rangle \in A\times \{0,1\} \mid (x\in B\land y=1) \lor (x \notin B\land y=0) \big\}.</math>
Since <math>\neg(0=1)</math>, one has 
:<math>\big(a\in B \ \leftrightarrow\, \langle a, 1\rangle\in X_B\big) \,\land\, \big(a\notin B \ \leftrightarrow\, \langle a, 0\rangle\in X_B\big)</math>
and so 
:<math>\big(a\in B \lor a\notin B\big)\ \leftrightarrow\ \exists!(y\in\{0,1\}). \langle a, y\rangle\in X_B</math>.
But be aware that in absence of any non-constructive axioms <math>a\in B</math> may in generally [[Undecidable problem|not be decidable]], since one requires an explicit proof of either disjunct. Constructively, when <math>\exists(y\in\{0,1\}). \langle x, y\rangle \in X_B</math> cannot be [[Witness (mathematics)|witness]]ed for all the <math>x\in A</math>, or uniqueness of the terms <math>y</math> associated with each <math>x</math> cannot be proven, then one cannot judge the comprehended collection to be total functional.
Case in point: The classical derivation of [[Schröder–Bernstein theorem|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 <math>{\mathsf{IZF}}</math> plus constructive principles.<ref>{{Cite arXiv|eprint=1904.09193|title=Cantor-Bernstein implies Excluded Middle|class=math.LO|last1=Pradic|first1=Cécilia|last2=Brown|first2=Chad E.|year=2019}}</ref> So to the extent that [[intuitionism|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 <math>{\mathsf{ZF}}</math>, the development in this section still always permits "function on <math>\omega</math>" to be interpreted as a completed object that is also not necessarily given as [[Choice sequence|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 [[Spread (intuitionism)|spread]]s.

If indeed one is given a function <math>\chi_B\colon A\to\{0,1\}</math>, it is the [[characteristic function]] actually deciding membership in some detachable subset <math>B\subset A</math> and
:<math>B=\{n\in\omega\mid\chi_B(n)=1\}.</math>
Per convention, the detachable subset <math>B</math>, <math>\chi_B</math> as well as any equivalent of the formulas <math>n\in B</math> and <math>\chi_B(n)=1</math> (with <math>n</math> free) may be referred to as a '''decidable property or set on <math>A</math>'''.

One may call a collection <math>A</math> searchable for <math>\chi_B</math> if existence is actually decidable,
:<math>\exists(x\in A).\chi_B(x)=1\ \lor\ \forall(x\in A).\chi_B(x)=0.</math>
Now consider the case <math>A=\omega</math>. If <math>\chi_B(0)=0</math>, say, then the range <math>\{0\}\subset R\subset\{0,1\}</math> of <math>\chi_B</math> is an inhabited, counted set, by Replacement. However, the <math>R</math> need not be again a decidable set itself, since the claim <math>R=\{0\}</math> is equivalent to the rather strong <math>\forall n. \chi_B(n)=0</math>. Moreover, <math>R=\{0\}</math> is also equivalent to <math>B=\{\}</math> and so one can state undecidable propositions about <math>B</math> also when membership in <math>B</math> is decidable.
This also plays out like this classically in the sense that statements about <math>B</math> may be [[Independence (mathematical logic)|independent]], but any classical theory then nonetheless claims the joint proposition <math>B=\{\}\lor \neg(B=\{\})</math>. Consider the set <math>B</math> of all indices of proofs of an inconsistency of the theory at hand, in which case the universally closed statement <math>B=\{\}</math> is a consistency claim. In terms of arithmetic principles, assuming decidability of this would be <math>\Pi_1^0</math>-<math>{\mathrm {PEM}}</math> or arithmetic <math>\forall</math>-<math>{\mathrm {PEM}}</math>. This and the [[Limited principle of omniscience|stronger related <math>{\mathrm {LPO}}</math>]], or arithmetic <math>\exists</math>-<math>{\mathrm {PEM}}</math>, is discussed below.

==== Witness of apartness ====
The [[identity of indiscernibles]], which in the first-order context is a higher order principle, holds that the equality <math>x=y</math> of two terms <math>x</math> and <math>y</math> necessitates that ''all'' predicates <math>P</math> agree on them. And so ''if there exists a'' predicate <math>P</math> that distinguishes two terms <math>x</math> and <math>y</math> in the sense that <math>P(x)\land\neg P(y)</math>, then the principle implies that the two terms do not coincide. A form of this may be expressed set theoretically: <math>x, y\in A</math> may be deemed apart if there exists a subset <math>B\subset A</math> such that one is a member and the other is not. Restricted to detachable subsets, this may also be formulated concisely using characteristic functions <math>\chi_B\in \{0,1\}^A</math>. Indeed, the latter does not actually depend on the codomain being a binary set: Equality is rejected, i.e. <math>x \neq y</math> is proven, as soon it is established that ''not all'' functions <math>f</math> on <math>A</math> validate <math>f(x)=f(y)</math>, a logically negative condition.

One may on any set <math>A</math> define the logically positive apartness relation
:<math>x\,\#_A\,y\,:=\,\exists (f\in {\mathbb N}^A). f(x)\neq f(y)</math>
As the naturals are discrete, for these functions the negative condition is equivalent to the (weaker) double-negation of this relation. Again in words, equality of <math>x</math> and <math>y</math> implies that no coloring <math>f\in {\mathbb N}^A</math> can distinguish them - and so to rule out the former, i.e. to prove <math>x\neq y</math>, one must merely rule out the latter, i.e. merely prove <math>\neg\neg(x\,\#_A\,y)</math>.

==== Computable sets ====
Going back to more generality, given a general predicate <math>Q</math> on the numbers (say one defined from [[Kleene's T predicate]]), let again
:<math>B:=\{n\in\omega\mid Q(n)\}.</math>
Given any natural <math>n\in\omega</math>, then
:<math>\big(Q(n)\lor \neg Q(n)\big) \leftrightarrow \big(n\in B\lor n\notin B\big).</math>
In classical set theory, <math>\forall(n\in\omega). Q(n)\lor \neg Q(n)</math> by <math>{\mathrm {PEM}}</math> and so excluded middle also holds for subclass membership. If the class <math>B</math> has no numerical bound, then successively going through the natural numbers <math>n</math>, and thus "listing" all numbers in <math>B</math> by simply skipping those with <math>n\notin B</math>, classically always constitutes an increasing surjective sequence <math>b\colon\omega\twoheadrightarrow B</math>. 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|''effectively'' computable]], or programmatically listable in praxis.

In [[computability theory]], the [[computable set]]s are ranges of non-decreasing total functions ''in the recursive sense'', at the level <math>\Sigma_1^0 \cap \Pi_1^0 = \Delta_1^0</math> of the [[arithmetical hierarchy]], and not higher. Deciding a predicate at that level amounts to solving the task of eventually finding a [[Certificate (complexity)|certificate]] that either validates or rejects membership.
As not every predicate <math>Q</math> is computably decidable, also the theory <math>{\mathsf{CZF}}</math> alone will not claim (prove) that all unbounded <math>B\subset \omega</math> are the range of some bijective function with domain <math>\omega</math>. 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 set|computably enumerable]] ones at <math>\Sigma_1^0</math>.

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 [[Many-one reduction#Subsets of natural numbers|particular injections]] in opposing directions.

==== Boundedness criteria ====
Any subset <math>B\subset\omega</math> injects into <math>\omega</math>. If <math>B</math> is decidable and inhabited with <math>y_0\in B</math>, the sequence
:<math>q := \big\{\langle x, y\rangle \in \omega\times B \mid (x\in B\land y=x) \lor (x \notin B\land y=y_0) \big\}</math>
i.e.
:<math>q(x) := \begin{cases} 
x   & x\in B \\
y_0  & x\notin B \\
\end{cases}</math>
is surjective onto <math>B</math>, making it a counted set. That function also has the property <math>\forall(x\in B). q(x)=x</math>.

Now consider a countable set <math>R\subset\omega</math> that is ''bounded'' in the sense defined previously. Any sequence taking values in <math>R</math> is then numerically capped as well, and in particular eventually does not exceed the identity function on its input indices. Formally,
:<math>\forall(r\colon\omega\to R).\exists(m\in\omega).\forall(k\in\omega). k>m \to r(k) < k</math>
A set <math>I</math> such that this loose bounding statement holds for all sequences taking values in <math>I</math> (or an equivalent formulation of this property) is called '''pseudo-bounded'''. The intention of this property would be to still capture that <math>I\subset\omega</math> is eventually exhausted, albeit now this is expressed in terms of the function space <math>I^\omega</math> (which is bigger than <math>I</math> in the sense that <math>I</math> always injects into <math>I^\omega</math>). The [[Bounded set (topological vector space)|related notion]] familiar from topological vector space theory is formulated in terms of ratios going to zero for all sequences (<math>\tfrac{r(k)}{k}</math> in the above notation). For a decidable, inhabited set, validity of pseudo-boundedness, together with the counting sequence defined above, grants a bound for all the elements of <math>I</math>.

The principle that any inhabited, pseudo-bounded subset of <math>\omega</math> that is just countable (but not necessarily decidable) is always also bounded is called <math>\mathrm{BD}</math>-<math>{\mathbb N}</math>. The principle also holds generally in many constructive frameworks, such as the Markovian base theory <math>{\mathsf {HA}}+{\mathrm {ECT}}_0+{\mathrm {MP}}</math>, which is a theory postulating exclusively lawlike sequences with nice number search termination properties. However, <math>\mathrm{BD}</math>-<math>{\mathbb N}</math> is independent of <math>{\mathsf {IZF}}</math>.

=== Choice functions ===
Not even classical <math>{\mathsf{ZF}}</math> proves each union of a countable set of two-element sets to be countable again. Indeed, [[model theory|models]] of <math>{\mathsf{ZF}}</math> have been [[forcing (mathematics)|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 still independent of <math>{\mathsf{ZF}}</math> - A naive proof strategy for that statement fails at the accounting of infinitely many [[existential instantiation]]s.

A choice principle postulates that certain selections can always be made in a joint fashion in the sense that they are also manifested as a single set function in the theory. As with any independent axiom, this raises the proving capabilities while restricting the scope of possible (model-theoretic) 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 <math>{\mathsf{ZF}}</math> does [[Absoluteness (logic)#Shoenfield's absoluteness theorem|not prove any new <math>\Pi_4^1</math>-theorems]], but it is strictly non-constructive, as shown below. The development here proceeds in a fashion agnostic to any of the variants described next.<ref>Michael Rathjen, [http://www1.maths.leeds.ac.uk/~rathjen/acend.pdf ''Choice principles in constructive and classical set theories''], Cambridge University Press: 31 March 2017</ref>
* [[Axiom of countable choice]] <math>{\mathrm{AC}_\omega}</math> (or <math>{\mathrm{CC}}</math>): If <math>g\colon\omega\to z</math>, one can form the one-to-many relation-set <math>\{\langle n, u\rangle\mid n\in\omega\land u\in g(n)\}</math>. The axiom of countable choice would grant that whenever <math>\forall (n\in\omega). \exists u. u\in g(n)</math>, 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 <math>{\mathsf{ZF}}</math> and countable choice is not <math>\Sigma_4^1</math>-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 <math>g</math>, giving the weak countable choice into countable, finite or even just binary sets (<math>{\mathrm{AC}_{\omega,2}}</math>). One may consider the version of countable choice for functions into <math>\omega</math> (called <math>{\mathrm{AC}_{\omega,\omega}}</math> or <math>{\mathrm{AC}_{00}}</math>), as is implied by the [[Church's thesis (constructive mathematics)|constructive Church's thesis principle]], i.e. by postulating that all total arithmetical relations are recursive. <math>{\mathrm{CT}_0}</math> 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 <math>\Pi_1^0</math>-<math>{\mathrm{AC}_{\omega,2}}</math>). The weak [[Kőnig's lemma]] <math>{\mathrm {WKL}}</math>, which breaks strictly recursive mathematics as further discussed below, is stronger than <math>\Pi_1^0</math>-<math>{\mathrm{AC}_{\omega,2}}</math> 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 non-constructive principle of more logical flavor, [[Limited principle of omniscience|<math>{\mathrm {LLPO}}</math>]]. Constructively, a weak form of choice is required for well-behaved [[Construction of the real numbers#Construction from Cauchy sequences|Cauchy reals]]. Countable choice is not valid in the [[categorical logic|internal logic]] of a general [[topos]], which can be seen as [[model theory|models]] of constructive set theories.
* [[Axiom of dependent choice]] <math>{\mathrm{DC}}</math>: Countable choice is implied by the more general axiom of dependent choice, extracting a sequence in an inhabited <math>z</math>, given any [[Binary relation|entire relation]] <math>R\subset z\times z</math>. In set theory, this sequence is again an infinite set of pairs, a subset of <math>\omega\times z</math>. So one is granted to pass from several existence statements to function existence, itself granting unique-existence statements, for every natural. An appropriate formulation of dependent choice is adopted in several constructive frameworks, e.g., by some schools that understand unending sequences as ongoing constructions instead of completed objects. At least those cases seem benign where, for any <math>x\in z</math>, next value existence <math>\exists(y\in z). x R y</math> can be validated in a computable fashion. The corresponding recursive function <math>\omega\to z</math>, if it exists, is then conceptualized as being able to return a value at infinitely many potential inputs <math>n\in\omega</math>, 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#The recursion theorem|recursion theorem]], one is already given a unique choice at each step, and that theorem lets one combine them to a function on <math>\omega</math>. So also with <math>{\mathrm{DC}}</math> one may consider forms of the axiom with restrictions on <math>R</math>. Via the bounded separation axiom in <math>{\mathsf{ECST}}</math>, the principle also is equivalent to a schema in two bounded predicate variables: Keeping all quantifiers ranging over <math>z</math>, one may further narrow this set domain using a unary <math>\Delta_0</math>-predicate variable, while also using any 2-ary <math>\Delta_0</math>-predicate instead of the relation set <math>R</math>. Dependent choice does not imply that subsingleton domains have a choice function.
* Relativized dependent choice <math>{\mathrm{RDC}}</math>: This is the schema just using two general classes, instead of requiring <math>z</math> and <math>R</math> be sets. The domain of the choice function granted to exist is still just <math>\omega</math>. Over <math>{\mathsf{ECST}}</math>, it implies full mathematical induction, which, in turn allows for function definition on <math>\omega</math> through the recursion schema. When <math>{\mathrm{RDC}}</math> is restricted to <math>\Delta_0</math>-definitions, it still implies mathematical induction for <math>\Sigma_1</math>-predicates (with an existential quantifier over sets) as well as <math>{\mathrm{DC}}</math>. In <math>{\mathsf{ZF}}</math>, the schema <math>{\mathrm{RDC}}</math> is equivalent to <math>{\mathrm{DC}}</math>.
* <math>\Pi\Sigma</math>-<math>\mathrm{AC}</math>: A family of sets is better controllable if it comes indexed by a function. A set <math>b</math> is a base if all indexed families of sets <math>i_s\colon b\to s</math> over it, have a choice function <math>f_s</math>, i.e. <math>\forall (x\in b). f_s(x)\in i_s(x)</math>. A collection of sets holding <math>\omega</math> and its elements and which is closed by taking indexed sums and products (see [[dependent type]]) is called <math>\Pi\Sigma</math>-closed. While the axiom that all sets in the smallest <math>\Pi\Sigma</math>-closed class are a base does need some work to formulate, it is the strongest choice principle over <math>{\mathsf {CZF}}</math> that holds in the type theoretical interpretation <math>{\mathsf {ML_1V}}</math>.
* [[Axiom of choice]] <math>{\mathrm{AC}}</math>: This is the "full" choice function postulate concerning domains that are general sets <math>\{z,\dots\}</math> 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 <math>{\mathcal P}_{\mathbb R}\setminus 1</math>. For this collection there can be no uniform element selection prescription that provably constitutes a choice function on the base of <math>{\mathsf{ZF}}</math>. Also, when restricted to the [[Borel algebra]] of the reals, <math>{\mathsf{ZF}}</math> alone does not prove the existence of a function selecting a member from each non-empty such [[Borel measure#On the real line|Lebesgue-measurable subset]]. (The set <math>{\mathcal B}({\mathbb R})</math> is the [[σ-algebra]] generated by the [[Interval (mathematics)|intervals]] <math>I:=\{(x, y\,] \mid x, y \in {\mathbb R}\}</math>. It strictly includes those intervals, in the sense of <math>I\subsetneq{\mathcal B}({\mathbb R})\subsetneq{\mathcal P}_{\mathbb R}</math>, but in <math>{\mathsf{ZF}}</math> also only has the cardinality of the reals itself.) Striking existence claims implied by the axiom are abound. <math>{\mathsf{ECST}}</math> proves <math>\omega</math> exists and then the axiom of choice also implies dependent choice. Critically in the present context, it moreover also implies instances of <math>{\mathrm {PEM}}</math> via Diaconescu's theorem. For <math>{\mathsf{ECST}}</math> or theories extending it, this means full choice at the very least proves <math>{\mathrm {PEM}}</math> for all <math>\Delta_0</math>-formulas, a non-constructive consequence not acceptable, for example, from a computability standpoint. Note that constructively, [[Zorn's lemma]] does not imply choice: When membership in function domains fails to be decidable, the extremal function granted by that principle is not provably always a choice function on the whole domain.

====Diaconescu's theorem====
To highlight the strength of full Choice and its relation to matters of [[intentionality]], one should consider the classes
:<math>a=\{u\in\{0, 1\} \mid (u=0) \lor P\}</math>
:<math>b=\{u\in\{0, 1\} \mid (u=1) \lor P\}</math>
from the proof of [[Diaconescu's theorem]]. They are as contingent as the proposition <math>P</math> 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]], <math>t\in a\leftrightarrow \big(t=0\lor (t=1\land P)\big)</math>. So unconditionally, <math>0\in a</math> as well as <math>1\in b</math>, and in particular they are inhabited. As <math>\neg(0=1)</math> in any model of Heyting arithmetic, using the [[disjunctive syllogism]] both <math>0\in b</math> and <math>1\in a</math> each imply <math>P</math>. The two statements are indeed equivalent to the proposition, as clearly <math>P\to(a=\{0, 1\}\land b=\{0, 1\})</math>. The latter also says that validity of <math>P</math> means <math>a</math> and <math>b</math> share all members, and there are two of these. As <math>a</math> are <math>b</math> are then sets, also <math>P\to (a=b\land\{a,b\}=\{a\})</math> by extensionality. Conversely, assuming they are equal means <math>x\in a\leftrightarrow x\in b</math> for any <math>x</math>, validating all membership statements. So both the membership statements as well as the equalities are found to be equivalent to <math>P</math>. Using the [[contrapositive]] results in the weaker equivalence of disjuncts <math>(P\lor\neg P)\leftrightarrow(a=b\lor\neg(a=b))</math>. Of course, explicitly <math>\neg P\to(a=\{0\}\land b=\{1\})</math> and so one actually finds in which way the sets can end up being different. As functions preserves equality by definition, <math>\neg\big(g(a)=g(b)\big)\to \neg P</math> indeed holds for any <math>g</math> with domain <math>\{a,b\}</math>.

In the following assume a context in which <math>a, b</math> are indeed established to be sets, and thus subfinite sets. The general axiom of choice claims existence of a function <math>f\colon\{a,b\}\to a\cup b</math> with <math>f(z)\in z</math>. It is important that the elements <math>a,b</math> of the function's domain are different than the natural numbers <math>0, 1</math> in the sense that a priori less is known about the former. When forming then union of the two classes, <math>u=0\lor u=1</math> is a necessary but then also sufficient condition. Thus <math>a\cup b = \{0, 1\}</math> and one is dealing with functions <math>f</math> into a set of two ''distinguishable'' values. With choice come the conjunction <math>f(a)\in a \land f(b)\in b</math> in the codomain of the function, but the ''possible'' function return values are known to be just <math>0</math> or <math>1</math>. Using the distributivity, there arises a list of conditions, another disjunction. Expanding what is then established, one finds that either both <math>P</math> as well as the sets equality holds, or that the return values are different and <math>P</math> can be rejected. The conclusion is that the choice postulate actually implies <math>P\lor\neg P</math> whenever a Separation axiom allows for set comprehension using undecidable proposition <math>P</math>.

====Analysis of Diaconescu's theorem====
So full choice is non-constructive in set theory as defined here. The issue is that when propositions are part of set comprehension (like when <math>P</math> is used to separate, and thereby define, the classes <math>a</math> and <math>b</math> from <math>\{0, 1\}</math>), 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 <math>f(a)=1</math> implies <math>P</math> and <math>a=b</math> and this conclusion independently also applies to witnessing <math>f(b)=0</math>. On the other hand, witnessing <math>f(a)=0\land f(b)=1</math> implies the two function arguments are not equal and this rules out <math>P</math>. There are really only three combinations, as the axiom of extensionality in the given setup makes <math>f(a)=1\land f(b)=0</math> 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 <math>\{a,b\}</math>, consider naive function candidates. Firstly, an analysis of the domain is in order. The surjection <math>\{\langle 0, a\rangle, \langle 1, b\rangle\}</math> witnesses that <math>\{a,b\}</math> is finitely indexed. It was noted that its members are subfinite and also inhabited, since regardless of <math>P</math> it is the case that <math>0\in a</math> and <math>1\in b</math>. So naively, this would seem to make <math>f = \{\langle a, 0\rangle, \langle b, 1\rangle\}</math> a contender for a choice function. When <math>P</math> can be rejected, then this is indeed the only option. But in the case of provability of <math>P</math>, when <math>\{a,b\}=\{a\}</math>, there is extensionally only one possible function input to a choice function. So in that situation, a choice function would explicitly have type <math>f\colon\{a\}\to\{0, 1\}</math>, for example <math>f = \{\langle a, 0\rangle\}</math> and this would rule out the initial contender. For general <math>P</math>, the domain of a would-be choice function is not concrete but contingent on <math>P</math> and not proven finite. When considering the above functional assignment <math>f(a)=0</math>, then neither unconditionally declaring <math>f(b)=1</math> nor <math>f(b)=0</math> is necessarily consistent. Having identified <math>1</math> with <math>\{0\}</math>, the two candidates described above can be represented simultaneously via <math>f = \{\langle a, 0\rangle, \langle b, B_\neg\rangle\}</math> (which is not proven finite either) with the subfinite "truth value of <math>\neg P</math>" given as <math>B_\neg:=\{u\in \{0\} \mid \neg P\}</math>. As <math>(P\to (B_\neg=0))\land(\neg P\to (B_\neg=1))</math>, postulating <math>P</math>, or <math>\neg P</math>, or the classical principle <math> P\lor\neg P</math> here would indeed imply that <math>B_\neg</math> is a natural, so that the latter set <math>f</math> constitutes a choice function into <math>\{0, 1\}</math>. 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 <math>P</math> or whether <math>\neg P</math> does hold. Vice versa, the third and last candidate <math>f = \{\langle b, 1\rangle\}</math> can be captured as part of <math>f = \{\langle a, B\rangle,\langle b, 1\rangle \}</math>, where <math>B:=\{u\in \{0\} \mid P\}</math>. Such a <math>B</math> had already been considered in the early section on the axiom of separation. Again, the latter <math>f</math> here is a classical choice function either way also, where <math>P</math> functions as a (potentially undecidable) "if-clause". Constructively, the domain and values of such <math>P</math>-dependent would-be functions are not understood enough to prove them to be a total functional relation into <math>\{0, 1\}</math>.

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 "if-clauses" 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 choice grants existence a function associated with every set-sized collection of inhabited elements <math>s</math>, with which one can then at once pick unique elements <math>t</math>.
The [[axiom of regularity]] states that for every inhabited set <math>s</math> in the universal collection, there ''exists'' an element <math>t</math> in <math>s</math>, which shares no elements with <math>s</math>. This formulation does not involve functions or unique existence claims, but instead directly guarantees sets <math>t\in s</math> with a specific property.
As the axiom correlates membership claims at different rank, the axiom also ends up implying <math>{\mathrm {PEM}}</math>:

The proof from Choice above had used <math>1:=\{0\}</math> and a particular set <math>\{a, b\}</math>. The proof in this paragraph also assumes Separation applies to <math>P</math> and uses <math>b</math>, for which <math>\{0\}\in b</math> by definition. 
It was already explained that <math>P\leftrightarrow 0\in b</math> and so one may prove excluded middle for <math>P</math> in the form <math>0\in b\lor 0\notin b</math>. Now let <math>t\in b</math> be the postulated member with the empty intersection property. The set <math>b</math> was defined as a subset of <math>\{0, 1\}</math> and so any given <math>t\in b</math> fulfills the disjunction <math>t=0\lor t=1</math>. The left clause <math>t=0</math> implies <math>0\in b</math>, while for the right clause <math>t=1</math> one may use that the special non-intersecting element <math>t</math> fulfills <math>(t=\{0\})\leftrightarrow (0\notin b)</math>.

Demanding that the set of naturals is [[well-ordered]] with respect to it standard order relation imposes the same condition on the inhabited set <math>b\subset\omega</math>. So the [[least number principle]] has the same non-constructive implication.
As with the proof from Choice, the scope of propositions for which these results hold is governed by one's Separation axiom.

=== Arithmetic ===
The four [[Peano axioms]] for <math>0</math> and <math>S</math>, characterizing the set <math>\omega</math> as a model of the natural numbers in the constructive set theory <math>{\mathsf {ECST}}</math>, have been discussed. The order "<math><</math>" of natural numbers is captured by membership "<math>\in</math>" in this von Neumann model and this set is discrete, i.e. also <math>\phi(n, m) := (n = m)</math> is decidable.

As discussed, induction for arithmetic formulas is a theorem. However, when not assuming full mathematical induction (or stronger axioms like full Separation) in a set theory, there is a pitfall regarding the existence of arithmetic operations. The first-order theory of [[Heyting arithmetic]] <math>{\mathsf{HA}}</math> has the same [[Signature (logic)|signature]] and non-logical axioms as Peano arithmetic <math>{\mathsf{PA}}</math>. In contrast, the signature of set theory does not contain addition "<math>+</math>" or multiplication "<math>\times</math>". <math>{\mathsf {ECST}}</math> does actually not enable [[primitive recursive function|primitive recursion]] in <math>\omega</math> for function definitions of what would be <math>h\colon(x\times\omega)\to y</math> (where "<math>\times</math>" 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 there to be a set capturing the addition function <math>+\colon(\omega\times\omega)\to \omega</math>. 
In the next section, it is clarified which set theoretical 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
:<math>{\mathsf{HA}}\vdash\forall n. \forall m.\big(\phi(n, m)\lor\neg\phi(n, m)\big)</math>
for any quantifier-free formula. Indeed, <math>{\mathsf{PA}}</math> is <math>\Pi_2^0</math>-conservative over <math>{\mathsf{HA}}</math> and double-negation elimination is possible for any [[Harrop formula]].

==== Arithmetic functions from recursion ====
Going a step beyond <math>{\mathsf {ECST}}</math>, the [[Recursive definition|axiom granting definition]] of set functions via iteration-step set functions must be added: For any set <math>y</math>, set <math>z\in y</math> and <math>f\colon y\to y</math>, there must also exist a function <math>g\colon \omega\to y</math> attained by making use of the former, namely such that <math>g(0)=z</math> and <math>g(Sn)=f(g(n))</math>. This iteration- or [[Recursion#The recursion theorem|recursion principle]] is akin to the [[Transfinite induction#Transfinite recursion|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 <math>{\mathsf {HA}}</math> in our set theory, including addition and multiplication functions.

With this, <math>{\mathbb N}</math> and <math>{\mathbb Z}</math> are well-founded, in the sense of the [[Well-founded relation#Induction and recursion|inductive subsets formulation]]. Further, arithmetic of rational numbers <math>{\mathbb Q}</math> can then also be defined and its properties, like uniqueness and countability, be proven.

==== Recursion from set theory axioms ====
Recall that <math>h\simeq y^x</math> is short for <math>\forall f. \big(f\in h\leftrightarrow f\in y^x\big)</math>, where <math>f\in y^x</math> 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 <math>h=y^x</math>. (Although by slight abuse of formal notation, as with the symbol "<math>\in</math>", the symbol "<math>=</math>" is also commonly used with classes anyhow.)

A set theory with the <math>{\mathsf {HA}}</math>-model enabling recursion principle, spelled out above, will also prove that, for all naturals <math>n</math> and <math>m</math>, the function spaces
:<math>{\{0,1,\dots,n-1\}}\to{\{0,1,\dots,m-1\}}</math>
are sets. Indeed, bounded recursion suffices, i.e. the principle for <math>\Delta_0</math>-defined classes.

Conversely, the recursion principle can be proven from a definition involving the union of recursive functions on finite domains. Relevant for this is the class of partial functions on <math>\omega</math> such that all of its members have a return values only up to some natural number bound, which may be expressed by <math>\cup_{n\in\omega}y^{\{0,1,\dots,n-1\}}</math>. Existence of this as a set becomes provable assuming that the individual function spaces <math>y^n</math> all form sets themselves. To this end
{| border=1 style="border:0px"
| style="border:1px solid #000000; padding:1.0em; background-color:#F8F9FA" |
Exponentiation for finite domains
; <math>\forall(n\in\omega). \forall y.\ \ \exists h. h\simeq y^n</math>
|}
With this axiom, any such space is now a ''set'' of subsets of <math>n\times y</math> and this is strictly weaker than full Separation. Notably, adoption of this principle has genuine set theoretical flavor, in contrast to a direct embedding of arithmetic principles into our theory. And it is a modest principle insofar as these function spaces are tame: When instead assuming full induction or full exponentiation, taking <math>y</math> to function spaces <math>y^n</math>, or to n-fold Cartesian products, provably does preserve countability.

In <math>{\mathsf{ECTS}}</math> plus finite exponentiation, the recursion principle is a theorem. Moreover, enumerable forms of the [[pigeon hole principle]] can now also be proven, e.g. that on a finitely indexed set, every auto-injection is also a surjection. As a consequence, the [[cardinal number|cardinality]] of finite sets, i.e. the finite von Neumann ordinal, is provably unique. The finitely indexed discrete sets are just the finite sets. In particular, finitely indexed subsets of <math>\omega</math> are finite. Taking quotients or taking the binary union or Cartesian product of two sets preserve finiteness, sub-finiteness and being finitely indexed.

The set theory axioms listed so far incorporates first-order arithemtic and suffices as formalized framework for a good portion of common mathematics. The restriction to finite domains is lifted in the strictly stronger exponentiation axiom below. However, also that axiom does not entail the full induction schema for formulas with unbound quantifiers over the domain of sets, nor a dependent choice principle. Likewise, there are Collection principles that are constructively not implied by Replacement, as discussed further below. A consequence of this is that for some statements of higher complexity or indirection, even if concrete instances of interest may well be provable, the theory may not prove the universal closure.
Stronger than this theory with finite exponentiation is <math>{\mathsf{ECTS}}</math> plus full induction. It implies the recursion principle even for classes and such that <math>g</math> is unique. Already that recursion principle when restricted to <math>\Delta_0</math> does prove finite exponentiation, and also the existence of a transitive closure for every set with respect to <math>\in</math> (since union formation is <math>\Delta_0</math>). With it more common constructions preserve countability. 
General unions over a finitely indexed set of finitely indexed sets are again finitely indexed, when at least assuming induction for <math>\Sigma_1</math>-predicates (with respect to the set theory language, and this then holds regardless of the decidability of their equality relations.)

==== Induction without infinite sets ====
Before discussing even classically uncountable sets, this last section takes a step back to a context more akin to <math>{\mathsf {BCST}}</math>. 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]] <math>{\mathsf{HA}}</math> is [[Interpretation (model theory)#Bi-interpretability|bi-interpretable]] 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 arithmetic|bounded formulations]] or [[Induction, bounding and least number principles|variations on induction schemas]] that may furthermore only allow for predicates of restricted complexity. On the classical first-order side, this leads to theories between the [[Robinson arithmetic]] <math>{\mathsf {Q}}</math> and [[Peano arithmetic]] <math>{\mathsf {PA}}</math>: The theory <math>{\mathsf {Q}}</math> does not have any induction. <math>{\mathsf {PA}}</math> has full mathematical induction for arithmetical formulas and has [[Epsilon numbers (mathematics)|ordinal <math>\varepsilon_0</math>]], 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 [[Grzegorczyk hierarchy|fast growing functions]]. Some of the most basic examples of arithmetics include [[elementary function arithmetic]] <math>{\mathsf {EFA}}</math>, which includes induction for just bounded arithmetical formulas, here meaning with quantifiers over finite number ranges. The theory has a [[ordinal analysis|proof theoretic]] ordinal (the least not provenly recursive [[well-ordering]]) of <math>\omega^3</math>.
The <math>\Sigma_1^0</math>-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 <math>\Pi_1^0</math>-induction schema.
The relatively weak classical first-order arithmetic which adopts that schema is denoted <math>\mathsf{I\Sigma}_1</math> and proves the primitive recursive functions total. The theory <math>\mathsf{I\Sigma}_1</math> is <math>\Pi_2^0</math>-conservative over [[primitive recursive arithmetic]] <math>{\mathsf {PRA}}</math>.
Note that the <math>\Sigma_1^0</math>-induction is also part of the [[Second-order logic|second-order]] reverse mathematics [[Reverse mathematics#The base system RCA0|base system <math>\mathsf{RCA}_0</math>]], its other axioms being <math>{\mathsf {Q}}</math> plus <math>\Delta_1^0</math>-comprehension of subsets of naturals. The theory <math>\mathsf{RCA}_0</math> is <math>\Pi_1^1</math>-conservative over <math>\mathsf{I\Sigma}_1</math>. Those last mentioned arithmetic theories all have ordinal <math>\omega^\omega</math>.

Let us mention one more step beyond the <math>\Sigma_1^0</math>-induction schema. Lack of stronger induction schemas means, for example, that some unbounded versions of the [[pigeon hole principle]] are unprovable. One relatively weak one being the [[Ramsey theorem]] type claim here expressed as follows: ''For any <math>m>0</math> and coding of a coloring map <math>f</math>, associating each <math>n\in\omega</math> with a color <math>\{0, 1, \dots, m-1\}</math>, it is not the case that for every color <math>c < m</math> there exists a threshold input number <math>n_c</math> beyond which <math>c</math> 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 <math>k</math> such that, in effect, for some unbounded domain <math>K\subset\omega</math> it holds that <math>\forall (n\in K). f(n) = k</math>. In words, when <math>f</math> provides infinite enumerated assignments, each being of one of <math>m</math> different possible colors, it is claimed that a particular <math>k</math> coloring infinitely many numbers always exists and that the set can thus be specified, without even having to inspect properties of <math>f</math>. When read constructively, one would want <math>k</math> 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 <math>n_c</math>'s, beyond which the function would still have to attain some color value. More specifically, the strength of the required [[Induction, bounding and least number principles#Definitions|bounding principle]] is [[Induction, bounding and least number principles#Relations between the principles|strictly between]] the induction schema in <math>\mathsf{I\Sigma}_1^0</math> and <math>\mathsf{I\Sigma}_2^0</math>.
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 for larger domains, but always finite. Acceptance of an induction schema as in <math>\mathsf{I\Sigma}_2^0</math> 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 [[Edward Nelson#Foundations of mathematics|predicative arithmetic]], even the mathematical induction schema has been criticized as possibly being [[Impredicativity|impredicative]], when natural numbers are defined as the object which fulfill this schema, which itself is defined in terms of all naturals.

=== Exponentiation ===
Classical <math>{\mathsf {ZFC}}</math> without the [[Powerset axiom]] has natural models in classes of sets of [[Hereditary property#In set theory|hereditary]] size less than certain uncountable cardinals.<ref>{{citation|first=Victoria|last=Gitman|arxiv=1110.2430|title=What is the theory ZFC without power set|year=2011}}</ref> In particular, it is still consistent with all existing sets (including sets holding reals) being [[subcountable]], and there even countable. Such a theory essentially amounts to [[second-order arithmetic]]. All sets being subcountable can constructively be consistent even in the present of uncountable sets, as introduced now.

Possible choice principles were discussed, a weakened form of the Separation schema was already adopted, and more of the standard <math>{\mathsf {ZFC}}</math> 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. The following axiom <math>{\mathrm {Exp}}</math> is strictly stronger than its pendant for finite domains discussed above:
{| border=1 style="border:0px"
| style="border:1px solid #000000; padding:1.0em; background-color:#F8F9FA" |
Exponentiation
; <math>\forall x. \forall y.\ \ \exists h. h\simeq y^x</math>
|}
The formulation here again uses the convenient notation for function spaces, as discussed above. In words, the axiom says that given two sets <math>x, y</math>, the class <math>y^x</math> of all functions is, in fact, also a set.
This is certainly required, for example, to formalize the object map of an internal [[hom-functor]] like <math>{\mathrm{hom}}({\mathbb N},-).</math>

Adopting such an existence statement also the quantification <math>\forall f</math> over the elements of certain classes of (total) functions now only range over sets. Consider the collection of pairs <math>\langle a, b\rangle\in x\times x</math> validating the apartness relation <math>\exists (f\in {\mathbb N}^x). f(a)\neq f(b)</math>. Via bounded Separation, this now constitutes a subset of <math>x\times x</math>. This examples shows that the Exponentiation axiom not only enriches the domain of sets directly, but via separation also enables the derivation of yet more sets, and this then furthermore also strengthens other axioms.

Notably, these bounded quantifiers now range over function spaces that are provably [[uncountable]], and hence even classically uncountable. E.g. the collection of all functions <math>f\colon\omega\to 2</math> where <math>2:=SS0=\{0, 1\}</math>, i.e. the set <math>2^{\mathbb N}</math> of points underlying the [[Cantor space]], is uncountable, by [[Cantor's diagonal argument#Ordering of cardinals|Cantor's diagonal argument]], and can at best be taken to be a subcountable set. In this theory one may now also quantify over subspaces of spaces like <math>2^{\mathbb N}</math>, which is a third order notion on the naturals. (In this section and beyond, the symbol for the semiring of natural numbers in expressions like <math>y^{\mathbb N}</math> is used, or written <math>\omega\to y</math>, just to avoid conflation of cardinal- with ordinal exponentiation.)
Roughly, classically uncountable sets, like for example these function spaces, tend to not have computably decidable equality.

By taking the general union over an <math>x</math>-indexed family <math>\{y_i\}_i</math>, also the dependent or indexed product, written <math>\Pi_{i\in x}\,y_i</math>, is now a set. For constant <math>y_i</math>, this again reduces to the function space
<math>y^x</math>.
And taking the general union over function spaces themselves, whenever the powerclass of <math>x</math> is a set, then also the superset <math>\cup_{s\subset x}y^s</math> of <math>y^x</math> is now a set - giving a means to talk about the space of partial functions on <math>x</math>.

==== Unions and countability ====
With Exponentiation, the theory proves the existence of any [[primitive recursive function]] in <math>x\times\omega\to y</math>, and in particular in the uncountable function spaces out of <math>\omega</math>. Indeed, with function spaces and the finite von Neumann ordinals as domains, we can model <math>{\mathsf{HA}}</math> as discussed, and thus encode ordinals in the arithmetic. One then furthermore obtains the [[Ordinal arithmetic#Exponentiation|ordinal]]-exponentiated number <math>\omega^\omega</math> as a set, which may be characterized as <math>\cup_{n\in\omega}\omega^n</math>, the counted set of words over an infinite [[Alphabet (formal languages)|alphabet]]. The union of all finite sequences over a countable set is now a countable set. Further, 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 <math>{\mathsf{ZF}}</math> is consistent with the uncountable set <math>{\mathbb{R}}</math> being the union of a countable set of countable sets.

The list here is by no means complete. Many theorems about the various function existence predicates hold, especially when assuming countable choice - which as noted is never implicitly assumed in this discussion.

At last, with Exponentiation, any finitely indexed union of a family of subfinitely indexed resp. subcountable sets is itself subfinitely indexed resp. subcountable as well.
The theory also proves the collection of all the ''countable'' subsets of any set <math>x</math> to be a set itself. Concerning this subset of the powerclass <math>{\mathcal P}_x</math>, some natural cardinality questions can also classically only be settled with Choice, at least for uncountable <math>x</math>.

==== The class of all subsets of a set ====
Given a sequence of sets, one may define new such sequences, e.g. in <math>\langle a,b\rangle \mapsto \langle \langle \rangle ,\langle a\rangle ,\langle b\rangle ,\langle a,b\rangle \rangle </math>. But notably, in a mathematical set theory framework, the collection of all subsets of a set is defined not in a bottom-up construction from its constituents but via a comprehension over ''all'' sets in the domain of discourse. The standard, standalone characterization of the powerclass of a set <math>x</math> involves unbounded universal quantification, namely <math>\forall u. \left(u\in {\mathcal P}_x\leftrightarrow u\subset x\right)</math>, where <math>\subset</math> was previously defined also in terms of the membership predicate <math>\in</math>. Here, a statement expressed as <math>\forall (u\in {\mathcal P}_x). Q(x)</math> must a priori be taken for <math>\forall u. \big(u\subset x\to Q(x)\big)</math> and is not equivalent to a set-bounded proposition. Indeed, the statement <math>y={\mathcal P}_x</math> itself [[Lévy hierarchy|is <math>\Pi_1</math>]]. If <math>{\mathcal P}_x</math> is a set, then the defining quantification even ranges across <math>{\mathcal P}_x</math>, which makes the [[axiom of powerset]] [[impredicative]].

Recall that a member of the set of characteristic functions <math>2^x</math> corresponds to a predicate that is decidable on a set <math>x</math>, which it thus determines a detachable subset <math>s\subset x</math>. In turn, the class <math>{\mathcal D}_x \subset {\mathcal P}_x</math> of all detachable subsets of <math>x</math> is now also a set, via Replacement. However, <math>{\mathcal D}_x</math> may fail to provably have desirable properties, e.g. being closed under unending operations such as the unions over countably infinite index sets: For a countable sequence <math>u_n\in {\mathcal D}_x</math>, the subset <math>U:=\cup_{k\in\omega}u_k</math> of <math>x</math> validating <math>(a\in U)\leftrightarrow \exist(m\in\omega). a\in u_m</math> for all <math>a\in x</math> does exist as a set. But it may fail to be detachable and is therefore then not necessarily provably itself a member of <math>{\mathcal D}_x</math>. Meanwhile, over classical logic, all subsets of a set <math>x</math> are trivially detachable, meaning <math>{\mathcal D}_x = {\mathcal P}_x</math> and then <math>{\mathcal D}_x</math> of course holds any subset. Over classical logic, this furthermore means that Exponentiation turns the power class into a set.

Translating results of set theory based mathematical theories like point-set topology or measure theory to a constructive framework is a subtle back and forth. For example, while <math>{\mathcal D}_x</math> is a [[field of sets]], for it to form a [[σ-algebra]] per definition also requires the above mentioned closedness under unions. But while a domain of subsets may fail to exhibit such closure property constructively, classically a measure <math>\mu</math> is [[Measure (mathematics)#Continuity from below|continuous from below]] and so its value on an infinite union can in any case also be expressed without reference to that set as function input, namely as <math>\lim_{n\to\infty}</math> of the growing sequence <math>\mu(\cup_{k\le n}u_k)</math> of the function's values at finite unions.

Apart from the class of detachable sets, also various other subclasses of any powerclass are now provenly sets. For example, the theory also proves this for the collection of all the countable subsets of any set. 

The richness of the full powerclass in a theory without excluded middle can best be understood by considering small classically finite sets. For any proposition <math>P</math>, consider the subclass <math>B:=\{x\in 1\mid P\}</math> of <math>1</math> (i.e. <math>\{0\}</math> or <math>S0</math>). It equals <math>B=0</math> when <math>P</math> can be rejected and it equals <math>B=1</math> (i.e. <math>B=S0</math>), when <math>P</math> can be proven. But <math>P</math> may also not be decidable at all. Consider three different undecidable proposition, none of which provenly imply another. They can be used to define three subclasses of the singleton <math>1</math>, none of which are provenly the same. In this view, the powerclass <math>{\mathcal P}_1</math> of the singleton, usually denoted by <math>\Omega</math>, is called the [[truth value]] [[Heyting algebra#Heyting algebras as applied to intuitionistic logic|algebra]] and does not necessarily provenly have only two elements.

With Exponentiation, the powerclass of the singleton, <math>{\mathcal P}_1</math>, being a set already implies Powerset for sets in general. The proof is via replacement for the association of <math>f\in{{\mathcal P}_1}^x</math> to <math>\{z\in x\mid 0\in f(z)\}\in{\mathcal P}_x</math>, and an argument why all subsets are covered. The set <math>2^x</math> injects into the function space <math>{{\mathcal P}_1}^x</math> also.

If the theory proves <math>B</math> above a set (as for example <math>{\mathsf{IZF}}</math> unconditionally does), then the subset <math> b := \{\langle 0, B\rangle\}</math> of <math>1\times {\mathcal P}_1</math> is a function <math>b \colon 1\to {\mathcal P}_1</math> with <math>\big(b(0)=1\big)\leftrightarrow P</math>. To claim that <math>{\mathcal P}_1=2</math> is to claim that excluded middle holds for <math>P</math>.

It has been pointed out that the empty set <math>0</math> and the set <math>1</math> itself are of course two subsets of <math>1</math>, meaning <math>2\subset{\mathcal P}_1</math>. Whether also <math>{\mathcal P}_1\subset 2</math> is true in a theory is contingent on a simple disjunction:
:<math>\big(\forall (x\in {\mathcal P}_1). (0\in x\lor 0\notin x)\big)\to\,{\mathcal P}_1\subset 2</math>.
So assuming <math>{\mathrm {PEM}}</math> for just bounded formulas, predicative Separation then lets one demonstrate that the powerclass <math>{\mathcal P}_1</math> is a set. And so in this context, also full Choice proves Powerset. (In the context of <math>{\mathsf {IZF}}</math>, bounded excluded middle in fact already turns set theory classical, as discussed further below.)

Full Separation is equivalent to just assuming that each individual subclass of <math>1</math> is a set. Assuming full Separation, both full Choice and Regularity prove <math>{\mathrm {PEM}}</math>.

Assuming <math>{\mathrm {PEM}}</math> in this theory, Set induction becomes equivalent to Regularity and Replacement becomes capable of proving full Separation.

Note that cardinal relations involving uncountable sets are also elusive in <math>{\mathsf {ZFC}}</math>, where the characterization of uncountability simplifies to <math> |\omega| < |x| </math>. For example, regarding the uncountable power <math> 2^{|\omega|}</math>, it is independent of that classical theory whether all such <math>x</math> have <math> 2^{|\omega|} \le |x| </math>, nor does it prove that <math> 2^{|\omega|} < 2^{|x|} </math>. See [[continuum hypothesis]] and the related [[Easton's theorem]].

==== Category and type theoretic notions ====
So in this context with Exponentiation, first-order arithmetic has a model and all function spaces between sets exist. The latter are more accessible than the classes containing all subsets of a set, as is the case with [[exponential object]]s resp. [[subobject]]s in category theory.
In [[category theory|category theoretical]] terms, the theory <math>{\mathsf {BCST}}+{\mathrm {Exp}}</math> essentially corresponds to constructively [[Well-pointed category|well-pointed]] [[Cartesian closed]] [[Heyting algebra|Heyting]] pre[[topos]]es with (whenever Infinity is adopted) a [[natural numbers object]]. Existence of powerset is what would turn a Heyting pretopos into an [[elementary topos]].<ref>{{citation|first=Michael|last=Shulman|arxiv=1808.05204|title=Comparing material and structural set theories|journal=Annals of Pure and Applied Logic|year=2019|volume=170 |issue=4 |page=465-504 |doi=10.1016/j.apal.2018.11.002 }}</ref>
Every such topos that interprets <math>{\mathsf {ZF}}</math> 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 <math>{\mathrm {PEM}}</math> 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 [[monomorphism]]s has a section. The latter is a [[Axiom of choice#Equivalents|formulation of choice]]. [[Geometric logic|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 "<math>x\to y</math>" 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 <math>(z\times x)\to y</math> and <math>z\to y^x</math>, an [[adjoint functor|adjunction]].
A typical type theory with general programming capability - and certainly those that can model <math>{\mathsf {CZF}}</math>, which is considered a constructive set theory - will have a type of integers and function spaces representing <math>{\mathbb Z}\to{\mathbb Z}</math>, and as such also include types that are not countable. This is just to say, or implies, that among the function terms <math>f\colon {\mathbb Z}\to({\mathbb Z}\to{\mathbb Z})</math>, none have the property of being a surjection.

Constructive set theories are also studied in the context of [[Combinatory logic|applicative axioms]].

====Metalogic====
While the theory <math> {\mathsf {ECST}} + {\mathrm {Exp}} </math> does not exceed the consistency strength of Heyting arithmetic, adding Excluded Middle gives a theory proving the same theorems as classical <math>{\mathsf {ZF}}</math> minus Regularity!
Thus, adding Regularity as well as either <math> { \mathrm {PEM} } </math> or full Separation to <math> {\mathsf {ECST} } + {\mathrm {Exp} } </math> gives full classical <math> { \mathsf {ZF} } </math>.
Adding full Choice and full Separation gives <math> { \mathsf {ZFC} } </math> minus Regularity.
So this would thus lead to a theory beyond the strength of typical [[type theory]].

The presented theory does not prove a function space like <math>{\mathbb N}^{\mathbb N}</math> to be not enumerable, in the sense of injections out of it. Without further axioms, intuitionistic mathematics has models in recursive functions but also forms of [[hypercomputation]].

=== Analysis ===
In this section the strength of <math>{\mathsf {ECST}}+{\mathrm {Exp}}</math> 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]],<ref>Errett Bishop, ''Foundations of Constructive Analysis'', July 1967</ref> [[Dyadic rational#Other related constructions|feasible analysis]] and [[computable analysis]].

The theory so far proves [[Categoricity|uniqueness]] of [[Archimedean property|Archimedean]], [[Dedekind complete]] ([[Pseudo-order|pseudo]]-)[[ordered field]]s, 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.

==== Topology ====
Regardless of the choice of model, the characteristic flavor of a constructive theory of numbers can be explicated using an independent proposition <math>P</math>. Consider a counter-example to the constructive provability of the well-orderedness of the naturals, but now embedded in the reals. Say
:<math>M:= \{x \in {\mathbb R} \mid (x=0 \land P) \lor (x=1) \}</math>.
The infimum metric distance between some point and such a subset, what may be expressed as <math>\rho(0, M)</math> for example, may constructively fail to provably exist. More generally, this locatedness property of subsets governs the well-developed constructive metric space theory.

Whether Cauchy or Dedekind reals, among others, also fewer statements about the arithmetic of the reals are [[Decidability (logic)|decidable]], compared to the classical theory.

==== Cauchy sequences ====
Exponentiation implies recursion principles and so in <math>{\mathsf {ECST}}+{\mathrm {Exp}}</math>, one can comfortably reason about sequences <math>s\colon\omega\to{\mathbb Q}</math>, their regularity properties such as <math>|s_n-s_m|\le \tfrac{1}{n}+\tfrac{1}{m}</math>, or about shrinking intervals in <math>\omega\to({\mathbb Q}\times{\mathbb Q})</math>. So this enables speaking of [[Cauchy sequences]] and their arithmetic. This is also the approach to analysis taken in <math>{\mathsf {Z}}_2</math>.

==== Cauchy reals ====
Any Cauchy real number is a collection of such sequences, i.e. a subset of a set of functions on <math>\omega</math> constructed with respect to an [[equivalence relation]]. Exponentiation together with bounded separation prove the collection of Cauchy reals to be a set, thus somewhat simplifying the logically treatment of the reals.

Even in the strong theory <math>{\mathsf {IZF}}</math> with a strengthened form of Collection, the Cauchy reals are poorly behaved when not assuming a form of [[countable choice]], and <math>{\mathrm{AC}_{\omega,2}}</math> suffices for most results. This concerns [[Completeness of the real numbers|completeness]] of equivalence classes of such sequences, equivalence of the whole set to the Dedekind reals, existence of a [[modulus of convergence]] for all Cauchy sequences and the preservation of such a modulus when taking limits.<ref>Robert S. Lubarsky, [https://arxiv.org/pdf/1510.00639.pdf ''On the Cauchy Completeness of the Constructive Cauchy Reals''], July 2015</ref> 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 cut#Definition|Dedekind cuts]] are characterized using subsets of algebraic structures such as <math>{\mathbb Q}</math>: 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 <math>\sqrt 2</math> given by
:<math>\big\langle\{x\in{\mathbb Q}\mid x<0 \lor x^2<2\},\,\{x\in{\mathbb Q}\mid 0<x \land 2 < x^2\}\big\rangle\,\ \in\,\ {{\mathcal P}_{\mathbb Q}}\times {{\mathcal P}_{\mathbb Q}}</math>
(Depending on the convention for cuts, either of the two parts or neither, like here, may makes use of the sign <math>\le</math>.)

The theory given by the axioms so far validates that a [[pseudo-order]]ed 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 <math>\{0,1\}^{\mathbb Q}</math> does not grant <math>{{\mathcal P}_{\mathbb Q}}</math> to be a set, and so neither is the class of all subsets of <math>{\mathbb Q}</math> 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 <math>{\mathrm {PEM}}</math> or Powerset, [[countable choice]] into finite sets is assumed to prove the uncountability of the set of all Dedekind reals.

==== Constructive schools ====
Most schools for constructive analysis validate some choice and also <math>\mathrm{BD}</math>-<math>{\mathbb N}</math>, 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. <math>{\mathsf {RUSS}}</math>), first one has [[Markov's principle]] <math>{\mathrm {MP}}</math>, 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 anti-classical [[Church's thesis (constructive mathematics)|constructive Church's thesis principle]] <math>{\mathrm {CT}}</math>, generally adopted for number-theoretic 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 <math>\Pi_2^0</math> in the [[arithmetical hierarchy]], meaning membership of any index is affirmed by validating a <math>\forall x\, \exists y</math> 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 <math>{\mathrm {CT}}</math> postulate makes <math>\omega\to\omega</math> into a "sparse" set, as viewed from classical set theory. [[Subcountability]] of sets can also be postulated independently. 
* So on another end, on the [[L. E. J. Brouwer|Brouwerian]] [[Mathematical intuitionism|intuitionist]] side (<math>{\mathsf {INT}}</math>), there are [[bar induction]], the decidable [[Kőnig's lemma#Relationship to constructive mathematics and compactness|fan theorem]] <math>{\mathrm {FAN}}_\Delta</math> saying decidable bars are uniform, which are amongst the weakest often discussed principles, Kripke's schema (with countable choice turning all subclasses of <math>\omega</math> countable), or even Brouwer's anti-classical continuity principle, determining return values of what is established a function on [[Choice sequence|unending sequences]] already through just finite initial segments.

Certain laws in both of those schools contradict <math>{\mathrm {WLPO}}</math>, so that choosing to adopt all principles from either school disproves theorems from classical analysis. <math>{\mathrm {CT}}_0</math> is still consistent with some choice, but contradicts the classical <math>{\mathrm {WKL}}</math> and <math>{\mathrm {LLPO}}</math>, explained below. The [[independence of premise|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, <math>{\mathrm {CT}}_0</math> also contradicts <math>{\mathrm {FAN}}_\Delta</math>, meaning the constructive schools also cannot be combined in full. Some of the principles cannot be combined constructively to the extent that together they imply forms of <math>{\mathrm {PEM}}</math> - for example <math>{\mathrm {MP}}</math> plus the countability of all subsets of the naturals. These combinations are then naturally also not consistent with further anti-classical principles.

====Indecomposability====
Denote the class of all sets by <math>{\mathcal V}</math>. Decidability of membership in a class <math>R</math> can be expressed as membership in <math>R\cup({\mathcal V}\setminus R)</math>. 
We also note that, by definition, the two extremal classes <math>{\mathcal V}</math> and <math>\{\}</math> are trivially decidable. Membership in those two is equivalent to the trivial propositions <math>x=x</math> resp. <math>\neg(x=x)</math>.

Call a class <math>R</math> [[Indecomposability (intuitionistic logic)|indecomposable]] or cohesive if, for any predicate <math>\chi</math>,
:<math>\big(\forall(x\in R). \chi(x)\lor\neg\chi(x)\big)\to \Big(\big(\forall(x\in R). \chi(x)\big)\lor\big(\forall(x\in R). \neg\chi(x)\big)\Big)</math>
This expresses that the only properties that are decidable on <math>R</math> are the trivial properties. This is well studied in intuitionistic analysis.

The so called indecomposability schema <math>{\mathrm {UZ}}</math> (Unzerlegbarkeit) for set theory is a possible principle which states that the whole class <math>{\mathcal V}</math> is indecomposable. Extensionally speaking, <math>{\mathrm {UZ}}</math> postulates that the two trivial classes are the only classes that are decidable with respect to the class of all sets. 
For a simple motivating predicate, consider membership <math>x\in 1</math> in the first non-trivial class, which is to say the property <math>x=\{\}</math> of being empty. This property is non-trivial to the extent that it separates some sets: The empty set is a member of <math>1</math>, by definition, while a plethora of sets are provenly not members of <math>1</math>. But, using Separation, one may of course also define various sets for which emptiness is not decidable in a constructive theory at all, i.e. membership in <math>1 \cup ({\mathcal V}\setminus 1)</math> is not provable for all sets. So here the property of emptiness does not partition the set theoretical domain of discourse into two decidable parts. For any such non-trivial property, the contrapositive of <math>{\mathrm {UZ}}</math> says that it cannot be decidable over all sets.

<math>{\mathrm {UZ}}</math> is implied by the uniformity principle <math>{\mathrm {UP}}</math>, which is consistent with <math>{\mathsf {CZF}}</math> and discussed below.

=== Non-constructive principles ===
Of course <math>{\mathrm {PEM}}</math> and many principles defining [[intermediate logic]]s are non-constructive. <math>{\mathrm {PEM}}</math> and <math>{\mathrm {WPEM}}</math>, which is <math>{\mathrm {PEM}}</math> for just negated propositions, can be presented as [[De Morgan's laws#In intuitionistic logic|De Morgan's rule]]s. 
More specifically, this section shall 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 <math>A</math> searchable if it is searchable for all its detachable subsets, which itself corresponds to <math>\{0,1\}^A</math>. This is a form of <math>\exists</math>-<math>{\mathrm {PEM}}</math> for <math>A</math>. Note that in the context of Exponentiation, such proposition on sets are now set-bound.

Particularly valuable in the study of [[constructive analysis]] are non-constructive claims commonly formulated in terms of the collection of all binary sequences and the characteristic functions <math>f</math> on the arithmetic domain <math>A=\omega</math> are well studied. Here <math>f({\underline{\mathrm n}})=0</math> is a decidable proposition at each numeral <math>{\mathrm n}</math>, but, as demonstrated previously, quantified statements in terms of <math>f</math> may not be. As is known from the [[Gödel's incompleteness theorems#Second incompleteness theorem|incompleteness theorem]] and its variations, already in first-order arithmetic, example functions on <math>{\mathbb N}</math> can be characterized such that if <math>{\mathsf {PA}}</math> is consistent, the competing <math>\exists</math>-<math>{\mathrm {PEM}}</math> disjuncts, of low complexity, are each <math>{\mathsf {PA}}</math>-unprovable (even if <math>{\mathsf {PA}}</math> proves the disjunction of the two axiomatically.)

More generally, the arithmetic <math>\exists</math>-<math>{\mathrm {PEM}}</math>, a most prominent non-constructive, essentially logical statement goes by the name [[limited principle of omniscience]] <math>{\mathrm {LPO}}</math>. In the constructive set theory <math>{\mathsf {CZF}}</math> introduced below, it implies <math>{\mathrm {BD}}</math>-<math>{\mathbb N}</math>, <math>{\mathrm {MP}}</math>, the <math>\Pi_1^0</math>-version of the fan theorem, but also <math>{\mathrm {WKL}}</math> discussed below. Recall examples of famous sentences that can be written down in a <math>\Pi_1^0</math>-fashion, i.e. of Goldbach-type: [[Goldbach conjecture]], [[Fermat's Last Theorem]] but also the [[Riemann hypothesis]] are among them. Assuming relativized dependent choice <math>{\mathrm {RDP}}</math> and the classical <math>{\mathrm {LPO}}</math> over <math>{\mathsf {CZF}}</math> does not enable proofs of more <math>\Pi_0^2</math>-statements.
<math>{\mathrm {LPO}}</math> postulates a disjunctive property, as does the weaker decidability statement for functions being constant (<math>\Pi_1^0</math>-sentences) <math>{\mathrm {WLPO}}</math>, the arithmetic <math>\forall</math>-<math>{\mathrm {PEM}}</math>. The two are related in a similar way as is <math>{\mathrm {PEM}}</math> versus <math>{\mathrm {WPEM}}</math> and they essentially differ by <math>{\mathrm {MP}}</math>.
<math>{\mathrm {WLPO}}</math> in turn implies the so-called "lesser" version <math>{\mathrm {LLPO}}</math>. This is the (arithmetic) <math>\exists</math>-version of the non-constructive De Morgan's rule for a negated conjunction. There are, for example, models of the strong set theory <math>{\mathsf {IZF}}</math> which separate such statements, in the sense that they may validate <math>{\mathrm {LLPO}}</math> but reject <math>{\mathrm {WLPO}}</math>.

Disjunctive principles about <math>\Pi_1^0</math>-sentences generally hint at equivalent formulations deciding [[apartness]] in analysis in a context with mild choice or <math>{\mathrm {MP}}</math>. 
The claim expressed by <math>{\mathrm {LPO}}</math> 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 <math>{\mathrm {LLPO}}</math> for real numbers is equivalent that the ordering <math>\le</math> 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 [[Halting problem#Halting on all inputs|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
:<math>T\,\subset\,\bigcup_{n\in\omega}\{0,1\}^{\{0,1,\dots,n-1\}}</math>,
with decidable membership, and those trees then provenly contain elements of arbitrary big finite size. The so called Weak [[Kőnig's lemma]] <math>{\mathrm {WKL}}</math> states: For such <math>T</math>, there always exists an infinite path in <math>\omega\to\{0,1\}</math>, i.e. an infinite sequence such that all its initial segments are part of the tree. In reverse mathematics, the second-order arithmetic subsystem <math>\mathsf{RCA}_0</math> does not prove <math>{\mathrm {WKL}}</math>. To understand this, note that there are computable trees <math>K</math> for which no ''computable'' such path through it exists. To prove this, one [[UTM theorem|enumerates the partial computable]] sequences and then diagonalizes all total computable sequences in one partial computable sequences <math>d</math>. One can then roll out a certain tree <math>K</math>, one exactly compatible with the still possible values of <math>d</math> everywhere, which by construction is incompatible with any total computable path.

In <math>{\mathsf {CZF}}</math>, the principle <math>{\mathrm {WKL}}</math> implies <math>{\mathrm {LLPO}}</math> and <math>\Pi_1^0</math>-<math>{\mathrm {AC}}_{\omega,2}</math>, a very modest form of countable choice introduced above. The former two are equivalent assuming that choice principle already in the more conservative arithmetic context. <math>{\mathrm {WKL}}</math> is also equivalent to the [[Brouwer fixed point theorem]] and other theorems regarding values of continuous functions on the reals. The fixed point theorem in turn implies the [[intermediate value theorem]], but always be aware that these claims may depend on the formulation, as the classical theorems about encoded reals can translate to different variants when expressed in a constructive context.<ref>Matthew Ralph John Hendtlass, [https://core.ac.uk/download/pdf/19417936.pdf ''Constructing fixed points and economic equilibria''], PhD Thesis, University of Leeds, April 2013</ref>

The <math>{\mathrm {WKL}}</math>, and some variants thereof, concerns ''infinite'' graphs and so its contrapositives gives a condition for finiteness. Again to connect to analysis, over the [[Reverse mathematics#The base system RCA0|classical arithmetic theory <math>\mathsf{RCA}_0</math>]], the claim of <math>{\mathrm {WKL}}</math> is for example equivalent to the [[Heine-Borel theorem|Borel compactness]] regarding finite subcovers of the real unit interval. <math>{\mathrm {FAN}}_\Delta</math> is a closely related existence claim involving finite sequences in an infinite context. Over <math>\mathsf{RCA}_0</math>, they are actually equivalent. In <math>{\mathsf {CZF}}</math> those are distinct, but, after again assuming some choice, here then <math>{\mathrm {WKL}}</math> implies <math>{\mathrm {FAN}}_\Delta</math>.

=== Induction ===
==== Mathematical induction ====
It was observed that in set language, induction principles can read <math>\mathrm{Ind}_A\to \omega\subset A</math>, with the antecedent <math>\mathrm{Ind}_A</math> defined as further above, and with <math>\omega\subset A</math> meaning <math>\forall (n\in\omega). n\in A</math> where the set <math>\omega</math> always denotes the standard model of natural numbers. Via the strong axiom of Infinity and predicative Separation, the validity of induction for set-bounded or <math>\Delta_0</math>-definitions was already established and thoroughly discussed. For those predicates involving only quantifiers over <math>\omega</math>, it validates induction in the sense of the first-order arithmetic theory. In a set theory context where <math>\omega</math> is a set, this induction principle can be used to prove predicatively defined subclasses of <math>\omega</math> to be the ''set'' <math>\omega</math> itself. The so called full mathematical induction schema now postulates set equality of <math>\omega</math> to ''all'' its inductive subclasses. As in the classical theory, it is also implied when passing to the impredicative full Separation schema. As stated in the section on Choice, induction principles such as this are also implied by various forms of choice principles.

The recursion principle for set functions mentioned in the section dedicated to arithmetic is also implied by the full mathematical induction schema over one's structure modeling the naturals (e.g. <math>\omega</math>). So for that theorem, granting a model of Heyting arithmetic, it represents an alternative to exponentiation principles.
{| border=1 style="border:0px"
| style="border:1px solid #000000; padding:1.0em; background-color:#F8F9FA" |
Axiom schema of full [[mathematical induction]]: For any predicate <math>\phi</math> on <math>\omega</math>,
; <math>\Big(\phi(0)\ \land\ \forall (k\in \omega). \big(\phi(k)\to \phi(Sk)\big)\Big)\to \forall (n\in \omega). \phi(n)</math>
|}
Predicate formulas used with the schema are to be understood as formulas in first-order set theory. The zero <math>0</math> denotes the set <math>\{\}</math> as above, and the set <math>Sn</math> denotes the successor set of <math>n\in\omega</math>, with <math>n\in Sn</math>. By Axiom of Infinity above, it is again a member of <math>\omega</math>. Beware that unlike in an arithmetic theory, the naturals here are not the abstract elements in the domain of discourse, but elements of a model. As has been observed in previous discussions, when accepting <math>{\mathsf{ECST}}</math>, not even for all predicatively defined sets is the equality to such a finite von Neumann ordinal necessarily decidable.

==== Set Induction ====
Going beyond the previous induction principles, one has full set induction, which is to be compared to [[Well-founded relation#Induction and recursion|well-founded induction]]. Like mathematical induction above, the following axiom is formulated as a schema in terms of predicates, and thus has a different character than induction principles proven from predicative set theory axioms. A variant of the axiom just for [[Bounded quantifier#Bounded quantifiers in set theory|bounded formulas]] is also studied independently and may be derived from other axioms.
{| border=1 style="border:0px"
| style="border:1px solid #000000; padding:1.0em; background-color:#F8F9FA" |
[[Epsilon-induction|Axiom schema of Set induction]]: For any predicate <math>\phi</math>,
; <math>\Big(\forall x.\, \big(\forall(y \in x).\ \phi(y)\big) \to \phi(x)\Big) \to \forall z. \phi(z)</math>
|}
Here <math>\forall(z\in \{\}). \phi(z)</math> holds trivially and so this covers to the "bottom case" <math>\phi(\{\})</math> in the standard framework. This (as well as natural number induction) may again be restricted to just the bounded set formulas, in which case arithmetic is not impacted.

In <math>{\mathsf{ECST}}</math>, the axiom proves induction in [[transitive set]]s and so in particular also for transitive sets of transitive sets. The latter then is an adequate definition of the ordinals, and even a <math>\Delta_0</math>-formulation. Set induction in turn enables ordinal arithmetic in this sense. It further allows definitions of class functions by [[Transfinite induction#Transfinite recursion|transfinite recursion]]. The study of the various principles that grant set definitions by induction, i.e. inductive definitions, is a main topic in the context of constructive set theory and their comparatively weak [[ordinal analysis|strengths]]. This also holds for their [[Inductive type|counterparts]] in type theory. Replacement is not required to prove induction over the set of naturals from set induction, but that axiom is necessary for their arithmetic modeled within the set theory.

The [[axiom of regularity]] is a single statement with universal quantifier over sets and not a schema. As show, it implies <math>{\mathrm {PEM}}</math>, and so is non-constructive. Now for <math>\phi</math> taken to be the negation of some predicate <math>\neg S</math> and writing <math>\Sigma</math> for the class <math>\{y\mid S(y)\}</math>, induction reads
:<math>\forall(x\in\Sigma).\neg(x\cap \Sigma=\{\})\,\,\leftrightarrow\,\,\Sigma=\{\}</math>
Via the contrapositive, set induction implies all instances of regularity but only with double-negated existence in the conclusion. In the other direction, given enough [[transitive set]]s, regularity implies each instance of set induction.

====Metalogic====
The theory formulated above can be expressed as <math>{\mathsf {CZF}}</math> with its collection axioms discarded in favour of the weaker Replacement and Exponentiation axioms. It proves the Cauchy reals to be a set, but not the class of Dedekind reals.

Call an ordinal itself trichotomous if the irreflexive membership relation "<math>\in</math>" among its members is [[Law of trichotomy|trichotomous]]. Like the axiom of regularity, set induction restricts the possible models of "<math>\in</math>" and thus that of a set theory, as was the motivation for the principle in the 20's. But the constructive theory here does not prove a trichotomy for all ordinals, while the trichotomous ordinals are not well behaved with respect to the notion of successor and rank.

The added proof-theoretical strength attained with Induction in the constructive context is significant, even if dropping Regularity in the context of <math>{\mathsf {ZF}}</math> does not reduce the proof-theoretical strength.
Even without Exponentiation, the present theory with set induction has the same proof theoretic strength as <math>{\mathsf {CZF}}</math> and proves the same functions recursive. Specifically, its proof-theoretic [[Large countable ordinal#Impredicative ordinals|large countable ordinal]] is the [[Bachmann–Howard ordinal]]. This is also the ordinal of classical or intuitionistic [[Kripke–Platek set theory]].
It is consistent even with <math>{\mathsf {IZF}}</math> to assume that the class of  trichotomous ordinals form a set. The current theory augmented with this ordinal set existence postulate proves the consistency of <math>{\mathsf {CZF}}</math>.

Aczel was also one of the main developers or [[Non-well-founded set theory]], which rejects set induction.

====Relation to ZF====
The theory also constitutes a presentation of [[Zermelo–Fraenkel set theory#Axioms|Zermelo–Fraenkel set theory]] <math>{\mathsf {ZF}}</math> in the sense that variants of all its eight axioms are present. Extensionality, Pairing, Union and Replacement are indeed identical. Separation is adopted in a weak predicative form while Infinity is stated in a strong formulation. Akin to the classical formulation, this Separation axiom and the existence of any set already proves the Empty Set axiom. Exponentiation for finite domains and full mathematical induction are also implied by their stronger adopted variants. Without the principle of excluded middle, the theory here is lacking, in its classical form, full Separation, Powerset as well as Regularity. Accepting <math>{\mathrm {PEM}}</math> now exactly leads into the classical theory.

The following highlights the different readings of a formal theory. Let <math>\mathrm{CH}</math> denote the continuum hypothesis and <math>B:=\{z\in 1\mid \mathrm{CH}\}</math> so that <math>0\in B\leftrightarrow\mathrm{CH}</math>. Then <math>b:=B\cup\{1\}</math> is inhabited by <math>1</math> and any set that is established to be a member of <math>b</math> either equals <math>0</math> or <math>1</math>. Induction on <math>\omega</math> implies that it cannot consistently be negated that <math>b</math> has some least natural number member. The value of such a member can be shown to be independent of theories such as <math>{\mathsf {ZFC}}</math>. Nonetheless, any classical set theory like <math>{\mathsf {ZFC}}</math> also proves there ''exists'' such a number.

=== Strong Collection ===
Having discussed all the weakened forms of the classical set theory axioms, Replacement and Exponentiation can be further strengthened without losing a type theoretical interpretation, and in a way that is not going beyond <math>{\mathsf {ZF}}</math>.

So firstly, one may reflect upon the strength of the [[axiom of replacement]], also in the context of the classical set theory. For any set <math>y</math> and any natural <math>n</math>, there exists the product <math>y^n</math> recursively given by <math>y^{n-1}\times y</math>, which have ever deeper [[Von Neumann universe|rank]]. Induction for unbound predicates proves that these sets exist for all of the infinitely many naturals. Replacement "for <math>n\mapsto y^n</math>" now moreover states that this infinite class of products can be turned into the infinite set, <math>\{p\mid \exists(n\in\omega). p=y^n\}</math>. This is also not a subset of any previously established set.

Going beyond those axioms also seen in Myhill's typed approach, consider the discussed constructive theory with Exponentiation and Induction, but now strengthened by the [[Axiom of collection|collection schema]]. In <math>{\mathsf {ZF}}</math> it is equivalent to Replacement, unless the powerset axiom is dropped. In the current context the strong axiom presented supersedes Replacement, due to not requiring the [[binary relation]] definition to be functional, but possibly multi-valued.
{| border=1 style="border:0px"
| style="border:1px solid #000000; padding:1.0em; background-color:#F8F9FA" |
Axiom schema of Strong Collection: For any predicate <math>\phi</math>,
; <math>\forall a.\ \ \Big(\forall (x \in a). \exists y. \phi(x,y)\Big) \to \exists b. \Big(\forall (x \in a). \exists (y \in b). \phi(x,y)\ \land\ \forall (y \in b). \exists (x \in a). \phi(x,y)\Big)</math>
|}
In words, for every total relation, there exists an image set <math>b</math> such that the relation is total in both directions. Expressing this via a raw first-order formulation leads to a somewhat repetitive format. The antecedent states that one considers relation <math>\phi</math> between sets <math>x</math> and <math>y</math> that are total over a certain domain set <math>a</math>, that is, <math>\phi</math> has at least one "image value" <math>y</math> for every element <math>x</math> in the domain. This is more general than an inhabitance condition <math>x\in y</math> in a set theoretical choice axiom, but also more general than the condition of Replacement, which demands unique existence <math>\exists!y</math>. In the consequent, firstly, the axioms states that then there exists a set <math>b</math> which contains at least one "image" value <math>y</math> under <math>\phi</math>, for every element of the domain. Secondly, in this axioms formulation it then moreover states that only such images <math>y</math> are elements of that new codomain set <math>b</math>. It is guaranteeing that <math>b</math> does not overshoot the codomain of <math>\phi</math> and thus the axiom is also expressing some power akin to a Separation procedure. The principle may be used in the constructive study of larger sets beyond the everyday need of analysis.

Weak collection and [[axiom schema of predicative separation|predicative separation]] together imply strong collection: separation cuts out the subset of <math>b</math> consisting of those <math>y</math> such that <math>\phi(x,y)</math> for some <math>x \in a</math>.

====Metalogic====
This theory without <math>{\mathrm {PEM}}</math>, without unbounded separation and without "naive" Power set enjoys various nice properties. For example, as opposed to <math>{\mathsf {CZF}}</math> with its subset collection schema below, it has the [[Disjunction and existence properties#Existence property|existence property]].

=== Constructive Zermelo–Fraenkel ===
====Binary refinement====
The so called binary refinement axiom says that for any <math>a</math> there exists a set <math>{\mathcal B}_a\subset{\mathcal P}_a</math> such that for any covering <math>a=x\cup y</math>, the set <math>{\mathcal B}_a</math> holds two subsets <math>c\subset x</math> and <math>d\subset y</math> that also do this covering job, <math>a=c\cup d</math>. It is a weakest form of the powerset axiom and at the core of some important mathematical proofs.
Fullness below, for relations between the set <math>a</math> and the finite <math>\{0,1\}</math>, implies that this is indeed possible.

Taking another step back, <math>{\mathsf {ECST}}</math> plus Recursion and plus Binary refinement already proves that there exists an Archimedean, Dedekind complete pseudo-ordered field. That set theory also proves that the class of left [[Dedekind cut]]s is a set, not requiring Induction or Collection. And it moreover proves that function spaces into discrete sets are sets (there e.g. <math>\omega\to\omega</math>), without assuming <math>{\mathrm {Exp}}</math>. Already over the weak theory <math>{\mathsf {BCST}}</math> (which is to say without Infinity) does binary refinement prove that function spaces into discrete sets are sets, and therefore e.g. the existence of all [[characteristic function]] spaces <math>\{0,1\}^a</math>.

====Subset Collection====
The theory known as <math>{\mathsf {CZF}}</math> adopts the axioms of the previous sections plus a stronger form of Exponentiation. It is by adopting the following alternative to Exponentiation, which can again be seen as a constructive version of the [[Power set axiom]]:
{| border=1 style="border:0px"
| style="border:1px solid #000000; padding:1.0em; background-color:#F8F9FA" |
Axiom schema of Subset Collection: For any predicate <math>\phi</math>,
; <math>\forall a. \forall b.\ \ \exists u. \forall z. \big(\forall (x \in a). \exists (y \in b). \phi(x,y,z)\big) \to \exists (v \in u). \big(\forall (x \in a). \exists (y \in v). \phi(x,y,z)\; \land\; \forall (y \in v). \exists (x \in a). \phi(x,y,z)\big)</math>
|}
An alternative that is not a schema is elaborated on below.

====Fullness====
For given <math>a</math> and <math>b</math>, let <math>{\mathcal R}_{ab}</math> be the class of all [[total relation]]s between <math>a</math> and <math>b</math>. This class is given as
:<math>r \in {\mathcal R}_{ab} \leftrightarrow \Big(\big(\forall (x \in a). \exists (y \in b). \langle x, y \rangle \in r\big) \, \land\,  \big(\forall (p \in r). \exists (x \in a). \exists (y \in b). p = \langle x, y \rangle\big)\Big)</math>
As opposed to the function definition, there is no unique existence quantifier in <math>\exists!(y \in b)</math>. The class <math>{\mathcal R}_{ab}</math> represents the space of "non-unique-valued functions" or "[[multivalued function]]s" from <math>a</math> to <math>b</math>, but as set of individual pairs with right projection in <math>b</math>. The second clause says that one is concerned with only these relations, not those which are total on <math>a</math> but also extend their domain beyond <math>a</math>.

One does not postulate <math>{\mathcal R}_{ab}</math> to be a set, since with Replacement one can use this collection of relations between a set <math>a</math> and the finite <math>b=\{0, 1\}</math>, i.e. the "bi-valued functions on <math>a</math>", to extract the set <math>{\mathcal P}_a</math> of all its subsets. In other words <math>{\mathcal R}_{ab}</math> being a set would imply the Powerset axiom.

Over <math>{\mathsf{ECTS}}+\text{Strong Collection}</math>, there is a single, somewhat clearer '''alternative axiom to the Subset Collection schema'''. It postulates the existence of a sufficiently large ''set'' <math>{\mathcal S}_{ab}</math> of total relations between <math>a</math> and <math>b</math>.
{| border=1 style="border:0px"
| style="border:1px solid #000000; padding:1.0em; background-color:#F8F9FA" |
Axiom of Fullness:
; <math>\forall a. \forall b.\ \exists {\mathcal S}_{ab}.\, ({\mathcal S}_{ab} \subset {\mathcal R}_{ab})\, \land\, \forall (r \in {\mathcal R}_{ab}). \exists (s \in {\mathcal S}_{ab}). s\subset r</math>
|}
This says that for any two sets <math>a</math> and <math>b</math>, there exists a set <math>{\mathcal S}_{ab}\subset {\mathcal R}_{ab}</math> which among its members inhabits a still total relation <math>s\in {\mathcal S}_{ab}</math> for any given total relation <math>r\in {\mathcal R}_{ab}</math>.

On a given domain <math>a</math>, the functions are exactly the sparsest total relations, namely the unique valued ones. Therefore, the axiom implies that there is a set such that all functions are in it. In this way, Fullness implies Exponentiation. It further implies binary refinement, already over <math>{\mathsf {BCST}}</math>.

The Fullness axiom, as well as dependent choice, is in turn also implied by the so-called Presentation Axiom about sections, which can also be formulated [[category theory|category theoretically]].

===Metalogic of CZF===
<math>{\mathsf {CZF}}</math> has the [[Disjunction and existence properties|numerical existence property and the disjunctive property]], but there are concessions: <math>{\mathsf {CZF}}</math> lacks the existence property due to the Subset Collection Schema or Fullness axiom. The schema can also be an obstacle for realizability models. The existence property is not lacking when the weaker Exponentiation or the stronger but impredicative Powerset axiom is adopted instead. The latter is in general lacking a constructive interpretation.

====Unprovable claims====
The theory is consistent with some anti-classical assertions, but on its own proves nothing not provable in <math>{\mathsf {ZF}}</math>. Some prominent statements not proven by the theory (nor by <math>{\mathsf {IZF}}</math>, for that matter) are part of the principles listed above, in the sections on constructive schools in analysis, on the Cauchy construction and on non-constructive principles. What follows concerns set theoretical concepts:

The bounded notion of a transitive set of transitive sets is a good way to define ordinals and enables induction on ordinals. But notably, this definition includes some <math>\Delta_0</math>-subsets in <math>{\mathsf {CZF}}</math>. So assuming that the membership of <math>0</math> is decidable in all successor ordinals <math>S\alpha</math> proves <math>{\mathrm {PEM}}</math> for bounded formulas in <math>{\mathsf {CZF}}</math>. Also, neither [[Total order|linearity]] of [[ordinal number|ordinals]], nor existence of power sets of finite sets are derivable in this theory, as assuming either implies Power set. The circumstance that ordinals are better behaved in the classical than in the constructive context manifests in a different theory of large set existence postulates.

Consider the functions the domain of which is <math>\omega</math> or some <math>n\in\omega</math>. These are sequences and their ranges are counted sets. Denote by <math>C</math> the class characterized as the smallest codomain such that the ranges of the aforementioned functions into <math>C</math> are also itself members of <math>C</math>. In <math>{\mathsf {ZF}}</math>, this is the ''set'' <math>H_{\aleph_1}</math> of [[hereditarily countable set]]s and has ordinal rank at most <math>\omega_2</math>. In <math>{\mathsf {ZF}}</math>, it is uncountable (as it also contains all countable ordinals, the cardinality of which is denoted <math>\aleph_1</math>) but its cardinality is not necessarily that of <math>{\mathbb R}</math>. Meanwhile, <math>{\mathsf {CZF}}</math> does not prove <math>C</math> even constitutes a set, even when [[countable choice]] is assumed.

Finally, the theory does not prove that all function spaces formed from sets in the [[constructible universe]] <math>L</math> are sets ''inside'' <math>L</math>, and this holds even when assuming Powerset instead of the weaker Exponentiation axiom. So this is a particular statement preventing <math>{\mathsf {CZF}}</math> from proving the class <math>L</math> to be a model of <math>{\mathsf {CZF}}</math>.

====Ordinal analysis====
Taking <math>{\mathsf {CZF}}</math> and dropping set induction gives a theory that is conservative over <math>{\mathsf {HA}}</math> for arithmetic statements, in that sense that it proves the same arithmetical statements for its <math>{\mathsf {HA}}</math>-model <math>\omega</math>. Adding back just mathematical induction gives a theory with [[Ordinal analysis|proof theoretic ordinal]] <math>\varphi(\varepsilon_0, 0)</math>, which is the first common fixed point of the [[Veblen function]]s <math>\varphi_\beta</math> for <math>\beta < \varepsilon_0</math>. This is the same ordinal as for <math>{\mathsf {ML_1}}</math> and is below the [[Feferman–Schütte ordinal]] <math>\Gamma_0</math>.
Exhibiting a type theoretical model, the full theory <math>{\mathsf {CZF}}</math> goes beyond <math>\Gamma_0</math>, its ordinal still being the modest Bachmann–Howard ordinal.
Assuming the class of trichotomous ordinals is a set raises the proof theoretical strength of <math>{\mathsf {CZF}}</math> (but not of <math>{\mathsf {IZF}}</math>).

Being related to inductive definitions or [[bar induction]], the regular extension axiom <math>{\mathrm {REA}}</math> raises the proof theoretical strength of <math>{\mathsf {CZF}}</math>. This large set axiom, granting the existence of certain nice supersets for every set, is proven by <math>{\mathsf {ZFC}}</math>.

====Models====
The category of sets and functions of <math>{\mathsf {CZF}}+{\mathrm {REA}}</math> is a <math>\Pi W</math>-pretopos. Without diverging into [[topos theory]], certain extended such <math>\Pi W</math>-pretopoi contain models of <math>{\mathsf {CZF}}+{\mathrm {REA}}</math>. The [[effective topos]] contains a model of this <math>{\mathsf {CZF}}+{\mathrm {REA}}</math> based on maps characterized by certain good subcountability properties.

Separation, stated redundantly in a classical context, is constructively not implied by Replacement. The discussion so far only committed to the predicatively justified bounded Separation. Note that full Separation (together with <math>{\mathrm {RDC}}</math>, <math>{\mathrm {MP}}</math> and also <math>{\mathrm {IP}}</math> for sets) is validated in some effective topos models, meaning the axiom does not spoil cornerstones of the restrictive recursive school.

Related are type theoretical interpretations.
In 1977 Aczel showed that <math>{\mathsf {CZF}}</math> can still be interpreted in [[Martin-Löf type theory]],<ref>Aczel, Peter: 1978. The type theoretic interpretation of constructive set theory. In: A. MacIntyre et al. (eds.), Logic Colloquium '77, Amsterdam: North-Holland, 55–66.</ref> using the [[propositions-as-types]] approach. More specifically, this uses one universe and <math>W</math>-types, providing what is now seen a standard model of <math>{\mathsf {CZF}}</math> in <math>{\mathsf {ML_1V}}</math>.<ref>{{citation|editor1-first=Godehard |editor1-last=Link|title=One Hundred Years of Russell ́s Paradox: Mathematics, Logic, Philosophy|year=2004|publisher=Walter de Gruyter|isbn=978-3-11-019968-0| chapter =Predicativity, Circularity, and Anti-Foundation | first = M. | last= Rathjen| chapter-url=http://www1.maths.leeds.ac.uk/~rathjen/russelle.pdf}}</ref>
This is done in terms of the images of its functions and has a fairly direct constructive and predicative justification, while retaining the language of set theory. Roughly, there are two "big" types <math>U, V</math>, the sets are all given through any <math>f\colon A\to V</math> on some <math>A\colon U</math>, and membership of a <math>x</math> in the set is defined to hold when <math>\exists(a\colon A). f(a)=x</math>.
Conversely, <math>{\mathsf {CZF}}</math> interprets <math>{\mathsf {ML_1V}}</math>.
All statements validated in the subcountable model of the set theory can be proven exactly via <math>{\mathsf {CZF}}</math> plus the [[axiom of dependent choice|choice principle]] <math>\Pi\Sigma</math>-<math>\mathrm{AC}</math>, stated further above.
As noted, theories like <math>{\mathsf {CZF}}</math>, and also together with choice, have the existence property for a broad class of sets in common mathematics.
Martin-Löf type theories with additional induction principles validate corresponding set theoretical axioms.

[[Soundness]] and [[completeness (logic)|Completeness theorems]] of <math>{\mathsf {CZF}}</math>, with respect to [[realizability]], have been established.

====Breaking with ZF====
One may of course add a Church's thesis.

One may postulate the [[subcountable|subcountability]] of all sets. This already holds true in the type theoretical interpretation and the model in the effective topos. By Infinity and Exponentiation, <math>\omega\to\omega</math> is an uncountable set, while the class <math>{\mathcal P}_\omega</math> or even <math>{\mathcal P}_1</math> is then provenly not a set, by [[Cantor's diagonal argument#Ordering of cardinals|Cantor's diagonal argument]]. So this theory then logically rejects Powerset and of course <math>{\mathrm {PEM}}</math>.
Subcountability is also in contradiction with various [[Critical point (set theory)|large set axioms]]. (On the other hand, also using <math>{\mathsf {CZF}}</math>, some such axioms imply the consistency of theories such as <math>{\mathsf {ZF}}</math> and stronger.)

As a rule of inference, <math>{\mathsf {CZF}}</math> is closed under [[Anne Sjerp Troelstra|Troelstra's]] general uniformity for both <math>z=\omega</math> and <math>z=\{0, 1\}</math>. One may adopt it as an anti-classical axiom schema, the uniformity principle which may be denoted <math>{\mathrm {UP}}</math>,
:<math>\forall z. \big(\forall x. \exists (y\in z). \phi(x, y)\big)\to \exists (y\in z). \forall x. \phi(x, y)</math>
This also is incompatible with the powerset axiom. 
The principle is also often formulated for <math>z=\omega</math>. Now for a binary set of labels <math>z=\{0, 1\}</math>, <math>{\mathrm {UP}}</math> implies the indecomposability schema <math>{\mathrm {UZ}}</math>, as noted.

In 1989 Ingrid Lindström showed that [[non-well-founded set]]s can also be interpreted in Martin-Löf type theory, which are obtained by replacing Set Induction in <math>{\mathsf {CZF}}</math> with [[Aczel's anti-foundation axiom]].<ref>Lindström, Ingrid: 1989. [https://www.cambridge.org/core/journals/journal-of-symbolic-logic/article/construction-of-nonwellfounded-sets-within-martinlofs-type-theory/2F809631E20B1E61F5EC1A3BB3765D1E A construction of non-well-founded sets within Martin-Löf type theory]. Journal of Symbolic Logic 54: 57–64.</ref> 
The resulting theory <math>{\mathsf {CZFA}}</math> may be studied by also adding back the <math>\omega</math>-induction schema or relativized [[dependent choice]], as well as the assertion that every set is member of a [[transitive set]].

===Intuitionistic Zermelo–Fraenkel===
The theory <math>{\mathsf {IZF}}</math> is <math>{\mathsf {CZF}}</math> '''adopting both the standard [[Axiom schema of separation|Separation]] as well as [[Axiom of power set|Power set]]''' and, as in <math>{\mathsf {ZF}}</math>, one conventionally formulates the theory with Collection below. As such, <math>{\mathsf {IZF}}</math> can be seen as the most straight forward variant of <math>{\mathsf {ZF}}</math> without {{math|PEM}}.
So as noted, in <math>{\mathsf{IZF}}</math>, in place of Replacement, one may use the
{| border=1 style="border:0px"
| style="border:1px solid #000000; padding:1.0em; background-color:#F8F9FA" |
[[Axiom schema of replacement#Axiom schema of collection|Axiom schema of collection]]: For any predicate <math>\phi</math>,
; <math>\forall z. \big(\forall (x \in z). \exists y. \phi(x,y)\big) \to \exists w. \forall (x \in z). \exists (y \in w). \phi(x,y)</math>
|}
While the axiom of replacement requires the relation {{mvar|&varphi;}} to be [[function (set theory)|functional]] over the set {{mvar|z}} (as in, for every {{mvar|x}} in {{mvar|z}} there is associated exactly one {{mvar|y}}), the Axiom of Collection does not.
It merely requires there be associated at least one {{mvar|y}}, and it asserts the existence of a set which collects at least one such {{mvar|y}} for each such {{mvar|x}}.
In classical <math>{\mathsf{ZFC}}</math>, the Collection schema implies the [[Axiom schema of replacement]]. When making use of Powerset (and only then), they can be shown to be classically equivalent.

While <math>{\mathsf {IZF}}</math> is based on intuitionistic rather than classical logic, it is considered [[impredicative]].
It allows formation of sets via a power set operation and using the general [[Axiom schema of specification|Axiom of Separation]] with any proposition, including ones which contain [[quantifier (logic)|quantifier]]s which are not bounded. Thus new sets can be formed in terms of the universe of all sets, distancing the theory from the bottom-up constructive perspective. So it is even easier to define ''sets'' <math>\{x\in B\mid Q(x)\}</math> with undecidable membership, namely by making use of undecidable predicates defined on a set.
The power set axiom further implies the existence of a set of [[truth value]]s. In the presence of excluded middle, this set has two elements. In the absence of it, the set of truth values is also considered impredicative. The axioms of <math>{\mathsf {IZF}}</math> are strong enough so that full {{math|PEM}} is already implied by {{math|PEM}} for bounded formulas. See also the previous discussion in the section on the Exponentiation axiom. And by the discussion about Separation, it is thus already implied by the particular formula <math>\forall x. \big(0\in x\lor 0\notin x\big)</math>, the principle that knowledge of membership of <math>0</math> shall always be decidable, no matter the set.

====Metalogic====
As implied above, the subcountability property cannot be adopted for all sets, given the theory proves <math>{\mathcal P}_\omega</math> to be a set.
The theory has many of the nice [[Disjunction and existence properties#Existence property|numerical existence properties]] and is e.g. consistent with Church's thesis principle as well as with <math>\omega\to\omega</math> being subcountable. It also has the disjunctive property.

<math>{\mathsf {IZF}}</math> with Replacement instead of Collection has the general existence property, even when adopting relativized dependent choice on top of it all. But just <math>{\mathsf {IZF}}</math> as formulated does not. The combination of schemas including full separation spoils it.

Even without {{math|PEM}}, the [[Ordinal analysis|proof theoretic strength]] of <math>{\mathsf {IZF}}</math> equals that of <math>{\mathsf {ZF}}</math>. And <math>{\mathsf {HA}}</math> proves them equiconsistent and they prove the same <math>\Pi_1^0</math>-sentences.

===Intuitionistic Z===
Again on the weaker end, as with its historical counterpart [[Zermelo set theory]], one may denote by <math>{\mathsf {IZ}}</math> the intuitionistic theory set up like <math>{\mathsf {IZF}}</math> but without Replacement, Collection or Induction.

===Intuitionistic KP===
Let us mention another very weak theory that has been investigated, namely Intuitionistic (or constructive) [[Kripke–Platek set theory]] <math>{\mathsf {IKP}}</math>.
It has not only Separation but also Collection restricted to <math>\Delta_0</math>-formulas, i.e. it is similar to <math>{\mathsf {BCST}}</math> but with Induction instead of full Replacement. The theory does not fit into the hierarchy as presented above, simply because it has [[Epsilon-induction|Axiom schema of Set Induction]] from the start. This enables theorems involving the class of ordinals. The theory has the disjunction property.
Of course, weaker versions of <math>{\mathsf {IKP}}</math> are obtained by restricting the induction schema to narrower classes of formulas, say <math>\Sigma_1</math>. The theory is especially weak when studied without Infinity.

==Sorted theories==
===Constructive set theory===
As he presented it, Myhill's system <math>{\mathsf {CST}}</math> is a theory using constructive first-order logic with identity and two more [[many-sorted logic|sorts]] beyond sets, namely [[natural numbers]] and [[function (mathematics)|function]]s. Its axioms are:
* The usual [[Axiom of Extensionality]] for sets, as well as one for functions, and the usual [[Axiom of union]].
* The Axiom of restricted, or predicative, [[Axiom schema of predicative separation|separation]], which is a weakened form of the [[Axiom schema of separation|Separation axiom]] from classical set theory, requiring that any [[quantification (logic)|quantification]]s be bounded to another set, as discussed.
* A form of the [[Axiom of Infinity]] asserting that the collection of natural numbers (for which he introduces a constant <math>\omega</math>) is in fact a set.
* The axiom of Exponentiation, asserting that for any two sets, there is a third set which contains all (and only) the functions whose domain is the first set, and whose range is the second set. This is a greatly weakened form of the [[Axiom of power set]] in classical set theory, to which Myhill, among others, objected on the grounds of its [[impredicative|impredicativity]].

And furthermore:
* The usual [[Peano axioms]] for natural numbers.
* Axioms asserting that the [[domain of a function|domain]] and [[range of a function|range]] of a function are both sets. Additionally, an [[Axiom of non-choice]] asserts the existence of a choice function in cases where the choice is already made. Together these act like the usual [[Axiom schema of replacement|Replacement axiom]] in classical set theory.

One can roughly identify the strength of this theory with a constructive subtheories of <math>{\mathsf {ZF}}</math> when comparing with the previous sections.

And finally the theory adopts
* An [[Axiom of dependent choice]], which is much weaker than the usual [[Axiom of choice]].

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

A lot of [[constructive analysis|analysis]] and [[Module (mathematics)|module theory]] has been developed in this context.

===Category theories===
Not all formal logic theories of sets need to axiomize the binary membership predicate "<math>\in</math>" directly. A theory like the Elementary Theory of the Categories Of Set (<math>{\mathsf {ETCS}}</math>), e.g. capturing pairs of composable mappings between objects, can also be expressed with a constructive background logic. [[Category theory]] can be set up as a theory of arrows and objects, although [[List of first-order theories|first-order]] axiomatizations only in terms of arrows are possible.

Beyond that, topoi also have [[categorical logic|internal languages]] that can be intuitionistic themselves and capture a [[Subobject classifier|notion of set]]s.

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

==See also==
{{cols}}
* [[Axiom schema of predicative separation]]
* [[Constructivism (philosophy of mathematics)|Constructive mathematics]]
* [[Constructive analysis]]
* [[Church's thesis (constructive mathematics)|Constructive Church's thesis rule and principle]]
* [[Computable set]]
* [[Diaconescu's theorem]]
* [[Disjunction and existence properties]]
* [[Epsilon-induction]]
* [[Hereditarily finite set]]
* [[Heyting arithmetic]]
* [[Impredicativity]]
* [[Intuitionistic type theory]]
* [[Law of excluded middle]]
* [[Ordinal analysis]]
* [[Set theory]]
* [[Subcountability]]
{{colend}}

==References==
{{Reflist}}

== Further reading ==
* {{cite book|isbn=978-0-444-70358-3|title=Constructivism in Mathematics, Vol. 2|last1=Troelstra|first1=Anne|author-link1=Anne Sjerp Troelstra|last2=van Dalen|first2=Dirk|author-link2=Dirk van Dalen|series=Studies in Logic and the Foundations of Mathematics|year=1988|page=[https://archive.org/details/constructivismin0002troe/page/619 619]|url=https://archive.org/details/constructivismin0002troe/page/619}}
* Aczel, P. and Rathjen, M. (2001). [https://web.archive.org/web/20070204153712/http://www.ml.kva.se/preprints/meta/AczelMon_Sep_24_09_16_56.rdf.html Notes on constructive set theory]. Technical Report 40, 2000/2001. Mittag-Leffler Institute, Sweden.

== External links ==
* {{Cite SEP
|author-last= Crosilla
|author-first= Laura
|url-id= set-theory-constructive/
|title= Set Theory: Constructive and Intuitionistic ZF
|date= 13 February 2019
}}
*{{Cite web
|last= Van den Berg
|first= Benno
|url= https://projects.illc.uva.nl/KNAW/Heyting/uploaded_files/inlineitem/vdberg-slides.pdf
|title= Constructive set theory – an overview
|date= 7 September 2012
|quote= Slides from Heyting dag, Amsterdam
}}

{{Foundations-footer}}
{{Non-classical logic}}
{{Mathematical logic}}
{{Set theory}}

{{DEFAULTSORT:Constructive Set Theory}}
[[Category:Constructivism (mathematics)]]
[[Category:Intuitionism]]
[[Category:Systems of set theory]]