Misplaced Pages

Axiomatic constructive set theory is an approach to mathematical constructivism following the program of axiomatic set theory. The same first-order language with "${\displaystyle =}$" and "${\displaystyle \in }$" of classical set theory is usually used, so this is not to be confused with a constructive types approach. On the other hand, some constructive theories are indeed motivated by their interpretability in type theories.

In addition to rejecting the principle of excluded middle (${\displaystyle {\mathrm {PEM} }}$), constructive set theories often require some logical quantifiers in their axioms to be set 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 in that it rejects the principle of excluded middle ${\displaystyle {\mathrm {PEM} }}$, i.e. that the disjunction ${\displaystyle \phi \lor \neg \phi }$ automatically holds for all propositions ${\displaystyle \phi }$. This is also often called the law of excluded middle (${\displaystyle {\mathrm {LEM} }}$) in contexts where it is assumed. Constructively, as a rule, to prove the excluded middle for a proposition ${\displaystyle P}$, i.e. to prove the particular disjunction ${\displaystyle P\lor \neg P}$, either ${\displaystyle P}$ or ${\displaystyle \neg P}$ 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 ${\displaystyle Q(x)}$ for ${\displaystyle x}$ in a domain ${\displaystyle X}$ is said to be decidable when the more intricate statement ${\displaystyle \forall (x\in X).{\big (}Q(x)\lor \neg Q(x){\big )}}$ is provable. Non-constructive axioms may enable proofs that formally claim decidability of such ${\displaystyle P}$ (and/or ${\displaystyle Q}$) in the sense that they prove excluded middle for ${\displaystyle P}$ (resp. the statement using the quantifier above) without demonstrating the truth of either side of the disjunction(s). This is often the case in classical logic. In contrast, axiomatic theories deemed constructive tend to not permit many classical proofs of statements involving properties that are provenly computationally undecidable.

The law of noncontradiction is a special case of the propositional form of modus ponens. Using the former with any negated statement ${\displaystyle \neg P}$, one valid De Morgan's law thus implies ${\displaystyle \neg \neg (P\lor \neg P)}$ 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 ${\displaystyle P}$) from the assumed axioms.

More generally, constructive mathematical theories tend to prove classically equivalent reformulations of classical theorems. For example, in constructive analysis, one cannot prove the intermediate value theorem in its textbook formulation, but one can prove theorems with algorithmic content that, as soon as double negation elimination and its consequences are assumed legal, are at once classically equivalent to the classical statement. The difference is that the constructive proofs are harder to find.

The intuitionistic logic underlying the set theories discussed here, unlike minimal logic, still permits double negation elimination for individual propositions ${\displaystyle P}$ for which excluded middle holds. In turn the theorem formulations regarding finite objects tends to not differ from their classical counterparts. Given a model of all natural numbers, the equivalent for predicates, namely Markov's principle, does not automatically hold, but may be considered as an additional principle.

In an inhabited domain and using explosion, the disjunction ${\displaystyle P\lor \exists (x\in X).\neg Q(x)}$ implies the existence claim ${\displaystyle \exists (x\in X).(Q(x)\to P)}$, which in turn implies ${\displaystyle {\big (}\forall (x\in X).Q(x){\big )}\to P}$. 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 ${\displaystyle P}$ is rejected, one deals with a counter-example existence claim ${\displaystyle \exists (x\in X).\neg Q(x)}$, which is generally constructively stronger than a rejection claim ${\displaystyle \neg \forall (x\in X).Q(x)}$: Exemplifying a ${\displaystyle t}$ such that ${\displaystyle Q(t)}$ is contradictory of course means it is not the case that ${\displaystyle Q}$ holds for all possible ${\displaystyle x}$. But one may also demonstrate that ${\displaystyle Q}$ holding for all ${\displaystyle x}$ 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 ${\displaystyle f\subset X\times Y}$ involving unbounded collections constitute a (mathematical, and so always meaning 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 ${\displaystyle {\mathrm {PEM} }}$ for the formulas permitted in one's adopted Separation schema, by Diaconescu's theorem. Similar results hold for the Axiom of Regularity existence claim, as shown below. The latter has a classically equivalent inductive substitute. So a genuinely intuitionistic development of set theory requires the rewording of some standard axioms to classically equivalent ones. Apart from demands for computability and reservations regrading of impredicativity, technical question regarding which 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 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, ${\displaystyle \top }$ or ${\displaystyle \bot }$. Also the real line may be taken to be indecomposable in this sense. Undecidability of disjunctions also affects the claims about total orders such as that of all ordinal numbers, expressed by the provability and rejection of the clauses in the order defining disjunction ${\displaystyle (\alpha \in \beta )\lor (\alpha =\beta )\lor (\beta \in \alpha )}$. This determines whether the relation is trichotomous. A weakened theory of ordinals in turn affects the proof theoretic strength defined in ordinal analysis.

In exchange, constructive set theories can exhibit attractive disjunction and existence properties, as is familiar from the study of constructive arithmetic theories. These are features of a fixed theory which metalogically relate judgements of propositions provable in the theory. Particularly well-studied are those such features that can be expressed in Heyting arithmetic, with quantifiers over numbers and which can often be realized by numbers, as formalized in proof theory. In particular, those are the numerical existence property and the closely related disjunctive property, as well as being closed under Church's rule, witnessing any given function to be computable.

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 ${\displaystyle \phi }$, 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 ${\displaystyle \psi }$ that uniquely describes such a set instance. More formally, for any predicate ${\displaystyle \phi }$ there is a predicate ${\displaystyle \psi }$ so that

${\displaystyle {\mathsf {T}}\vdash \exists x.\phi (x)\implies {\mathsf {T}}\vdash \exists !x.\phi (x)\land \psi (x)}$

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, a theory denoted ${\displaystyle {\mathsf {ZF}}+({\mathrm {V} }={\mathrm {HOD} })}$, no sets without such definability exist. The property is also enforced via the constructible universe postulate in ${\displaystyle {\mathsf {ZF}}+({\mathrm {V} }={\mathrm {L} })}$. For contrast, consider the theory ${\displaystyle {\mathsf {ZFC}}}$ given by ${\displaystyle {\mathsf {ZF}}}$ 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 ${\displaystyle W\subset {\mathbb {R} }\times {\mathbb {R} }}$ formally exist that establish the well-ordering of ${\displaystyle {\mathbb {R} }}$ (i.e. the theory claims the existence of a least element for all subsets of ${\displaystyle {\mathbb {R} }}$ with respect to those relations). This is despite the fact that definability of such an ordering is known to be independent of ${\displaystyle {\mathsf {ZFC}}}$. The latter implies that for no particular formula ${\displaystyle \psi }$ in the language of the theory does the theory prove that the corresponding set is a well-ordering relation of the reals. So ${\displaystyle {\mathsf {ZFC}}}$ formally proves the existence of a subset ${\displaystyle W\subset {\mathbb {R} }\times {\mathbb {R} }}$ with the property of being a well-ordering relation, but at the same time no particular set ${\displaystyle W}$ for which the property could be validated can possibly be defined.

Anti-classical principles

As mentioned above, a constructive theory ${\displaystyle {\mathsf {T}}}$ may exhibit the numerical existence property, ${\displaystyle {\mathsf {T}}\vdash \exists e.\psi (e)\implies {\mathsf {T}}\vdash \psi ({\underline {\mathrm {e} }})}$, for some number ${\displaystyle {\mathrm {e} }}$ and where ${\displaystyle {\underline {\mathrm {e} }}}$ denotes the corresponding numeral in the formal theory. Here one must carefully distinguish between provable implications between two propositions, ${\displaystyle {\mathsf {T}}\vdash P\to Q}$, and a theory's properties of the form ${\displaystyle {\mathsf {T}}\vdash P\implies {\mathsf {T}}\vdash Q}$. 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 ${\displaystyle {\mathsf {T}}}$ 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 "${\displaystyle \to }$") to ${\displaystyle {\mathsf {T}}}$, as an axiom schema or in quantified form. A situation commonly studied is that of a fixed ${\displaystyle {\mathsf {T}}}$ exhibiting the meta-theoretical property of the following type: For an instance from some collection of formulas of a particular form, here captured via ${\displaystyle \phi }$ and ${\displaystyle \psi }$, one established the existence of a number ${\displaystyle {\mathrm {e} }}$ so that ${\displaystyle {\mathsf {T}}\vdash \phi \implies {\mathsf {T}}\vdash \psi ({\underline {\mathrm {e} }})}$. Here one may then postulate ${\displaystyle \phi \to \exists (e\in {\mathbb {N} }).\psi (e)}$, where the bound ${\displaystyle e}$ is a number variable in language of the theory. For example, Church's rule is an admissible rule in first-order Heyting arithmetic ${\displaystyle {\mathsf {HA}}}$ and, furthermore, the corresponding Church's thesis principle ${\displaystyle {\mathrm {CT} }_{0}}$ 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 ${\displaystyle {\mathrm {PEM} }}$. Similarly, adjoining the excluded middle principle ${\displaystyle {\mathrm {PEM} }}$ to some theory ${\displaystyle {\mathsf {T}}}$, 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 ${\displaystyle {\mathsf {T}}}$. In such a fashion, ${\displaystyle {\mathrm {CT} }_{0}}$ may not be adopted in ${\displaystyle {\mathsf {HA}}+{\mathrm {PEM} }}$, also known as Peano arithmetic ${\displaystyle {\mathsf {PA}}}$.

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

${\displaystyle \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 )}}$

