Constructive set theory

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, motivated by results tied to impredicativity.

Introduction[edit]

Constructive outlook[edit]

Preliminary on the use of intuitionistic logic[edit]

The logic of the set theories discussed here is constructive in that it rejects the principle of excluded middle ${\displaystyle {\mathrm {PEM} }}$, i.e. that the disjunction ${\displaystyle \phi \lor \neg \phi }$ automatically holds for all propositions ${\displaystyle \phi }$. 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[edit]

Compared to the classical counterpart, one is generally less likely to prove the existence of relations that cannot be realized. A restriction to the constructive reading of existence apriori leads to stricter requirements regarding which characterizations of a set ${\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[edit]

With computably undecidable propositions already arising in Robinson arithmetic, even just Predicative separation lets one define elusive subsets easily. In stark contrast to the classical framework, constructive set theories may be closed under the rule that any property that is decidable for all sets is already equivalent to one of the two trivial ones, ${\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.^[1]

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 {OD} })}$, 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[edit]

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 ones 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[edit]

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}}}$.^[2][3] 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}}}$,^[4] 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, see also Lévy hierarchy. Boundedness can be handled as a syntactic property or, alternatively, the theories can be conservatively extended with a higher boundedness predicate and its axioms. Secondly, the impredicative Powerset axiom is discarded, generally in favor of related but weaker axioms. The strong form is very casually used in classical general topology. Adding ${\displaystyle {\mathrm {PEM} }}$ to a theory even weaker than ${\displaystyle {\mathsf {CZF}}}$ recovers ${\displaystyle {\mathsf {ZF}}}$, as detailed below.^[5] 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[edit]

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 but plus the existence of all transitive closures. (The latter is also implied after promoting Regularity to 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,^[6] 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.^[7][8] 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.^[9]

Notation[edit]

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 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[edit]

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. 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[edit]

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[edit]

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 below.

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 disjointness 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 below the proposition will furthermore be expressible as ${\displaystyle A\cap B=\{\}}$.

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}$. The similar 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. 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}$.

Extensional equivalence[edit]

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[edit]

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[edit]

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.

Extensionality ${\displaystyle \forall x.\forall y.\ \ x\simeq y\to x=y}$

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 Q}$ may be not decidable for all elements in ${\displaystyle B}$, the two classes 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 w=\{x\in w\mid Q(x)\}}$. This means that establishing such ${\displaystyle \forall }$-theorems, e.g. the ones provable from full mathematical induction, enables treating the subclass of ${\displaystyle w}$ on the right hand side of the equality to be used wherever ${\displaystyle w}$ is used.

Alternative approaches[edit]

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. Even then, the above definition can be used to characterize equality of subsets ${\displaystyle u\subset x}$ and ${\displaystyle v\subset x}$. Note that adopting "${\displaystyle =}$" as a symbol in a predicate logic theory makes equality of two terms a quantifier-free expression.

Merging sets[edit]

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,

Pairing ${\displaystyle \forall x.\forall y.\ \ \exists p.\{x,y\}\subset p}$

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,

Union ${\displaystyle \forall x.\ \ \exists u.\forall z.{\Big (}{\big (}\exists (y\in x).z\in y{\big )}\to z\in u{\Big )}}$

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[edit]

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

Axiom of empty set: ${\displaystyle \exists x.\forall y.\,\neg (y\in x)}$

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[edit]