Kleene's T predicate together with the result extraction expresses that any input number ${\displaystyle n}$ being mapped to the number ${\displaystyle f(n)}$ is, through ${\displaystyle w}$, witnessed to be a computable mapping. Here ${\displaystyle {\mathbb {N} }}$ now denotes a set theory model of the standard natural numbers and ${\displaystyle e}$ is an index with respect to a fixed program enumeration. Stronger variants have been used, which extend this principle to functions ${\displaystyle f\in {\mathbb {N} }^{X}}$ defined on domains ${\displaystyle X\subset {\mathbb {N} }}$ of low complexity. The principle rejects decidability for the predicate ${\displaystyle Q(e)}$ defined as ${\displaystyle \exists (w\in {\mathbb {N} }).T(e,e,w)}$, expressing that ${\displaystyle e}$ is the index of a computable function halting on its own index. Weaker, double negated forms of the principle may be considered too, which do not require the existence of a recursive implementation for every ${\displaystyle f}$, 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 theory ${\displaystyle {\mathsf {RCA}}_{0}}$, a subsystem of the two-sorted first-order theory ${\displaystyle {\mathsf {Z}}_{2}}$.

The collection of computable functions is classically subcountable, which classically is the same as being countable. But classical set theories will generally claim that ${\displaystyle {\mathbb {N} }^{\mathbb {N} }}$ holds also other functions than the computable ones. For example there is a proof in ${\displaystyle {\mathsf {ZF}}}$ 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 (${\displaystyle {\mathbb {N} }^{\mathbb {N} }}$) 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 ${\displaystyle \forall (x\in X).\neg \neg {\big (}Q(x)\lor \neg Q(x){\big )}}$ for any ${\displaystyle Q}$. And so for any given element ${\displaystyle x}$ of ${\displaystyle X}$, the corresponding excluded middle statement for the proposition cannot be negated. Indeed, for any given ${\displaystyle x}$, by noncontradiction it is impossible to rule out ${\displaystyle Q(x)}$ 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 ${\displaystyle \neg \forall (x\in X).{\big (}Q(x)\lor \neg Q(x){\big )}}$. Adopting this does not necessitate providing a particular ${\displaystyle t\in X}$ witnessing the failure of excluded middle for the particular proposition ${\displaystyle Q(t)}$, i.e. witnessing the inconsistent ${\displaystyle \neg {\big (}Q(t)\lor \neg Q(t){\big )}}$. Predicates ${\displaystyle Q(x)}$ on an infinite domain ${\displaystyle X}$ correspond to decision problems. Motivated by provenly computably undecidable problems, one may reject the possibility of decidability of a predicate without also making any existence claim in ${\displaystyle X}$. As another example, such a situation is enforced in Brouwerian intuitionistic analysis, in a case where the quantifier ranges over infinitely many unending binary sequences and ${\displaystyle Q(x)}$ states that a sequence ${\displaystyle x}$ 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 "${\displaystyle {\mathsf {CST}}}$") begun with John Myhill's work on the theories also called ${\displaystyle {\mathsf {IZF}}}$ and ${\displaystyle {\mathsf {CST}}}$. In 1973, he had proposed the former as a first-order set theory based on intuitionistic logic, taking the most common foundation ${\displaystyle {\mathsf {ZFC}}}$ 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 ${\displaystyle {\mathsf {ZFC}}}$ axioms which are equivalent in the classical setting are inequivalent in the constructive setting, and some forms imply ${\displaystyle {\mathrm {PEM} }}$, as will be demonstrated. In those cases, the intuitionistically weaker formulations were consequently adopted. The far more conservative system ${\displaystyle {\mathsf {CST}}}$ 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 ${\displaystyle {\mathsf {ZF}}}$, leading up to Peter Aczel's well studied ${\displaystyle {\mathsf {CZF}}}$, and beyond. Many modern results trace back to Rathjen and his students. ${\displaystyle {\mathsf {CZF}}}$ is also characterized by the two features present also in Myhill's theory: On the one hand, it is using the Predicative Separation instead of the full, unbounded Separation schema. 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 ${\displaystyle {\mathrm {PEM} }}$ to a theory even weaker than ${\displaystyle {\mathsf {CZF}}}$ recovers ${\displaystyle {\mathsf {ZF}}}$, as detailed below. The system, which has come to be known as Intuitionistic Zermelo–Fraenkel set theory (${\displaystyle {\mathsf {IZF}}}$), is a strong set theory without ${\displaystyle {\mathrm {PEM} }}$. It is similar to ${\displaystyle {\mathsf {CZF}}}$, but less conservative or predicative. The theory denoted ${\displaystyle {\mathsf {IKP}}}$ is the constructive version of ${\displaystyle {\mathsf {KP}}}$, 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 (${\displaystyle {\mathsf {ZF}}}$) with respect to their axiom as well as their underlying logic. Such theories can then also be interpreted in any model of ${\displaystyle {\mathsf {ZF}}}$.

Peano arithmetic ${\displaystyle {\mathsf {PA}}}$ is bi-interpretable with the theory given by ${\displaystyle {\mathsf {ZF}}}$ minus Infinity and without infinite sets, plus the existence of all transitive closures. (The latter is also implied after promoting Regularity to the Set Induction schema, which is discussed below.) Likewise, constructive arithmetic can also be taken as an apology for most axioms adopted in ${\displaystyle {\mathsf {CZF}}}$: Heyting arithmetic ${\displaystyle {\mathsf {HA}}}$ is bi-interpretable with a weak constructive set theory, as also described in the article on ${\displaystyle {\mathsf {HA}}}$. One may arithmetically characterize a membership relation "${\displaystyle \in }$" and with it prove - instead of the existence of a set of natural numbers ${\displaystyle \omega }$ - that all sets in its theory are in bijection with a (finite) von Neumann natural, a principle denoted ${\displaystyle {\mathrm {V} }={\mathrm {Fin} }}$. 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 ${\displaystyle {\mathsf {CZF}}}$ minus the existence of ${\displaystyle \omega }$ but plus ${\displaystyle {\mathrm {V} }={\mathrm {Fin} }}$ as axiom. All those axioms are discussed in detail below. Relatedly, ${\displaystyle {\mathsf {CZF}}}$ also proves that the hereditarily finite sets fulfill all the previous axioms. This is a result which persists when passing on to ${\displaystyle {\mathsf {PA}}}$ and ${\displaystyle {\mathsf {ZF}}}$ minus Infinity.

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

Presheaf models for constructive set theories have also been introduced. These are analogous to presheaf models for intuitionistic set theory developed by Dana Scott in the 1980s. Realizability models of ${\displaystyle {\mathsf {CZF}}}$ within the effective topos have been identified, which, say, at once validate full Separation, relativized dependent choice ${\displaystyle {\mathrm {RDC} }}$, independence of premise ${\displaystyle {\mathrm {IP} }}$ for sets, but also the subcountability of all sets, Markov's principle ${\displaystyle {\mathrm {MP} }}$ and Church's thesis ${\displaystyle {\mathrm {CT} _{0}}}$ in the formulation for all predicates.

Notation

In an axiomatic set theory, sets are the entities exhibiting properties. But there is then a more intricate relation between the set concept and logic. For example, the property of being a natural number smaller than 100 may be reformulated as being a member of the set of numbers with that property. The set theory axioms govern set existence and thus govern which predicates can be materialized as entity in itself, in this sense. Specification is also directly governed by the axioms, as discussed below. For a practical consideration, consider 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 theoretic formalization of a 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 propositional connective symbols used to form syntactic formulas are standard. The axioms of set theory give a means to prove equality "${\displaystyle =}$" 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 "${\displaystyle \neg }$" of equality is sometimes called the denial of equality, and is commonly written "${\displaystyle \neq }$". 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, "${\displaystyle \in }$". As with equality, negation of elementhood "${\displaystyle \in }$" is often written "${\displaystyle \notin }$".

Variables

Below the Greek ${\displaystyle \phi }$ denotes a proposition or predicate variable in axiom schemas and ${\displaystyle P}$ or ${\displaystyle Q}$ is used for particular such predicates. The word "predicate" is sometimes used interchangeably with "formulas" as well, even in the unary case.

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

Classes

As is also common, one makes use set builder notation for classes, which, in most contexts, are not part of the object language but used for concise discussion. In particular, one may introduce notation declarations of the corresponding class via "${\displaystyle A=\{z\mid Q(z)\}}$", for the purpose of expressing any ${\displaystyle Q(a)}$ as ${\displaystyle a\in A}$. Logically equivalent predicates can be used to introduce the same class. One also writes ${\displaystyle \{z\in B\mid Q(z)\}}$ as shorthand for ${\displaystyle \{z\mid z\in B\land Q(z)\}}$. For example, one may consider ${\displaystyle \{z\in B\mid z\notin C\}}$ and this is also denoted ${\displaystyle B\setminus C}$.

One abbreviates ${\displaystyle \forall z.{\big (}z\in A\to Q(z){\big )}}$ by ${\displaystyle \forall (z\in A).Q(z)}$ and ${\displaystyle \exists z.{\big (}z\in A\land Q(z){\big )}}$ by ${\displaystyle \exists (z\in A).Q(z)}$. 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 ${\displaystyle \forall (z\in A).z\in B}$, i.e. ${\displaystyle \forall z.(z\in A\to z\in B)}$, by ${\displaystyle A\subset B}$. For a predicate ${\displaystyle Q}$, trivially ${\displaystyle \forall z.{\big (}(z\in B\land Q(z))\to z\in B{\big )}}$. And so follows that ${\displaystyle \{z\in B\mid Q(z)\}\subset B}$. The notion of subset-bounded quantifiers, as in ${\displaystyle \forall (z\subset A).z\in B}$, 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 ${\displaystyle \exists z.(z\in A)}$, then one calls it inhabited. One may also use quantification in ${\displaystyle A}$ to express this as ${\displaystyle \exists (z\in A).(z=z)}$. The class ${\displaystyle A}$ 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 does capture many of the intuitionistically valid negation rules: ${\displaystyle {\big (}\forall (x\in A).x\notin B{\big )}\leftrightarrow \neg \exists (x\in A).x\in B}$. Using the above notation, this is a purely logical equivalence and in this article the proposition will furthermore be expressible as ${\displaystyle A\cap B=\{\}}$.