The following makes use of axiom schemas, i.e. axioms for some collection of predicates. Some of the stated axiom schemas shall allow for any collection of set parameters as well (meaning any particular named variables ${\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[edit]

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

Axiom schema of predicative separation: For any bounded predicate ${\displaystyle \phi }$, with parameters and with set variable ${\displaystyle y}$ not free in it, ${\displaystyle \forall y.\,\exists s.\forall x.{\big (}x\in s\,\leftrightarrow \,(x\in y\land \phi (x)){\big )}}$

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 Bounded Separation schema is actually equivalent to Empty Set plus the existence of the binary intersection for any two sets. The latter variant of axiomatization does not make use of a formula schema.

For a proposition ${\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 also, equivalently, also ${\displaystyle \neg (0\in B)}$. In the model of the naturals, if ${\displaystyle B}$ is a number, ${\displaystyle 0\in B}$ 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 ${\displaystyle P\lor \neg P}$ 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. 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 ones 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 ${\displaystyle \forall b.(0\in b)\lor (0\notin b)}$.

The axiom schema of Predicative Separation is also called Bounded Separation, as in Separation for set-bounded quantifiers only. The scope of specified subsets that can be proven to exist is enriched with further set existence postulate. Bounded Separation is a schema that takes into account syntactic aspects of set defining predicates, up to provable equivalence. The permitted formulas are denoted by ${\displaystyle \Delta _{0}}$ in the set theoretical Lévy hierarchy, in analogy to ${\displaystyle \Delta _{0}^{0}}$ in the arithmetical hierarchy. (Note however that the arithmetic classification is sometimes expressed not syntactically but in terms of subclasses of the naturals. Also, the bottom level of the arithmetical hierarchy has several common definitions, some not allowing the use of some total functions. The distinction is not relevant on the level ${\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. See also Kripke-Platek set theory.

No universal set[edit]

By a remark in the section on merging sets, a set cannot consistently ruled out to be a member of a class of the form ${\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 on the right is not a set. The following demonstrates this in the special case when ${\displaystyle A}$ is empty, i.e. when the right side is the universal class.

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)}$ is a bounded one and 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 with the axiom of regularity, like ${\displaystyle {\mathsf {ZF}}}$, of course that subset ${\displaystyle \{x\in y\mid x\notin x\}}$ can be proven to be equal to ${\displaystyle y}$ itself. As an aside, in a theory with stratification like Intuitionistic New Foundations, a universal set may exist because use of the syntactic expression ${\displaystyle x\in x}$ may be disallowed in proofs of existence by, essentially, separation.

Already the special case ${\displaystyle s=y}$ implies that the subclass ${\displaystyle \{x\mid x\notin x\}}$ of the universal class is proper as well.

Predicativity[edit]

The restriction in the axiom is also gatekeeping impredicative definitions: Existence should at best not be claimed for objects that are not explicitly describable, or whose definition involves themselves or reference to a proper class, such as when a property to be checked involves a universal quantifier. So in a constructive theory without Axiom of power set, when ${\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 must be emphasized that many class definitions that are classically equivalent are not so when restricting oneself to constructive logic. So in this way, one gets a broader theory, constructively. Due to the potential undecidability of general predicates, the notion of subset and subclass is more elaborate in constructive set theories than in classical ones. This remains true if full Separation is adopted, as in the theory ${\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[edit]

Next consider the

Axiom schema of Replacement: For any predicate ${\displaystyle \phi }$ with set variable ${\displaystyle r}$ not free in it, ${\displaystyle \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 )}}$

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 discrete 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. Equality of elements inside a set ${\displaystyle x}$ is decidable if the corresponding relation as a subset of ${\displaystyle x\times x}$ is decidable, in which case ${\displaystyle x}$ is sometimes called discrete.

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.

Hereditarily finite sets[edit]

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: Union, Separation and Replacement are related to flattening, filtering and comprehension. 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.^[10][11] Such principles are relevant for the standard modeling of individual Neumann ordinals. 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[edit]

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 \exists z.(z\in A)\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

Strong Infinity ${\displaystyle \exists w.{\Big (}\mathrm {Ind} _{w}\,\land \,{\big (}\forall y.\mathrm {Ind} _{y}\to w\subset y{\big )}{\Big )}}$

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}$ 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 it 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 }$". It is important to note that the theory proves the order as well as the equality relation on this set to be decidable. Not only is no number smaller than ${\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 decidable 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[edit]

Should it need motivation, the handiness of postulating an unbounded set of numbers in relation to other inductive properties becomes clear in the discussion of arithmetic in set theory further below. But as is familiar from classical set theory, also weak forms of Infinity can be formulated. For example, one may just postulate the existence of some inductive set, ${\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[edit]

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