A subclass ${\displaystyle A\subset B}$ is called detachable from ${\displaystyle B}$ if the relativized membership predicate is decidable, i.e. if ${\displaystyle \forall (x\in B).x\in A\lor x\notin A}$ 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 ${\displaystyle A\simeq B}$ the statement expressing that two classes have exactly the same elements, i.e. ${\displaystyle \forall z.(z\in A\leftrightarrow z\in B)}$, or equivalently ${\displaystyle (A\subset B)\land (B\subset A)}$. This is not to be conflated with the concept of equinumerosity also used below.

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

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

Syntactically more general, a set ${\displaystyle w}$ may also be characterized using another 2-ary predicate ${\displaystyle R}$ trough ${\displaystyle \forall x.x\in w\leftrightarrow R(x,w)}$, where the right hand side may depend on the actual variable ${\displaystyle w}$, and possibly even on membership in ${\displaystyle w}$ 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 ${\displaystyle {\mathrm {PEM} }}$ 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 "${\displaystyle =}$" of two sets, so that through substitution, any predicate about ${\displaystyle x}$ translates to one of ${\displaystyle y}$. By the logical properties of equality, the converse direction of the postulated implication holds automatically.

In a constructive interpretation, the elements of a subclass ${\displaystyle A=\{z\in B\mid Q(z)\lor \neg Q(z)\}}$ of ${\displaystyle B}$ may come equipped with more information than those of ${\displaystyle B}$, in the sense that being able to judge ${\displaystyle b\in A}$ is being able to judge ${\displaystyle Q(b)\lor \neg Q(b)}$. And (unless the whole disjunction follows from axioms) in the Brouwer–Heyting–Kolmogorov interpretation, this means to have proven ${\displaystyle Q(b)}$ or having rejected it. As ${\displaystyle \{z\in B\mid Q(z)\}}$ may not be detachable from ${\displaystyle B}$, i.e. as ${\displaystyle Q}$ may be not decidable for all elements in ${\displaystyle B}$, the two classes ${\displaystyle A}$ and ${\displaystyle B}$ must a priori be distinguished.

Consider a predicate ${\displaystyle Q}$ that provenly holds for all elements of a set ${\displaystyle y}$, so that ${\displaystyle y\simeq \{z\in y\mid Q(z)\}}$, 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 ${\displaystyle Q}$ 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 ${\displaystyle \forall (x\in w).Q(x)}$, which in informal class notation may be expressed as ${\displaystyle w\subset \{x\mid Q(x)\}}$, is then equivalently expressed as ${\displaystyle \{x\in w\mid Q(x)\}=w}$. This means that establishing such ${\displaystyle \forall }$-theorems (e.g. the ones provable from full mathematical induction) enables substituting the subclass of ${\displaystyle w}$ on the left hand side of the equality for just ${\displaystyle w}$, in any formula.

Note that adopting "${\displaystyle =}$" 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 Fregian notion.

Modern type theories may instead aim at defining the demanded equivalence "${\displaystyle \simeq }$" in terms of functions, see e.g. type equivalence. The related concept of function extensionality is often not adopted in type theory.

Other frameworks for constructive mathematics might instead demand a particular rule for equality or apartness come for the elements ${\displaystyle z\in x}$ of each and every set ${\displaystyle x}$ 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 "${\displaystyle \simeq }$" of those subsets. Relatedly, a loose notion of complementation of two subsets ${\displaystyle u\subset x}$ and ${\displaystyle v\subset x}$ is given when any two members ${\displaystyle s\in u}$ and ${\displaystyle t\in v}$ are provably apart from each other. The collection of complementing pairs ${\displaystyle \langle u,v\rangle }$ is algebraically well behaved.

Merging sets

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

Two other basic existence postulates given some other sets are as follows. Firstly,

Given the definitions above, ${\displaystyle \{x,y\}\subset p}$ expands to ${\displaystyle \forall z.(z=x\lor z=y)\to z\in p}$, so this is making use of equality and a disjunction. The axiom says that for any two sets ${\displaystyle x}$ and ${\displaystyle y}$, there is at least one set ${\displaystyle p}$, which hold at least those two sets.

With bounded Separation below, also the class ${\displaystyle \{x,y\}}$ exists as a set. Denote by ${\displaystyle \langle x,y\rangle }$ the standard ordered pair model ${\displaystyle \{\{x\},\{x,y\}\}}$, so that e.g. ${\displaystyle q=\langle x,y\rangle }$ denotes another bounded formula in the formal language of the theory.

And then, using existential quantification and a conjunction,

saying that for any set ${\displaystyle x}$, there is at least one set ${\displaystyle u}$, which holds all the members ${\displaystyle z}$, of ${\displaystyle x}$'s members ${\displaystyle y}$. The minimal such set is the union.

The two axioms are commonly formulated stronger, in terms of "${\displaystyle \leftrightarrow }$" instead of just "${\displaystyle \to }$", although this is technically redundant in the context of ${\displaystyle {\mathsf {BCST}}}$: As the Separation axiom below is formulated with "${\displaystyle \leftrightarrow }$", for statements ${\displaystyle \exists t.\forall z.\phi (z)\to z\in t}$ the equivalence can be derived, given the theory allows for separation using ${\displaystyle \phi }$. In cases where ${\displaystyle \phi }$ is an existential statement, like here in the union axiom, there is also another formulation using a universal quantifier.

Also using bounded Separation, the two axioms just stated together imply the existence of a binary union of two classes ${\displaystyle a}$ and ${\displaystyle b}$, when they have been established to be sets, denoted by ${\displaystyle \bigcup \{a,b\}}$ or ${\displaystyle a\cup b}$. For a fixed set ${\displaystyle z}$, to validate membership ${\displaystyle z\in a\cup b}$ in the union of two given sets ${\displaystyle y=a}$ and ${\displaystyle y=b}$, one needs to validate the ${\displaystyle z\in y}$ part of the axiom, which can be done by validating the disjunction of the predicates defining the sets ${\displaystyle a}$ and ${\displaystyle b}$, for ${\displaystyle z}$. In terms of the associated sets, it is done by validating the disjunction ${\displaystyle z\in a\lor z\in b}$.

The union and other set forming notations are also used for classes. For instance, the proposition ${\displaystyle z\in A\land z\notin C}$ is written ${\displaystyle z\in A\setminus C}$. Let now ${\displaystyle B\subset A}$. Given ${\displaystyle z\in A}$, the decidability of membership in ${\displaystyle B}$, i.e. the potentially independent statement ${\displaystyle z\in B\lor z\notin B}$, can also be expressed as ${\displaystyle z\in B\cup (A\setminus B)}$. But, as for any excluded middle statement, the double-negation of the latter holds: That union isn't not inhabited by ${\displaystyle z}$. 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 ${\displaystyle \{\}}$ or zero, ${\displaystyle 0}$. That the empty class is a set readily follows from other existence axioms, such as the Axiom of Infinity below. But if, e.g., one is explicitly interested in excluding infinite sets in one's study, one may at this point adopt the

Introduction of the symbol ${\displaystyle \{\}}$ (as abbreviating notation for expressions in involving characterizing properties) is justified as uniqueness for this set can be proven. As ${\displaystyle y\in \{\}}$ is false for any ${\displaystyle y}$, the axiom then reads ${\displaystyle \exists x.x\simeq \{\}}$.

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

More generally, for a set ${\displaystyle x}$, define the successor set ${\displaystyle Sx}$ as ${\displaystyle x\cup \{x\}}$. The interplay of the successor operation with the membership relation has a recursive clause, in the sense that ${\displaystyle (y\in Sx)\leftrightarrow (y\in x\lor y=x)}$. By reflexivity of equality, ${\displaystyle x\in Sx}$, and in particular ${\displaystyle Sx}$ is always inhabited.

BCST

The following makes use of axiom schemas, i.e. axioms for some collection of predicates. Some of the stated axiom schemas shall allow for any collection of set parameters as well (meaning any particular named variables ${\displaystyle v_{0},v_{1},\dots ,v_{n}}$). That is, instantiations of the schema are permitted in which the predicate (some particular ${\displaystyle \phi }$) 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 ${\displaystyle \forall v_{0}.\forall v_{1}.\cdots \forall v_{n}.}$).

Separation

Basic constructive set theory ${\displaystyle {\mathsf {BCST}}}$ consists of several axioms also part of standard set theory, except the so called "full" Separation axiom is weakened. Beyond the four axioms above, it postulates Predicative Separation as well as the Replacement schema.

This axiom amounts to postulating the existence of a set ${\displaystyle s}$ obtained by the intersection of any set ${\displaystyle y}$ and any predicatively described class ${\displaystyle \{x\mid \phi (x)\}}$. For any ${\displaystyle z}$ proven to be a set, when the predicate is taken as ${\displaystyle \phi (x):=x\in z}$, one obtains the binary intersection of sets and writes ${\displaystyle s=y\cap z}$. Intersection corresponds to conjunction in an analog way to how union corresponds to disjunction.

When the predicate is taken as the negation ${\displaystyle \phi (x):=x\notin z}$, one obtains the difference principle, granting existence of any set ${\displaystyle y\setminus z}$. Note that sets like ${\displaystyle y\setminus y}$ or ${\displaystyle \{x\in y\mid \neg (x=x)\}}$ 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 ${\displaystyle \{\}}$ (also denoted ${\displaystyle 0}$). Within this conservative context of ${\displaystyle {\mathsf {BCST}}}$, 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 ${\displaystyle \Delta _{0}}$, the lowest level in the set theoretical Lévy hierarchy. General predicates in set theory are never syntactically restricted in such a way and so, in praxis, generic subclasses of sets are still part of the mathematical language. As the scope of subclasses that are provably sets is sensitive to what sets already exist, this scope is expanded when further set existence postulates added added.

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

If one's separation axiom allows for separation with ${\displaystyle P}$, then ${\displaystyle B}$ is a subset, which may be called the truth value associated with ${\displaystyle P}$. 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 ${\displaystyle P}$ is then also implied by the global statement ${\displaystyle \forall b.(0\in b)\lor (0\notin b)}$.

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 ${\displaystyle \neg \exists x.A\subset x}$, then ${\displaystyle A}$ must be proper. (When taking up the perspective of ${\displaystyle {\mathsf {ZF}}}$ 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 ${\displaystyle A\cup \{x\mid x\notin A\}}$. A constructive proof that it is in that class contains information. Now if ${\displaystyle A}$ is a set, then the class ${\displaystyle \{x\mid x\notin A\}}$ is provably proper. The following demonstrates this in the special case when ${\displaystyle A}$ 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 ${\displaystyle E}$. It gives a purely logical condition such that two terms ${\displaystyle s}$ and ${\displaystyle y}$ cannot be ${\displaystyle E}$-related to one another.

${\displaystyle {\big (}\forall x.xEs\leftrightarrow (xEy\land \neg xEx){\big )}\to \neg (yEs\lor sEs\lor sEy)}$

Most important here is the rejection of the final disjunct, ${\displaystyle \neg sEy}$. The expression ${\displaystyle \neg (x\in x)}$ does not involve unbounded quantification and is thus allowed in Separation. Russel's construction in turn shows that ${\displaystyle \{x\in y\mid x\notin x\}\notin y}$. So for any set ${\displaystyle y}$, Predicative Separation alone implies that there exists a set which is not a member of ${\displaystyle y}$. In particular, no universal set can exist in this theory.

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

For any ${\displaystyle E}$ and ${\displaystyle y}$, the special case ${\displaystyle s=y}$ in the formula above gives

${\displaystyle \neg {\big (}\forall x.xEy\leftrightarrow \neg xEx{\big )}}$

This already implies that no set ${\displaystyle y}$ equals the subclass ${\displaystyle \{x\mid x\notin x\}}$ of the universal class is, i.e. that subclass is a proper one as well. But even in ${\displaystyle {\mathsf {ZF}}}$ without Regularity it is consistent for there to be a proper class of singletons which each contain exactly themselves.

As an aside, in a theory with stratification like Intuitionistic New Foundations, the syntactic expression ${\displaystyle x\in x}$ 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 ${\displaystyle \Delta _{0}}$-Separation or Bounded Separation, as in Separation for set-bounded quantifiers only. (Warning note: The Lévy hierarchy nomenclature is in analogy to ${\displaystyle \Delta _{0}^{0}}$ 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 ${\displaystyle \Sigma _{1}^{0}}$ or higher. Finally note that a ${\displaystyle \Delta _{0}}$ 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 ${\displaystyle {\mathsf {Z}}}$, for mathematical foundations related to topos theory. It is also used in the study of absoluteness, and there part of the formulation of Kripke-Platek set theory.

The restriction in the axiom is also gatekeeping impredicative definitions: Existence should at best not be claimed for objects that are not explicitly describable, or whose definition involves themselves or reference to a proper class, such as when a property to be checked involves a universal quantifier. So in a constructive theory without Axiom of power set, when ${\displaystyle R}$ denotes some 2-ary predicate, one should not generally expect a subclass ${\displaystyle s}$ of ${\displaystyle y}$ to be a set, in case that it is defined, for example, as in

${\displaystyle \{x\in y\mid \forall t.{\big (}(t\subset y)\to R(x,t){\big )}\}}$,

or via a similar definitions involving any quantification over the sets ${\displaystyle t\subset y}$. Note that if this subclass ${\displaystyle s}$ of ${\displaystyle y}$ is provenly a set, then this subset itself is also in the unbounded scope of set variable ${\displaystyle t}$. In other words, as the subclass property ${\displaystyle s\subset y}$ is fulfilled, this exact set ${\displaystyle s}$, defined using the expression ${\displaystyle R(x,s)}$, would play a role in its own characterization.

While predicative Separation leads to fewer given class definitions being sets, it may be emphasized that many class definitions that are classically equivalent are not so when restricting oneself to the weaker logic. Due to the potential undecidability of general predicates, the notion of subset and subclass is automatically more elaborate in constructive set theories than in classical ones. So in this way one has obtained a broader theory. This remains true if full Separation is adopted, such as in the theory ${\displaystyle {\mathsf {IZF}}}$, 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

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

With the Replacement schema, the theory outlined thus far proves that the equivalence classes or indexed sums are sets. In particular, the Cartesian product, holding all pairs of elements of two sets, is a set. In turn, for any fixed number (in the metatheory), the corresponding product expression, say ${\displaystyle x\times x\times x\times x}$, can be constructed as a set. The axiomatic requirements for sets recursively defined in the language are discussed further below. A set ${\displaystyle x}$ is discrete, i.e. equality of elements inside a set ${\displaystyle x}$ is decidable, if the corresponding relation as a subset of ${\displaystyle x\times x}$ is decidable.

Replacement is relevant for function comprehension and can be seen as a form of comprehension more generally. Only when assuming ${\displaystyle {\mathrm {PEM} }}$ does Replacement already imply full Separation. In ${\displaystyle {\mathsf {ZF}}}$, Replacement is mostly important to prove the existence of sets of high rank, namely via instances of the axiom schema where ${\displaystyle \phi (x,y)}$ relates relatively small set ${\displaystyle x}$ to bigger ones, ${\displaystyle y}$.

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

If ${\displaystyle i_{X}}$ is provenly a function on ${\displaystyle X}$ and it is equipped with a codomain ${\displaystyle Y}$ (all discussed in detail below), then the image of ${\displaystyle i_{X}}$ is a subset of ${\displaystyle Y}$. 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 ${\displaystyle H_{\aleph _{0}}}$ can be implemented in any common programming language. The axioms discussed above abstract from common operations on the set data type: Pairing and Union are related to nesting and flattening, or taken together concatenation. Replacement is related to comprehension and Separation is then related to the often simpler filtering. Replacement together with Set Induction (introduced below) suffices to axiomize ${\displaystyle H_{\aleph _{0}}}$ 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. Such principles are relevant for the standard modeling of individual Neumann ordinals. Axiom formulations also exist that pair Union and Replacement in one. While postulating Replacement is not a necessity in the design of a weak constructive set theory that is bi-interpretable with Heyting arithmetic ${\displaystyle {\mathsf {HA}}}$, 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 theories, namely products and the collection of natural numbers as a completed set. Infinite sets are particularly handy to reason about operations applied to sequences defined on unbounded index domains, say the formal differentiation of a generating function or the addition of two Cauchy sequences.

ECST

For some fixed predicate ${\displaystyle I}$ and a set ${\displaystyle a}$, the statement ${\displaystyle I(a)\land {\big (}\forall y.I(y)\to a\subset y{\big )}}$ expresses that ${\displaystyle a}$ is the smallest (in the sense of "${\displaystyle \subset }$") among all sets ${\displaystyle y}$ for which ${\displaystyle I(y)}$ holds true, and that it is always a subset of such ${\displaystyle y}$. 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,

${\displaystyle {\big (}\exists z.z\in A{\big )}\land \forall (x\in A).\exists (s\in A).x\in s}$.

More concretely, denote by ${\displaystyle \mathrm {Ind} _{A}}$ the inductive property,

${\displaystyle (0\in A)\land \forall (x\in A).Sx\in A}$.

In terms of a predicate ${\displaystyle Q}$ underlying the class so that ${\displaystyle \forall x.(x\in A)\leftrightarrow Q(x)}$, the latter translates to ${\displaystyle Q(0)\land \forall x.{\big (}Q(x)\to Q(Sx){\big )}}$.

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

One commonly defines a class ${\displaystyle \omega =\bigcap \{y\mid \mathrm {Ind} _{y}\}}$, the intersection of all inductive sets. (Variants of this treatment may work in terms of a formula that depends on a set parameter ${\displaystyle w}$ so that ${\displaystyle \omega \subset w}$.) The class ${\displaystyle \omega }$ exactly holds all ${\displaystyle x}$ fulfilling the unbounded property ${\displaystyle \forall y.\mathrm {Ind} _{y}\to x\in y}$. The intention is that if inductive sets exist at all, then the class ${\displaystyle \omega }$ shares each common natural number with them, and then the proposition ${\displaystyle \omega \subset A}$, by definition of "${\displaystyle \subset }$", implies that ${\displaystyle Q}$ holds for each of these naturals. While bounded separation does not suffice to prove ${\displaystyle \omega }$ 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 ${\displaystyle {\mathsf {ECST}}}$ has the axiom of ${\displaystyle {\mathsf {BCST}}}$ as well as the postulate

Going on, one takes the symbol ${\displaystyle \omega }$ to denote the now unique smallest inductive set, an unbounded von Neumann ordinal. It contains the empty set and, for each set in ${\displaystyle \omega }$, another set in ${\displaystyle \omega }$ that contains one element more.

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

For some predicate of sets ${\displaystyle P}$, the statement ${\displaystyle \forall S.(S\subset \omega \to P(S))}$ claims ${\displaystyle P}$ 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 "${\displaystyle <}$" on the naturals is captured by their membership relation "${\displaystyle \in }$". The theory proves the order as well as the equality relation on this set to be decidable. Not only is no number smaller than ${\displaystyle 0}$, but induction implies that among subsets of ${\displaystyle \omega }$, it is exactly the empty set which has no least member. The contrapositive of this proves the double-negated least number existence for all non-empty subsets of ${\displaystyle \omega }$. 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 ${\displaystyle b:=\{z\in 1\mid P\}\cup \{1\}}$ of ${\displaystyle \omega }$ is equivalent to excluded middle for ${\displaystyle P}$, and a constructive theory will therefore not prove ${\displaystyle \omega }$ to be well-ordered.

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, ${\displaystyle \exists y.\mathrm {Ind} _{y}}$ - such an existence postulate suffices when full Separation may then be used to carve out the inductive subset ${\displaystyle w}$ 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 ${\displaystyle \Delta _{0}}$ predecessor existence property in the sense of the von Neumann model:

${\displaystyle \forall m.(m\in w)\leftrightarrow {\big (}m=0\lor \exists (p\in w).Sp=m{\big )}}$

Without making use of the notation for the previously defined successor notation, the extensional equality to a successor ${\displaystyle Sp=m}$ is captured by ${\displaystyle \forall n.(n\in m)\leftrightarrow (n=p\lor n\in p)}$. This expresses that all elements ${\displaystyle m}$ are either equal to ${\displaystyle 0}$ or themselves hold a predecessor set ${\displaystyle p\in w}$ which shares all other members with ${\displaystyle m}$.

Observe that through the expression "${\displaystyle \exists (p\in w)}$" on the right hand side, the property characterizing ${\displaystyle w}$ by its members ${\displaystyle m}$ here syntactically again contains the symbol ${\displaystyle w}$ itself. Due to the bottom-up nature of the natural numbers, this is tame here. Assuming ${\displaystyle \Delta _{0}}$-set induction on top of ${\displaystyle {\mathsf {ECST}}}$, no two different sets have this property. Also note that there are also longer formulations of this property, avoiding "${\displaystyle \exists (p\in w)}$" in favor unbounded quantifiers.

Number bounds

Adopting an Axiom of Infinity, the set-bounded quantification legal in predicates used in ${\displaystyle \Delta _{0}}$-Separation then explicitly permits numerically unbounded quantifiers - the two meanings of "bounded" should not be confused. With ${\displaystyle \omega }$ at hand, call a class of numbers ${\displaystyle I\subset \omega }$ bounded if the following existence statement holds

${\displaystyle \exists (m\in \omega ).\forall (n\in \omega ).(n\in I\to n<m)}$

This is a statements of finiteness, also equivalently formulated via ${\displaystyle m\leq n\to n\notin I}$. Similarly, to reflect more closely the discussion of functions below, consider the above condition in the form ${\displaystyle \exists (m\in \omega ).\forall (n\in I).(n<m)}$. For decidable properties, these are ${\displaystyle \Sigma _{2}^{0}}$-statements in arithmetic, but with the Axiom of Infinity, the two quantifiers are set-bound.

For a class ${\displaystyle C}$, the logically positive unboundedness statement

${\displaystyle \forall (k\in \omega ).\exists (j\in \omega ).(k\leq j\land j\in C)}$

is now also one of infinitude. It is ${\displaystyle \Pi _{2}^{0}}$ 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 ${\displaystyle \omega }$.

Moderate induction in ECST

In the following, an initial segment of the natural numbers, i.e. ${\displaystyle \{n\in \omega \mid n<m\}}$ for any ${\displaystyle m\in \omega }$ and including the empty set, is denoted by ${\displaystyle \{0,1,\dots ,m-1\}}$. This set equals ${\displaystyle m}$ and so at this point "${\displaystyle m-1}$" 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 ${\displaystyle y}$ and let ${\displaystyle Q(n)}$ denote the existential statement that the function space on the finite ordinal into ${\displaystyle y}$ exist. The predicate will be denoted ${\displaystyle \exists h.h\simeq y^{\{0,1,\dots ,n-1\}}}$ 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 ${\displaystyle \forall (n\in \omega ).Q(n)}$ and, less formally, the equality ${\displaystyle \omega =\{n\in \omega \mid Q(n)\}}$ are just two ways of formulating the same desired statement, namely an ${\displaystyle n}$-indexed conjunction of existential propositions where ${\displaystyle n}$ 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 ${\displaystyle \forall (n\in \omega ).Q(n)}$ 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 ${\displaystyle \forall }$-statements.

The second universally quantified conjunct in the strong axiom of Infinity expresses mathematical induction for all ${\displaystyle y}$ in the universe of discourse, i.e. for sets. This is because the consequent of this clause, ${\displaystyle \omega \subset y}$, states that all ${\displaystyle n\in \omega }$ fulfill the associated predicate. Being able to use predicative separation to define subsets of ${\displaystyle \omega }$, the theory proves induction for all predicates ${\displaystyle \phi (n)}$ 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, ${\displaystyle {\mathsf {ECST}}}$ already validates induction with quantifiers over the naturals, and hence induction as in the first-order arithmetic theory ${\displaystyle {\mathsf {HA}}}$. The so called axiom of full mathematical induction for any predicate (i.e. class) expressed through set theory language is far stronger than the bounded induction principle valid in ${\displaystyle {\mathsf {ECST}}}$. 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 ${\displaystyle \forall }$ 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 ${\displaystyle {\mathsf {HA}}}$, one interprets these arithmetical formulas. In that context, the bounded quantification specifically means quantification over a finite range of numbers. One may also speak about the induction in the first-order but two-sorted theory of so-called second-order arithmetic ${\displaystyle {\mathsf {Z}}_{2}}$, 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 ${\displaystyle {\mathsf {Z}}_{2}}$ with very low complexity comprehension studied in that framework have a language that does not merely express arithmetical sets, while all sets of naturals particular such theories prove to exist are just computable sets. Theorems therein can be a relevant reference point for weak set theories with a set of naturals, predicative separation and only some further restricted form of induction. Constructive reverse mathematics exists as a field but is less developed than its classical counterpart. ${\displaystyle {\mathsf {Z}}_{2}}$ shall moreover not be confused with the second-order formulation of Peano arithmetic ${\displaystyle {\mathsf {PA}}_{2}}$. 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. Likewise, care must always be taken with insights about totality of functions. In computability theory, the μ operator enables all partial general recursive functions (or programs, in the sense that they are Turing computable), including ones e.g. non-primitive recursive but ${\displaystyle {\mathsf {PA}}}$-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 ${\displaystyle R}$ express a property such that a mathematical framework validates what amounts to the statement

${\displaystyle \forall (a\in A).\exists (c\in C).R(a,c)}$

A constructive proof calculus may validate such a judgement in terms of programs on represented domains and some object representing a concrete assignment ${\displaystyle a\mapsto c_{a}}$, providing a particular choice of value in ${\displaystyle C}$ (a unique one), for each input from ${\displaystyle A}$. Expressed through the rewriting ${\displaystyle \forall (a\in A).R(a,c_{a})}$, this function object may be understood as witnessing the proposition. Consider for example the notions of proof in through realizability theory or function terms in a type theory with a notion of quantifiers. The latter captures proof of logical proposition through programs via the Curry–Howard correspondence.

Depending on the context, the word "function" may be used in association with a particular model of computation, and this is a priori narrower than what is discussed in the present set theory context. One notion of program is formalized by partial recursive "functions" in computability theory. But beware that here the word "function" is used in a way that also comprises partial functions, and not just "total functions". The scare quotes are used for clarity here, as in a set theory context there is technically no need to speak of total functions, because this requirement is part of the definition of a set theoretical function and partial function spaces can be modeled via unions. At the same time, when combined with a formal arithmetic, partial function programs provides one particularly sharp notion of totality for functions. By Kleene's normal form theorem, each partial recursive function on the naturals computes, for the values where it terminates, the same as ${\displaystyle a\mapsto U(\mu w.T_{1}(e,a,w))}$, for some partial function program index ${\displaystyle e\in {\mathbb {N} }}$, and any index will constitute some partial function. A program can be associated with a ${\displaystyle e}$ and may be said to be ${\displaystyle T_{1}}$-total whenever a theory proves ${\displaystyle \forall a.\exists w.T_{1}(e,a,w)}$, where ${\displaystyle T_{1}}$ amounts to a primitive recursive program and ${\displaystyle w}$ is related to the execution of ${\displaystyle e}$. Kreisel proved that the class of partial recursive functions proven ${\displaystyle T_{1}}$-total by ${\displaystyle {\mathsf {HA}}}$ is not enriched when ${\displaystyle {\mathrm {PEM} }}$ is added. As a predicate in ${\displaystyle e}$, this totality constitutes an undecidable subset of indices, highlighting that the recursive world of functions between the naturals is already captured by a set dominated by ${\displaystyle {\mathbb {N} }}$. As a third warning, note that this notion is really about programs and several indices will in fact constitute the same function, in the extensional sense.

A theory in first-order logic, such as the axiomatic set theories discussed here, comes with a joint notion of total and functional for a binary predicate ${\displaystyle R}$, namely ${\displaystyle \forall a.\exists !c.R(a,c)}$. Such theories relate to programs only indirectly. If ${\displaystyle S}$ denotes the successor operation in a formal language of a theory being studied, then any number, e.g. ${\displaystyle {\mathrm {SSS0} }}$ (the number three), may metalogically be related to the standard numeral, e.g. ${\displaystyle {\underline {\mathrm {SSS0} }}=SSS0}$. 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 ${\displaystyle {\mathsf {PA}}}$, classical Robinson arithmetic ${\displaystyle {\mathsf {Q}}}$ 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 ${\displaystyle T_{1}}$-total recursive functions here, it is a meta-theorem that the language of arithmetic expresses them by ${\displaystyle \Sigma _{1}}$-predicates ${\displaystyle G}$ encoding their graph such that ${\displaystyle {\mathsf {Q}}}$ represents them, in the sense that it correctly proves or rejects ${\displaystyle G({\underline {\mathrm {a} }},{\underline {\mathrm {c} }})}$ for any input-output pair of numbers ${\displaystyle \mathrm {a} }$ and ${\displaystyle \mathrm {c} }$ in the meta-theory. Now given a correctly representing ${\displaystyle G}$, the predicate ${\displaystyle G_{\mathrm {least} }(a,c)}$ defined by ${\displaystyle G(a,c)\land \forall (n<c).\neg G(a,n)}$ 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 ${\displaystyle {\mathrm {a} }}$ in the sense of ${\displaystyle {\mathsf {Q}}\vdash \exists !c.G_{\mathrm {least} }({\underline {\mathrm {a} }},c)}$. Given a representing predicate, then at the cost of making use of ${\displaystyle {\mathrm {PEM} }}$, one can always also systematically (i.e. with a ${\displaystyle \forall a.}$) prove the graph to be total functional.

Which predicates are provably functional for various inputs, or even total functional on their domain, generally depends on the adopted axioms of a theory and proof calculus. For example, for the diagonal halting problem, which cannot have a ${\displaystyle T_{1}}$-total index, it is ${\displaystyle {\mathsf {HA}}}$-independent whether the corresponding graph predicate on ${\displaystyle {\mathbb {N} }\times \{0,1\}}$ (a decision problem) is total functional, but ${\displaystyle {\mathrm {PEM} }}$ implies that it is. Proof theoretical function hierarchies provide examples of predicates proven total functional in systems going beyond ${\displaystyle {\mathsf {PA}}}$. 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 ${\displaystyle \Sigma _{1}}$-sound.

Total functional relations

In set theory language here, speak of a function class when ${\displaystyle f\subset A\times C}$ and provenly

${\displaystyle \forall (a\in A).\,\exists !(c\in C).\langle a,c\rangle \in f}$.

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

By construction, any such function respects equality in the sense that ${\displaystyle (x=y)\to f(x)=f(y)}$, for any inputs from ${\displaystyle A}$. 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 setoids have been defined as well. A subset of a function is still a function and the function predicate may also be proven for enlarged chosen codomain sets. As noted, care must be taken with nomenclature "function", a word which sees use in most mathematical frameworks. When a function set itself is not tied to a particular codomain, then this set of pairs is also member of a function space with larger codomain. This do not happen when by the word one denotes the subset of pairs paired with a codomain set, i.e. a formalization in terms of ${\displaystyle (A\times C)\times \{C\}}$. 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 functions and their domains.

If both the domain ${\displaystyle A}$ and considered codomain ${\displaystyle C}$ 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 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-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 ${\displaystyle A\times C}$, i.e. the property is expressing not more or less than functionality w.r.t. the inputs from ${\displaystyle A}$. Now if the domain is a set, the function comprehension principle, also called 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 ${\displaystyle {\mathsf {CZF}}}$. 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 ${\displaystyle 1}$, 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 ${\displaystyle {\mathsf {BCST}}}$ that adding a function symbol for a provenly total class function is a conservative extension, despite this formally changing the scope of bounded Separation. In summary, in the set theory context the focus is on capturing particular total relations that are functional. To delineate the notion of function in the theories of the previous subsection (a 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 (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 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 ${\displaystyle {\mathsf {ETCS}}}$ 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 ${\displaystyle {\mathrm {PEM} }}$. More finiteness properties for a set ${\displaystyle X}$ 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 ${\displaystyle X}$. One definition considers some notion of non-injectivity into ${\displaystyle X}$. Other definitions consider functions to a fixed superset of ${\displaystyle X}$ 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 ${\displaystyle \omega }$ itself is clearly unbounded. In fact, for any surjection from a finite range onto ${\displaystyle \omega }$, 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 ${\displaystyle \omega }$, unlike any of its members, can be put in bijection with some of its proper unbounded subsets, e.g. those of the form ${\displaystyle w_{m}:=\{k\in \omega \mid k>m\}}$ for any ${\displaystyle m\in \omega }$. 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 ${\displaystyle \omega }$ into it. A set that is even in bijection with ${\displaystyle \omega }$ may be called countably infinite. A set is Tarski-infinite if there is a chain of ${\displaystyle \subset }$-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 ${\displaystyle {\mathsf {ZF}}}$ and that theory does not prove all non-finite sets to be infinite in the injection existence sense, albeit it there holds when further assuming countable choice. ${\displaystyle {\mathsf {ZF}}}$ 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).