To install click the Add extension button. That's it.

The source code for the WIKI 2 extension is being checked by specialists of the Mozilla Foundation, Google, and Apple. You could also do it yourself at any point in time.

4,5
Kelly Slayton
Congratulations on this excellent venture… what a great idea!
Alexander Grigorievskiy
I use WIKI 2 every day and almost forgot how the original Wikipedia looks like.
Live Statistics
English Articles
Improved in 24 Hours
What we do. Every page goes through several hundred of perfecting techniques; in live mode. Quite the same Wikipedia. Just better.
.
Leo
Newton
Brights
Milds

# Constructive set theory

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 law of excluded middle (${\displaystyle {\mathrm {LEM} }}$), constructive set theories often require some logical quantifiers in their axioms to be bounded, motivated by results tied to impredicativity.

## Introduction

### Outlook

The logic of the set theories discussed here is constructive in that it rejects ${\displaystyle {\mathrm {LEM} }}$, i.e. that the disjunction ${\displaystyle \phi \lor \neg \phi }$ automatically holds for all propositions. This then requires rejection of strong choice principles and the rewording of some standard axioms. For example, the Axiom of Choice implies ${\displaystyle {\mathrm {LEM} }}$ for the formulas in one's adopted Separation schema, by Diaconescu's theorem. Similar results hold for the Axiom of Regularity in its standard form. As a rule, to prove a particular disjunction ${\displaystyle P\lor \neg P}$, either ${\displaystyle P}$ or ${\displaystyle \neg P}$ needs to be proven. In that case, ones says the disjunction is decidable. In turn, constructive theories tend to not permit many classical proofs of properties that are e.g. provably computationally undecidable. Unlike the more conservative minimal logic, here the underlying logic permits double negation elimination for decidable predicates and the theorem formulations regarding finite constructions tends to not differ from their classical counterparts.

Notably, a restriction to constructive logic 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 implying  total) function. This is often because the predicate in a case-wise would-be definition may not be decidable. Compared to the classical counterpart, one is generally less likely to prove the existence of relations that cannot be realized. This then also affects the provability of statements about total orders such as that of all ordinal numbers, expressed by truth and negation of the terms in the order defining disjunction ${\displaystyle (\alpha \in \beta )\lor (\alpha =\beta )\lor (\beta \in \alpha )}$. And this in turn affects the proof theoretic strength defined in ordinal analysis.

That said, constructive mathematical theories generally 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 ${\displaystyle {\mathrm {LEM} }}$ is assumed, are at once classically equivalent to the classical statement. The difference is that the constructive proofs are harder to find.

### On 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}}}$. As far as constructive realizations go there is a realizability theory and Aczel's theory constructive Zermelo-Fraenkel (${\displaystyle {\mathsf {CZF}}}$) has been interpreted in a  Martin-Löf type theories, as described below. In this way, set theory theorems provable in ${\displaystyle {\mathsf {CZF}}}$ and weaker theories are candidates for a computer realization. More recently, presheaf models for constructive set theories have been introduced. These are analogous to unpublished Presheaf models for intuitionistic set theory developed by Dana Scott in the 1980s.[1][2]

### Overview

The subject of constructive set theory (often "${\displaystyle {\mathsf {CST}}}$") begun by John Myhill's work on the theory also called ${\displaystyle {\mathsf {CST}}}$, a theory of several sorts and bounded quantification, aiming to provide a formal foundation for Errett Bishop's program of constructive mathematics. Below is a sequence of theories in the same language as ${\displaystyle {\mathsf {ZF}}}$, leading up to Peter Aczel's well studied ${\displaystyle {\mathsf {CZF}}}$,[3] 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 {LEM} }}$ 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 {LEM} }}$. 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 where even the Axiom of Collection is bounded.

## Subtheories of ZF

### Notation

#### Language

The propositional connective symbols are standard. The axioms of set theory give a means to prove equality "${\displaystyle =}$" of sets and the symbol may, by abuse of notation, be used for classes. Negation "${\displaystyle \neg }$" of elementhood "${\displaystyle \in }$" is often written "${\displaystyle \notin }$", and usually the same goes for non-equality ${\displaystyle \neq }$, although in constructive mathematics the latter symbol is also used in the context with apartness relations.

#### Variables

Below the greek ${\displaystyle \phi }$ denote a predicate variable in axiom schemas and use ${\displaystyle P}$ or ${\displaystyle Q}$ for particular predicates. The word formulas is often used interchangeably with predicate, even in the unary case.

Quantifiers range over set and those are denoted by lower case letters. As is common, one may use argument brackets to highlight particular free variables, as in "${\displaystyle P(z)}$". One abbreviates ${\displaystyle \forall z.(z\in A\implies P(z))}$ by ${\displaystyle \forall (z\in A).P(z)}$ and ${\displaystyle \exists z.(z\in A\land P(z))}$ by ${\displaystyle \exists (z\in A).P(z)}$. The syntactic notion of bounded quantification in this sense can play a role in the formulation of axiom schemes, as we shall see. Express the subclass claim ${\displaystyle \forall (z\in A).z\in B}$, i.e. ${\displaystyle \forall z.(z\in A\implies 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. Unique existence ${\displaystyle \exists !x.P(x)}$ e.g. means ${\displaystyle \exists x.\forall y.\left(y=x\iff P(y)\right)}$.

#### Classes

As is also common in the study of set theories, one makes use set builder notation for classes, which, in most contexts, are not part of the object language but used for concise discussion. In particular, one may introduce notation declarations of the corresponding class via "${\displaystyle A=\{z\mid P(z)\}}$", for the purpose of expressing ${\displaystyle P(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 P(z)\}}$ as shorthand for ${\displaystyle \{z\mid z\in B\land P(z)\}}$. For a property ${\displaystyle P}$, trivially ${\displaystyle \forall z.{\big (}(z\in B\land P(z))\implies z\in B{\big )}}$. And so follows that ${\displaystyle \{z\in B\mid P(z)\}\subset B}$.

### Common axioms

A starting point of ${\displaystyle {\mathsf {ZF}}}$ axioms that are virtually always deemed uncontroversial and part of all theories considered in this article.

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\iff z\in B)}$, or equivalently ${\displaystyle (A\subset B)\land (B\subset A)}$.

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

 ${\displaystyle \forall x.\forall y.\ \ x\simeq y\implies x=y}$

By the logical properties of equality, the converse direction 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 Q}$ may be not decidable for all elements in ${\displaystyle B}$, the two classes must a priori be distinguished.

Consider a property ${\displaystyle P}$ that provably holds for all elements of a set ${\displaystyle y}$, so that ${\displaystyle \{z\in y\mid P(z)\}\simeq y}$, and assume that the class on the left hand side is established to be a set. Note that, even if this set on the left informally also ties to proof-relevant information about the validity of ${\displaystyle P}$ for all the elements, the Extensionality axiom postulates that, in our set theory, the set on the left hand side is judged equal to the one on the right hand side.

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

Two other basic axioms as follows. Firstly,

 ${\displaystyle \forall x.\forall y.\ \ \exists p.\forall z.{\big (}(z=x\lor z=y)\implies z\in p{\big )}}$

saying 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 (${\displaystyle z}$).

And then,

 ${\displaystyle \forall x.\ \ \exists u.\forall y.{\big (}(\exists z.y\in z\land z\in x)\implies y\in u{\big )}}$

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

The two axioms may also be formulated stronger in terms of "${\displaystyle \iff }$", e.g. in the context of ${\displaystyle {\mathsf {BCST}}}$ with Separation, this is not necessary.

Together, these two axioms imply the existence of the binary union of two classes ${\displaystyle a}$ and ${\displaystyle b}$ when they have been established to be sets, and this is denoted ${\displaystyle \bigcup \{a,b\}}$ or ${\displaystyle a\cup b}$. Define class notation for finite elements via disjunctions, e.g., ${\displaystyle c\in \{a,b\}}$ says ${\displaystyle (c=a)\lor (c=b)}$, and define the successor set ${\displaystyle Sx}$ as ${\displaystyle x\cup \{x\}}$. A sort of blend between pairing and union, an axiom more readily related to the successor is the Axiom of adjunction. It is relevant for the standard modeling of individual Neumann ordinals. This axiom would also readily be accepted, but is not relevant in the context of stronger axioms below. Denote by ${\displaystyle \langle x,y\rangle }$ the standard ordered pair model ${\displaystyle \{\{x\},\{x,y\}\}}$.

The property that is false for any set corresponds to the empty class, denoted by ${\displaystyle \{\}}$ or zero, 0. That this is a set readily follows from other axioms, such as the Axiom of Infinity below. But if, e.g., one is explicitly interested in excluding infinite sets in one's study, one may at this point adopt the Axiom of empty set

${\displaystyle \exists x.\forall y.\,\neg (y\in x)}$

### BCST

The following makes use of axiom schemas, i.e. axioms for some collection of predicates. Note that some of the stated axiom schemas are often presented with set parameters ${\displaystyle v}$ as well, i.e. variants with extra universal closures ${\displaystyle \forall v}$ such that the ${\displaystyle \phi }$'s may depend on the parameters.

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 three axioms above, it adopts the

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

The 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)\}}$. When the predicate is taken as ${\displaystyle x\in z}$ for ${\displaystyle z}$ proven to be a set, one obtains the binary intersection of sets and writes ${\displaystyle s=y\cap z}$.

The schema is also called Bounded Separation, as in Separation for set-bounded quantifiers only. It is the axiom schema that makes reference to syntactic aspects of predicates. The bounded formulas are also 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 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.) 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 whos definition involves themselves or reference to a proper class, such as when a property to be checked involves an universal quantifier. So in a constructive theory without Axiom of power set, when ${\displaystyle Q}$ denotes some 2-ary predicate, one should not expect a class ${\displaystyle s}$ defined as

${\displaystyle \{x\in y\mid \forall (t\in {\mathcal {P}}y).Q(x,t)\}}$

i.e.

${\displaystyle \{x\in y\mid \forall t.{\big (}\forall (z\in t).(z\in y)\implies Q(x,t){\big )}\}}$

to be a set. Note that if this subclass ${\displaystyle s}$ is provably a set, then this ${\displaystyle s}$ defined here is also in the unbounded scope of set variable ${\displaystyle t}$. As ${\displaystyle s}$ fulfills the subset property ${\displaystyle \forall (z\in s).(z\in y)}$, the expression ${\displaystyle Q(x,s)}$ 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 bottom-up view of constructive sets and a type theoretical interpretation. 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.

As noted, from Separation and the existence of any set (e.g. Infinity below) and the predicate that is false of any set, like ${\displaystyle \neg (x=x)}$, will follow the existence of the empty set.

By virtue of the purely logical theorem ${\displaystyle \forall x.{\big (}xRs\Leftrightarrow (xRy\land \neg xRx){\big )}\implies \neg sRy}$, Russel's construction shows that Predicative Separation alone implies that ${\displaystyle \{x\in y\mid x\notin x\}\notin y}$. In particular, no universal set exists.

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

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)\implies \exists r.\forall y.{\big (}y\in r\iff \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, even if of course weaker schemas could be considered.

With the Replacement schema, this theory proves that the equivalence classes or indexed sums are sets. In particular, the Cartesian product, holding all pairs of elements of two sets, is a set.

Replacement and the axiom of Set Induction (introduced below) suffices to axiomize hereditarily finite sets constructively and that theory is also studied without Infinity. For comparison, consider the very weak classical theory called General set theory that interprets the class of natural numbers and their arithmetic via just Extensionality, Adjunction and full Separation.

Replacement can be seen as a form of comprehension. Only when assuming ${\displaystyle {\mathrm {LEM} }}$ 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. The discussion precedes with axioms granting existence of objects also found in dependent type theory, namely natural numbers and products.

### ECST

Denote by ${\displaystyle \mathrm {Ind} (A)}$ the Inductive property, e.g. ${\displaystyle 0\in A\land \forall (n\in A).Sn\in A}$. In terms of a predicate ${\displaystyle P}$ underling the class, this would be translated as ${\displaystyle P(0)\land \forall n.{\big (}P(n)\implies P(Sn){\big )}}$. Here ${\displaystyle n}$ denotes a generic set variable. Write ${\displaystyle \bigcap A}$ for ${\displaystyle \{x\mid \forall y.(y\in A\implies x\in y)\}}$. Define a class ${\displaystyle \omega =\bigcap \{x\mid \mathrm {Ind} (x)\}}$.

For some fixed predicate ${\displaystyle P}$, the statement ${\displaystyle P(a)\land \forall x.P(x)\implies a\subset x}$ expresses that ${\displaystyle a}$ is the smallest set among all sets ${\displaystyle x}$ for which ${\displaystyle P(x)}$ holds true. The elementary constructive Set Theory ${\displaystyle {\mathsf {ECST}}}$ has the axiom of ${\displaystyle {\mathsf {BCST}}}$ as well as

 ${\displaystyle \exists w.{\Big (}\mathrm {Ind} (w)\,\land \,{\big (}\forall x.\mathrm {Ind} (x)\implies w\subset x{\big )}{\Big )}}$

With this, ${\displaystyle \omega }$ is a uniquely characterized set, the smallest infinite von Neumann ordinal. The second universally quantified conjunct expresses mathematical induction for all ${\displaystyle x}$ in the universe of discourse, i.e. for sets, resp. for predicates if they indeed define sets ${\displaystyle x}$. In this way, the principles discussed in this section give means of proving that some predicates hold at least for all elements of ${\displaystyle \omega }$. Be aware that even the quite strong axiom of full mathematical induction (induction for any predicate, discussed below) may also be adopted and used without ever postulating that ${\displaystyle \omega }$ forms a set. Full induction also follows from full Separation as well as from full Set induction.

Weak forms of axioms of infinity can be formulated, all postulating that some set with the common natural number properties exist. Then full Separation may be used to obtain the "sparse" such set, the set of natural numbers. In the context of otherwise weaker axiom systems, an axiom of infinity should be strengthened so as to imply existence of such a sparse set on its own. One weaker form of Infinity reads

${\displaystyle \exists w.\forall m.{\Big (}m\in w\iff {\big (}m=0\lor (\exists n\in w).\forall k.(k\in m\iff k\in n\lor k=n){\big )}{\Big )}}$

which can also be written more concisely using ${\displaystyle S}$. For elements ${\displaystyle n,m}$ of this set, the claim ${\displaystyle n=m}$ is decidable.

With this, ${\displaystyle {\mathsf {ECST}}}$ proves induction for all predicates given by bounded formulas. The two of the five Peano axioms regarding zero and one regarding closedness of ${\displaystyle S}$ with respect to ${\displaystyle \omega }$ follow fairly directly from the axioms of infinity. Finally, ${\displaystyle S}$ can be proven to be an injective operation.

Natural numbers are distinguishable, meaning equality (and thus inequality) of them is decidable. The basic order is captured by membership in this model. For the sake of standard notation, let ${\displaystyle \{0,1,\dots ,n-1\}}$ denote an initial segment of the natural numbers, ${\displaystyle \{k\in \omega \mid k for any ${\displaystyle k\in \omega }$, including the empty set.

To be finite means there is a bijective function to a natural. To be subfinite means to be a subset of a finite set. The claim that being a finite set is equivalent to being subfinite is equivalent to ${\displaystyle {\mathrm {LEM} }}$.

### Functions

#### Totality

Naturally, the logical meaning of existence claims is a topic of interest in intuitionistic logic. Here the focus is on total relations.

The proof calculus, in a constructive mathematical framework, of statements such as

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

might be set up in terms of programs on represented domains and possibly having to witness the claim. This is to be understood in the sense of, informally speaking, ${\displaystyle \forall (a\in A).P(a,c_{a})}$, where ${\displaystyle c_{a}}$ denotes the value of a program as mentioned, but this gets into questions of  realizability theory. For a stronger context, if ${\displaystyle A=C=\omega }$ and when the proposition holds, then demanding that this shall always be possible with a ${\displaystyle a\mapsto c_{a}}$ realized by some  total recursive function is a possible  Church's thesis postulate adopted in, consequently, strictly non-classical  Russian constructivism. In the previous paragraph, "function" needs to be understood in the computable sense of recursion theory - this occasional ambiguity must also be watched out for below.

Relatedly, consider Robinson arithmetic, which is a classical arithmetic theory that substitutes the full mathematical induction schema for a predecessor number existence claim. It is a theorem that that theory represents exactly the recursive functions in the sense of defining predicates ${\displaystyle P}$ that are provably a total functional relations,

${\displaystyle \forall (a\in {\mathbb {N} }).\exists !(c\in {\mathbb {N} }).P(a,c)}$.

Now in the current set theoretical approach, wdefine the property involving the function application brackets, ${\displaystyle f(a)=c}$, as ${\displaystyle \langle a,c\rangle \in f}$ and speak of a function ${\displaystyle f\subset A\times C}$ when provably

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

i.e.

${\displaystyle \forall (a\in A).\,\exists (c\in C).\,\forall (c'\in C).{\big (}c'=c\iff \langle a,c'\rangle \in f{\big )}}$,

which notably involves quantifier explicitly asking for existence. Whether a subclass can be judged to be a function will depend on the strength of the theory, which is to say the axioms one adopts. Notably, a general class could fulfill the above 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. inputs from ${\displaystyle A}$. If the domain is a set, then a set function exists. The axiom scheme of Replacement can also be formulated in terms of the ranges of such set functions. If domain and codomain are sets, then the above predicate only involves bounded quantifiers. Common notions such as injectivity and surjectivity can be expressed in a bounded fashion as well.

It is a metatheorem for theories containing ${\displaystyle {\mathsf {BCST}}}$ that adding a function symbol for a provably total class function is a conservative extension, despite this changing the scope of bounded Separation.

Let ${\displaystyle C^{A}}$ (also written ${\displaystyle ^{A}C}$) denote the class of set functions. When functions are understood as just function graphs as above, the membership proposition ${\displaystyle f\in C^{A}}$ is also written ${\displaystyle f\colon A\to C}$. Below might write ${\displaystyle x\to y}$ for ${\displaystyle y^{x}}$ for the sake of distinguishing it from ordinal exponentiation.

Separation lets use cut out subsets of products ${\displaystyle A\times C}$, at least when they are described in a bounded fashion. Write ${\displaystyle 1}$ for ${\displaystyle S0}$. Given any ${\displaystyle B\subset A}$, one is now led to reason about classes such as

${\displaystyle \{\langle x,y\rangle \in A\times \{0,1\}\mid (x\in B\land y=1)\lor (\neg (x\in B)\land y=0)\}.}$

The boolean-valued characteristic functions ${\displaystyle \chi _{B}\colon A\to \{0,1\}}$ are among such classes. But be aware that ${\displaystyle a\in B}$ may in generally not be decidable. That is to say, in absence of any non-constructive axioms, the disjunction ${\displaystyle a\in B\lor a\notin B}$ may not be provable, since one requires an explicit proof of either disjunct. When

${\displaystyle \exists (y_{a}\in \{0,1\}).f(a)=y_{a}}$

cannot be witnessed for all ${\displaystyle a\in A}$, or uniqueness of a term ${\displaystyle y_{a}}$ not be proven, then one cant constructively judge the comprehended collection to be functional.

Variants of the functional predicate definition using apartness relations on setoids have been defined as well. A function will be a set if its range is. Care must be taken with nomenclature "function", which use in most mathematical frameworks, also because some tie a function term itself to a particular codomain.

#### Computable sets

Given Infinity and any propositions ${\displaystyle Q}$, let ${\displaystyle I=\{k\in \omega \mid Q(k)\}}$. Given any natural ${\displaystyle n\in \omega }$, then

${\displaystyle Q(n)\lor \neg Q(n)\implies n\in I\lor n\notin I}$.

In classical set theory, ${\displaystyle Q}$ decidable just by ${\displaystyle {\mathrm {LEM} }}$, so is subclass membership. If the class ${\displaystyle I}$ is not finite, successively "listing" all numbers in ${\displaystyle I}$ by simply skipping those with ${\displaystyle n\notin I}$ classically constitutes an increasing surjective sequence ${\displaystyle a:\omega \twoheadrightarrow I}$. There, one can obtain a bijective function. In this way, the classical class of functions is provably rich, as it also contains objects that are beyond what we know to be effectively computable, or programmatically listable in praxis.

In computability theory, the computable sets are ranges of non-decreasing total functions in the recursive sense, at the level ${\displaystyle \Sigma _{1}^{0}\cap \Pi _{1}^{0}=\Delta _{1}^{0}}$ of the arithmetical hierarchy, and not higher. Deciding a predicate at that level amounts to solving the task of eventually finding a certificate that either validates or rejects membership. As not every predicate ${\displaystyle Q}$ is computably decidable, the theory ${\displaystyle {\mathsf {CZF}}}$ alone will not claim (prove) that all infinite ${\displaystyle I\subset \omega }$ are the range of some bijective function with domain ${\displaystyle \omega }$.

But being compatible with ${\displaystyle {\mathsf {ZF}}}$, the development in this section still always permits "function on ${\displaystyle \omega }$" to be interpreted as an object not necessarily given as  lawlike sequence. Applications may be found in the common models for claims about probability, e.g. statements involving the notion of "being given" an unending random sequence of coin flips.

#### Choice

The constructive development here proceeds in a fashion agnostic to any discussed choice principles, but here are well studied variants:

• Axiom of countable choice: If ${\displaystyle g\colon \omega \to z}$, one can form the one-to-many relation-set ${\displaystyle \{\langle n,u\rangle \mid n\in \omega \land u\in g(n)\}}$. The axiom of countable choice would grant that whenever ${\displaystyle \forall (n\in \omega ).\exists u.u\in g(n)}$, one can form a function mapping each number to a unique value. Countable choice can also be weakened further, e.g. by restricting the possible cardinalities of the sets in the range of ${\displaystyle g}$, or by restricting the involved definition w.r.t. their place in the syntactic hierarchies.
• Relativized dependent choice: The stronger relativized dependent choice principle is a variant of it - a schema involving an extra predicate variable. Adopting this for just bounded formulas in ${\displaystyle {\mathsf {ECST}}}$, the theory already proves the ${\displaystyle \Sigma _{1}^{0}}$-induction, further discussed below.
• ${\displaystyle \Pi \Sigma }$-${\displaystyle AC}$: A family of sets is better controllable if it comes indexed by a function. A set ${\displaystyle B}$ is a base if all indexed families of sets ${\displaystyle i_{S}\colon B\to S}$ over it, have a choice function ${\displaystyle f_{S}}$, i.e. ${\displaystyle \forall (x\in B).f_{S}(x)\in i_{S}(x)}$. A collection of sets holding ${\displaystyle \omega }$ and its elements and which is closed by taking indexed sums and products (see dependent type) is called ${\displaystyle \Pi \Sigma }$-closed. While the axiom that all sets in the smallest ${\displaystyle \Pi \Sigma }$-closed class are a base does need some work to formulate, it is the strongest principle over ${\displaystyle {\mathsf {CZF}}}$ that holds in the type theoretical interpretation ${\displaystyle {\mathsf {ML_{1}V}}}$.
• Axiom of choice: The axiom of choice concerning functions on general sets of sets. It implies Dependent choice.

To highlight the strength of full Choice and its relation to matters of Intentionality, one should consider the subfinite classes

${\displaystyle x=\{u\in \{0,1\}\mid u=0\lor (u=1\land P)\}}$
${\displaystyle y=\{u\in \{0,1\}\mid u=1\lor (u=0\land P)\}}$

Here ${\displaystyle x}$ and ${\displaystyle y}$ are as contingent as the predicates involved in their definition. Now assume a context in which they are established to be sets, so that ${\displaystyle \{x,y\}}$ is as well. Here, Axiom of Choice would then grant existence of a map ${\displaystyle f\colon \{x,y\}\to \{0,1\}}$ with ${\displaystyle f(z)\in z}$ into distinguishable elements. This now actually implies that ${\displaystyle P\lor \neg P}$. So the existence claim of general choice functions is non-constructive. To better understand this phenomenon, one must consider cases of logical implications, such as ${\displaystyle P\implies x=y}$, et cetera. The difference between the discrete codomain of some natural numbers and the domain ${\displaystyle \{x,y\}}$ lies in the fact that a priori little is known about the latter. It is the case that ${\displaystyle 0\in x}$ and ${\displaystyle 1\in y}$, regardless of ${\displaystyle P}$, possibly making ${\displaystyle \{\langle x,0\rangle ,\langle y,1\rangle \}}$ a contender for a choice function. But in the case of ${\displaystyle x=y}$, as implied by provability of ${\displaystyle P}$, one has ${\displaystyle \{x,y\}=\{x\}}$ so that there is extensionally only one possible function input to a choice choice function, now with just ${\displaystyle \{x\}\to \{0,1\}}$, choice functions could be ${\displaystyle \{\langle x,0\rangle \}}$ or ${\displaystyle \{\langle x,1\rangle \}}$. So when considering the functional assignment ${\displaystyle f(x)=0}$, then unconditionally declaring ${\displaystyle f(y)=1}$ would not be consistent. Choice may be not adopted in an otherwise strong set theory, because the mere claim of function existence does not realize a particular function. Subclass comprehension (used to separate ${\displaystyle x}$ and ${\displaystyle y}$ from ${\displaystyle \{0,1\}}$, i.e. define them) ties predicates involved therein to set equality, in the described way, and this relates to information about functions.

#### Arithmetic

The assumptions necessary to obtain a theory of arithmetic are thoroughly studied in proof theory. For context, here a paragraph on the classifications therein: The classical theories starting with bounded arithmetic adopt different conservative induction schemata and may adds symbols for particular functions, leading to theories between Robinson- and Peano arithmetic ${\displaystyle {\mathsf {PA}}}$. Most of such theories are however relatively weak regarding proof of totality for some more fast growing functions. Some of the most basic examples include elementary function arithmetic ${\displaystyle {\mathsf {EFA}}}$, which includes the already established induction for bounded formulas, and with a proof theoretic ordinal (the least not provably recursive well-ordering) of ${\displaystyle \omega ^{3}}$. ${\displaystyle {\mathsf {PA}}}$ has full mathematical induction and ordinal ${\displaystyle \varepsilon _{0}}$, meaning the theory lets one encode ordinals of weaker (in this ordinal analysis sense) theories (say ${\displaystyle \langle \omega ^{3},\in \rangle }$, in set theory terms) as recursive relation on just the naturals, ${\displaystyle \langle \omega ,E\rangle }$. The ${\displaystyle \Sigma _{1}^{0}}$-induction schema, as e.g. implied by the relativized dependent choice, means induction for those subclasses of naturals computable via a finite search with unbound (finite) runtime. The schema is also equivalent to ${\displaystyle \Pi _{1}^{0}}$-induction schema. The relatively weak classical first-order arithmetic which adopts that schema is denoted ${\displaystyle {\mathsf {I\Sigma }}_{1}}$. The ${\displaystyle \Sigma _{1}^{0}}$-induction is also adopted the second-order reverse mathematics base system ${\displaystyle {\mathsf {RCA}}_{0}}$. That second-order theory is ${\displaystyle \Pi _{2}^{0}}$-conservative over primitive recursive arithmetic ${\displaystyle {\mathsf {PRA}}}$, so proves all primitive recursive functions total. Those last mentioned arithmetic theories all have ordinal ${\displaystyle \omega ^{\omega }}$. The higher-order arithmetic is a relevant reference point this discussion insofar as its language does not merely express arithmetical sets, while all sets of naturals the theory proves to exist are just computable sets. In this classical context, lack of full induction means that some versions of the pigeon hole principle are unprovable, e.g. one of the weakest ones being the claim that for a coloring ${\displaystyle f\colon \omega \to \{0,\dots ,n\}}$, there exists a ${\displaystyle k}$ and an infinite set ${\displaystyle I_{k}\subset \omega }$ such that ${\displaystyle \forall (n\in I_{k}).f(n)=k}$.

That all said, the set theory ${\displaystyle {\mathsf {ECST}}}$ does actually not even interpret full primitive recursion. Indeed, despite having the Replacement axiom, the theory does not proof the addition function to be a set function. On the other hand, many statements can be proven per individual set in this theory (as opposed to expressions involving a universal quantifier, as e.g. available with an induction principle) and objects of mathematical interest can be made use of at the class level on an individual basis. As such, the axioms listed so far suffice as basic working theory for a good portion of basic mathematics. Going beyond ${\displaystyle {\mathsf {ECST}}}$ with regards to arithmetic, the axiom granting definition of set functions via iteration-step set functions must be added. What is necessary is the set theoretical equivalent of a natural numbers object. This then enables an interpretation of Heyting arithmetic, ${\displaystyle {\mathsf {HA}}}$. With this, arithmetic of rational numbers ${\displaystyle {\mathbb {Q} }}$ can then also be defined and its properties, like uniqueness and countability, be proven. A set theory with this will also prove that, for any naturals ${\displaystyle n}$ and ${\displaystyle m}$, the function spaces

${\displaystyle {\{0,1,\dots ,n-1\}}\to {\{0,1,\dots ,m-1\}}}$

are sets.

Conversely, a proof of the seeked iteration principle may be based on the collection of functions one would want to write as ${\displaystyle \cup _{n\in \omega }y^{\{0,1,\dots ,n-1\}}}$ and the existence of this is implied by assuming that the individual function spaces on finite domains into sets ${\displaystyle y}$ form sets themselves. This remark should motivate the adoption of an axiom of more set theoretical flavor, instead of just directly embedding arithmetic principles into our theory. The iteration principle obtained through the next, more set theoretical axiom will, however, still not prove the full mathematical induction schema.

### Exponentiation

A weakened form of the Separation schema was already adopted, and more of the standard ${\displaystyle {\mathsf {ZF}}}$ axioms shall be weakened for a more predicative and constructive theory. The first one of those is the Powerset axiom, which is adopted in the form of the space of characteristic functions, itself tied to exactly the decidable subclasses.

The characterization of the class ${\displaystyle {\mathcal {P}}x}$ of all subsets of a set ${\displaystyle x}$ involves unbounded universal quantification, namely ${\displaystyle \forall u.u\subset x\iff u\in {\mathcal {P}}x}$. Here ${\displaystyle \subset }$ has been defined in terms of the membership predicate ${\displaystyle \in }$ above. The statement ${\displaystyle y={\mathcal {P}}x}$ itself is ${\displaystyle \Pi _{1}}$. So in a mathematical set theory framework, the power class is defined not in a bottom-up construction from its constituents (like an algorithm on a list, that e.g. maps ${\displaystyle \langle a,b\rangle \mapsto \langle \langle \rangle ,\langle a\rangle ,\langle b\rangle ,\langle a,b\rangle \rangle }$) but via a comprehension over all sets.

The richness of the powerclass in a theory without excluded middle can best be understood by considering small classically finite sets. For any formula ${\displaystyle P}$, the class ${\displaystyle \{x\mid (x=0)\land P\}}$ equals 0 when ${\displaystyle P}$ can be rejected and 1 when ${\displaystyle P}$ can be proven, but ${\displaystyle P}$ may also not be decidable at all. In this view, the powerclass of the singleton ${\displaystyle \{0\}=1}$, i.e. the class ${\displaystyle {\mathcal {P}}1}$, or suggestively "${\displaystyle \{0,\dots ,1\}}$", and usually denoted by ${\displaystyle \Omega }$, is called the truth value algebra. The ${\displaystyle \{0,1\}}$-valued functions on a set ${\displaystyle x}$ inject into ${\displaystyle {{\mathcal {P}}1}^{x}}$ and thus correspond to just its decidable subsets.

So next consider the axiom ${\displaystyle {\mathrm {Exp} }}$.

 Exponentiation ${\displaystyle \forall x.\forall y.\ \ \exists h.\forall f.{\big (}f\in h\iff f\in y^{x}{\big )}}$

The formulation here uses the convenient notation for function spaces. Otherwise the axiom is lengthier, characterizing ${\displaystyle h}$ using bounded quantifiers in the total function predicate. In words, the axiom says that given two sets ${\displaystyle x,y}$, the class ${\displaystyle y^{x}}$ of all functions is, in fact, also a set. This is certainly required, for example, to formalize the object map of an internal hom-functor like ${\displaystyle {\mathrm {hom} }({\mathbb {N} },-)}$.

Adopting it, quantification ${\displaystyle \forall f}$ over the elements of certain classes of functions only ranges over a set, also when such function spaces are even classically uncountable. E.g. the collection of all functions ${\displaystyle f\colon \omega \to 2}$ where ${\displaystyle 2=\{0,1\}}$, i.e. the set ${\displaystyle 2^{\mathbb {N} }}$ of points underlying the Cantor space, is uncountable, by Cantor's diagonal argument, and can at best be taken to be a subcountable set. (In this section we start to use the symbol for the semiring of natural numbers in expressions like ${\displaystyle y^{\mathbb {N} }}$ or write ${\displaystyle \omega \to y}$ just to avoid conflation of cardinal- with ordinal exponentiation.)

Existence statements like Exponentiation, i.e. function spaces being sets, enable the derivation of more sets via bounded Separation. The dependent or indexed products ${\displaystyle \Pi _{i\in x}\,y_{i}}$ are now sets. The set theory then also proves the existence of any primitive recursive function on the naturals ${\displaystyle \omega }$, as set functions in the set ${\displaystyle \omega \to \omega }$. Relatedly, obtain the  ordinal-exponentiated number ${\displaystyle \omega ^{\omega }}$, which may be characterized as ${\displaystyle \bigcup _{n\in \omega }\omega ^{n}}$. Spoken more generally, Exponentiation proves the union of all finite sequences over a countable set to be a countable set. And indeed, unions of the ranges of any countable family of counting functions is countable.

As far as comprehension goes, the theory now proves the collection of all the countable subsets of any set (the collection is a subclass of the powerclass) to be a set. Also enumerable forms of the pigeon hole principle can be proven.

In general, one has

${\displaystyle {\big (}\forall (x\subset 1).(0\notin x\lor 0\in x){\big )}\implies {\mathcal {P}}1\subset \{0,1\}}$.

So assuming ${\displaystyle {\mathrm {LEM} }}$ for just bounded formulas, predicative Separation lets one demonstrate that the powerclass ${\displaystyle {\mathcal {P}}1}$ is a set. With exponentiation, ${\displaystyle {\mathcal {P}}1}$ being a set already implies Powerset for sets in general. So in this context, also full Choice proves Powerset. With bounded excluded middle, ${\displaystyle {\mathcal {P}}z}$ is then in bijection with ${\displaystyle 2^{z}}$. See also ${\displaystyle {\mathsf {IZF}}}$.

Full Separation is equivalent to just assuming that each individual subclass of ${\displaystyle 1}$ is a set. Assuming full Separation, both full Choice and Regularity prove ${\displaystyle {\mathrm {LEM} }}$. Assuming ${\displaystyle {\mathrm {LEM} }}$, Replacement proves full Separation and Set induction is equivalent to Regularity.

#### Metalogic

While the theory ${\displaystyle {\mathsf {ECST}}+{\mathrm {Exp} }}$ does not exceed the consistency strength of Heyting arithmetic, adding Excluded Middle gives a theory proving the same theorems as classical ${\displaystyle {\mathsf {ZF}}}$ minus Regularity! Thus, adding Regularity as well as either ${\displaystyle {\mathrm {LEM} }}$ or full Separation to ${\displaystyle {\mathsf {ECST}}+{\mathrm {Exp} }}$ gives full classical ${\displaystyle {\mathsf {ZF}}}$. Adding full Choice and full Separation gives ${\displaystyle {\mathsf {ZFC}}}$ minus Regularity.

So this would thus lead to a theory beyond the strength of typical type theory.

#### Category and type theoretic notions

So in this context with Exponentiation, function spaces are more accessible than classes of subsets, as is the case with exponential objects resp. subobjects in category theory. In category theoretical terms, the theory ${\displaystyle {\mathsf {BCST}}+{\mathrm {Exp} }}$ essentially corresponds to constructively well-pointed Cartesian closed Heyting pretoposes with (whenever Infinity is adopted) a natural numbers object. Existence of powerset is what would turn a Heyting pretopos into an elementary topos. Every such topos that interprets ${\displaystyle {\mathsf {ZF}}}$ is of course a model of these weaker theories, but locally Cartesian closed pretoposes have been defined that e.g. interpret theories with Exponentiation but reject full Separation and Powerset.

In type theory, the expression "${\displaystyle x\to y}$" exists on its own and denotes function spaces, a primitive notion. These types (or, in set theory, classes or sets) naturally appear, for example, as the type of the currying bijection between ${\displaystyle (z\times x)\to y}$ and ${\displaystyle z\to y^{x}}$, an adjunction. A typical type theory with general programming capability - and certainly those that can model ${\displaystyle {\mathsf {CZF}}}$, which is considered a constructive set theory - will have a type of integers and function spaces representing ${\displaystyle {\mathbb {Z} }\to {\mathbb {Z} }}$, and as such also include types that are not countable. This just implies and means that among the function terms ${\displaystyle f\colon {\mathbb {Z} }\to ({\mathbb {Z} }\to {\mathbb {Z} })}$, none have the property of being a bijection.

Constructive set theories are also studied in the context of applicative axioms.

### Analysis

In this section the strength of ${\displaystyle {\mathsf {ECST}}+{\mathrm {Exp} }}$ is elaborated one. For context, possible further principles are mentioned, which are not necessarily classical and also not generally considered constructive. Here a general warning is in order: When reading proposition equivalence claims in the computable context, one shall always be aware which choice, induction and comprehension principles are silently assumed. See also the related Constructive analysis and Computable analysis.

#### Towards the reals

Exponentiation implies recursion principles and so in ${\displaystyle {\mathsf {ECST}}+{\mathrm {Exp} }}$, one can reason about sequences ${\displaystyle \omega \to {\mathbb {Q} }}$ or about shrinking intervals in ${\displaystyle \omega \to ({\mathbb {Q} }\times {\mathbb {Q} })}$ and this also enables speaking of Cauchy sequences and their arithmetic. Any Cauchy real number is a collection of sequences, i.e. subset of a set of functions on ${\displaystyle \omega }$. More axioms are required to always grant completeness of equivalence classes of such sequences and strong principles need to be postulated to imply the existence of a modulus of convergence for all Cauchy sequences. Weak countable choice is generally the context for proving uniqueness of the Cauchy reals as complete (pseudo-)ordered field. "Pseudo-" here highlights that the order will, in any case, constructively not always be decidable.

As in the classical theory, Dedekind cuts are characterized using subsets of algebraic structures such as ${\displaystyle {\mathbb {Q} }}$: The properties of being inhabited, numerically bounded above, "closed downwards" and "open upwards" are all bounded formulas with respect to the given set underlying the algebraic structure. A standard example of a cut, the first component indeed exhibiting these properties, is the representation of ${\displaystyle {\sqrt {2}}}$ given by

${\displaystyle {\big \langle }\{x\in {\mathbb {Q} }\mid x<0\lor x^{2}<2\},\,\{x\in {\mathbb {Q} }\mid 0

(Depending on the convention for cuts, either of the two parts or neither, like here, may makes use of the sign ${\displaystyle \leq }$.)

The theory given by the axioms so far validates that a pseudo-ordered field that is also Archimedean and Dedekind complete, if it exists at all, is in this way characterized uniquely, up to isomorphism. However, the existence of just function spaces such as ${\displaystyle \{0,1\}^{\mathbb {Q} }}$ does not grant ${\displaystyle {{\mathcal {P}}{\mathbb {Q} }}}$ to be a set, and so neither is the class of all subsets of ${\displaystyle {\mathbb {Q} }}$ that do fulfill the named properties. What is required for the class of Dedekind reals to be a set is an axiom regarding existence of a set of subsets.

In either case, fewer statements about the arithmetic of the reals are decidable, compared to the classical theory.

#### Constructive schools

Non-constructive claims valuable in the study of constructive analysis are commonly formulated as concerning all binary sequences, i.e. functions ${\displaystyle f\colon \omega \to \{0,1\}}$. That is to say claims quantified by ${\displaystyle \forall (f\in \{0,1\}^{\mathbb {N} })}$.

A most prominent example is the limited principle of omniscience ${\displaystyle {\mathrm {LPO} }}$, postulating a disjunctive property, like ${\displaystyle {\mathrm {LEM} }}$ at the level of ${\displaystyle \Pi _{1}^{0}}$-sentences or functions. (Example functions can be constructed in raw ${\displaystyle {\mathsf {PA}}}$ such that, if ${\displaystyle {\mathsf {PA}}}$ is consistent, the competing disjuncts are ${\displaystyle {\mathsf {PA}}}$-unprovable.) The principle is independent of e.g. ${\displaystyle {\mathsf {CZF}}}$ introduced below. In that constructive set theory, ${\displaystyle {\mathrm {LPO} }}$ implies its "lesser" version, denoted ${\displaystyle {\mathrm {LLPO} }}$, a restricted variant of De Morgan’s law. It moreover implies Markov's principle ${\displaystyle {\mathrm {MP} }}$, a form of proof by contradiction and the ${\displaystyle \Pi _{1}^{0}}$-version of the  fan theorem. Mention of such principles holding for ${\displaystyle \Pi _{1}^{0}}$-sentences generally hint at equivalent formulations in terms of sequences, deciding apartness of reals. In a constructive analysis context with countable choice, ${\displaystyle {\mathrm {LPO} }}$ is e.g. equivalent to the claim that every real is either rational or irrational - again without the requirement to witness either disjunct.

So for some propositions employed in theories of constructive analysis that are not provable using just base intuitionistic logic, see ${\displaystyle {\mathrm {MP} }}$ or even the non-classical  constructive Church's thesis ${\displaystyle {\mathrm {CT} }}$ or some of its consequences on the recursive mathematics side (${\displaystyle {\mathsf {RUSS}}}$ or ${\displaystyle {\mathsf {CRM}}}$), and as well as Kripke's schema (turning all subclasses of ${\displaystyle \omega }$ countable), bar induction, the decidable fan theorem ${\displaystyle {\mathrm {FAN} }_{\Delta }}$ or even the non-classical continuity principle determining functions on  unending sequences through finite initial segments on  Brouwerian intuitionist side (${\displaystyle {\mathsf {INT}}}$). Both schools contradict ${\displaystyle {\mathrm {LPO} }}$, so that choosing to adopt such laws makes the theory inconsistent with theorems in classical analysis.

#### Infinite trees

Through the relation between computability and the arithmetical hierarchy, insights in this classical study are also revealing for constructive considerations. A basic insight of reverse mathematics concerns computable infinite finitely branching binary trees. Such a tree may e.g. be encoded as an infinite set of finite sets

${\displaystyle T\,\subset \,\cup _{n\in \omega }\{0,1\}^{\{0,1,\dots ,n-1\}}}$,

with decidable membership, and those trees then provably contain elements of arbitrary big finite size. The Weak Kőnigs lemma ${\displaystyle {\mathrm {WKL} }}$ states states: For such ${\displaystyle T}$, there always exists an infinite path in ${\displaystyle \omega \to \{0,1\}}$, i.e. an infinite sequence such that all its initial segments are part of the tree. In reverse mathematics, the second-order arithmetic ${\displaystyle {\mathsf {RCA}}_{0}}$ does not prove ${\displaystyle {\mathrm {WKL} }}$. To understand this, note that there are computable trees ${\displaystyle K}$ for which no computable such path through it exists. To prove this, one enumerates the partial computable sequences and then diagonalizes all total computable sequences in one partial computable sequences ${\displaystyle d}$. One can then roll out a certain tree ${\displaystyle K}$, one exactly compatible with the still possible values of ${\displaystyle d}$ everywhere, which by construction is incompatible with any total computable path.

In ${\displaystyle {\mathsf {CZF}}}$, the principle ${\displaystyle {\mathrm {WKL} }}$ implies the non-constructive lesser limited principle of omniscience ${\displaystyle {\mathrm {LLPO} }}$. In a more conservative context, they are equivalent assuming ${\displaystyle \Pi _{1}^{0}}$-${\displaystyle {\mathrm {AC} }_{\omega ,2}}$ (a very weak countable choice). It is also equivalent to the Brouwer fixed point theorem and other theorems regarding values of continuous functions on the reals. The fixed point theorem in turn implies the intermediate value theorem, but be aware that the classical theorems can translate to different variants when expressed in a constructive context.

The ${\displaystyle {\mathrm {WKL} }}$ concerns infinite graphs and so its contrapositive gives a condition for finiteness. Over the classical arithmetic theory ${\displaystyle {\mathsf {RCA}}_{0}}$, this gives equivalence to the Borel compactness regarding finite subcovers of the real unit interval. A closely related existence claim involving finite sequences in an infinite context is the decidable fan theorem ${\displaystyle {\mathrm {FAN} }_{\Delta }}$. Over the ${\displaystyle {\mathsf {RCA}}_{0}}$, they are actually equivalent. In ${\displaystyle {\mathsf {CZF}}}$, those are distinct, but again assuming some choice, ${\displaystyle {\mathrm {WKL} }}$ implies ${\displaystyle {\mathrm {FAN} }_{\Delta }}$.

#### Restricting function spaces

In the following remark function and claims made about them is again meant in the sense of 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 but ${\displaystyle {\mathrm {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 at hand. Either way, those natural numbers that are, in computability theory, thought of as indices for the computable functions which are total, are ${\displaystyle \Pi _{2}^{0}}$, in the arithmetical hierarchy. Which is to say it is still a subclass of the naturals. And there, totality, as a predicate on all programs, is famously computably undecidable.

A non-classical constructive Church's thesis ${\displaystyle {\mathrm {CT} }}$, as per assumption in its antecedent, concerns the predicate definitions (and thus here set functions) that are demonstrably total and it postulates they corresponds to computable programs. Adopting the postulate makes ${\displaystyle \omega \to \omega }$ into a "sparse" set, as viewed from classical set theory. See subcountability.

The postulate ${\displaystyle {\mathrm {CT} }}$ is still consistent with intuitionistic arithmetic or choice. But it contradicts classically valid principles such as ${\displaystyle {\mathrm {LLPO} }}$ and ${\displaystyle {\mathrm {FAN} }_{\Delta }}$, which are amongst the weakest often discussed principles.

### Induction

#### Mathematical induction

In set language, induction principles can read ${\displaystyle \mathrm {Ind} (A)\implies \omega \subset A}$ with the antecedent ${\displaystyle \mathrm {Ind} (A)}$ defined as further above. Via the strong axiom of Infinity and bounded Separation, the validity of induction for bounded definitions was already established, so induction holds for formulas ${\displaystyle \phi (k)}$ of the form ${\displaystyle k\in x}$, where ${\displaystyle x}$ is a set.

It is instructive to observe that a proposition in the consequent of a subclass proposition, such as in ${\displaystyle \omega \subset \{n\in \omega \mid y^{\{0,1,\dots ,n-1\}}{\text{ is a set}}\}}$ (here expressed using class notation involving a subclass that may not constitute a set - meaning many axioms wont apply) and the plain ${\displaystyle \forall (n\in \omega ).y^{\{0,1,\dots ,n-1\}}{\text{ is a set}}}$ are just two ways of formulating the same desired claim (an ${\displaystyle n}$-indexed conjunction of claims here, in particular.) So a set theoretical framework with just bounded Separation can be strengthened through arithmetical induction schemas for unbounded predicates.

The iteration principle for set functions mentioned before is, alternatively to Exponentiation, also implied by the full induction schema over one's structure modeling the naturals (e.g. ${\displaystyle \omega }$). This is also the first-order arithmetic principle to prove more functions total, than ${\displaystyle {\mathsf {PRA}}}$ does. It is often formulated directly in terms of predicates, as follows.

Consider schema ${\displaystyle {\mathrm {Ind} }_{\omega }}$:

 Axiom schema of full mathematical induction: For any predicate ${\displaystyle \phi }$ on ${\displaystyle \omega }$, ${\displaystyle {\Big (}\phi (0)\ \land \ \forall (k\in \omega ).{\big (}\phi (k)\implies \phi (Sk){\big )}{\Big )}\implies \forall (n\in \omega ).\phi (n)}$

Here the 0 denotes ${\displaystyle \{\}}$ as above, and the set ${\displaystyle Sn}$ denotes the successor set of ${\displaystyle n\in \omega }$, with ${\displaystyle n\in Sn}$. By Axiom of Infinity above, it is again a member of ${\displaystyle \omega }$.

As stated in the section on Choice, induction principles are also implied by various forms of choice principles. The full induction schema is implied by the full Separation schema.

To proof the existence of a transitive closure for every set with respect to ${\displaystyle \in }$, at least a bounded iteration schema is needed. It is worth noting that in the program of predicative arithmetic, the full mathematical induction schema has been criticized as possibly being impredicative, when natural numbers are defined as the object which fulfill this schema.

#### Set Induction

Full Set Induction in ${\displaystyle {\mathsf {ECST}}}$ proves full mathematical induction over the natural numbers. Indeed, it gives induction on ordinals and ordinal arithmetic. Replacement is not required to prove induction over the set of naturals, but it is for their arithmetic modeled within the set theory.

The stronger axiom ${\displaystyle {\mathrm {Ind} }_{\in }}$ then reads as follows:

 Axiom schema of Set induction: For any predicate ${\displaystyle \phi }$, ${\displaystyle {\Big (}\forall s.\,{\big (}\forall (x\in s).\ \phi (x){\big )}\implies \phi (s){\Big )}\implies \forall y.\phi (y)}$

Here ${\displaystyle \forall x\in \{\}.\phi (x)}$ holds trivially and corresponds to the "bottom case" in the standard framework. The variant of the Axiom just for bounded formulas is also studied independently and may be derived from other axioms.

The axiom allows definitions of class functions by transfinite recursion. The study of the various principles that grant set definitions by induction, i.e. inductive definitions, is a main topic in the context of constructive set theory and their comparatively weak  strengths. This also holds for their  counterparts in type theory.

The Axiom of Regularity together with bounded/unbounded Separation implies Set Induction but also bounded/unbounded ${\displaystyle {\mathrm {LEM} }}$, so Regularity is non-constructive. Conversely, ${\displaystyle {\mathrm {LEM} }}$ together with Set Induction implies Regularity.

#### Metalogic

This now covers variants of all of the eight Zermelo–Fraenkel axioms. Extensionality, Pairing, Union and Replacement are indeed identical. Infinity is stated in a strong formulation and implies Emty Set, as in the classical case. Separation, classically stated redundantly, is constructively not implied by Replacement. Without the Law of Excluded Middle, the theory here is lacking, in its classical form, full Separation, Powerset as well as Regularity. Adding ${\displaystyle {\mathrm {LEM} }}$ gives ${\displaystyle {\mathsf {ZF}}}$.

The added proof-theoretical strength attained with Induction in the constructive context is significant, even if dropping Regularity in the context of ${\displaystyle {\mathsf {ZF}}}$ does not reduce the proof-theoretical strength. Aczel was also one of the main developers or Non-well-founded set theory, which rejects this last axiom.

### Strong Collection

With all the weakened axioms of ${\displaystyle {\mathsf {ZF}}}$ and now going beyond those axioms also seen in Myhill's typed approach, consider the theory with Exponentiation now strengthened by the  collection schema. It concerns a property for relations, giving rise to a somewhat repetitive format in its first-order formulation.

 Axiom schema of Strong Collection: For any predicate ${\displaystyle \phi }$, ${\displaystyle \forall a.\ \ {\Big (}\forall (x\in a).\exists y.\phi (x,y){\Big )}\implies \exists b.{\Big (}\forall (x\in a).\exists (y\in b).\phi (x,y)\ \land \ \forall (y\in b).\exists (x\in a).\phi (x,y){\Big )}}$

It states that if ${\displaystyle \phi }$ is a relation between sets which is total over a certain domain set ${\displaystyle a}$ (that is, it has at least one image value for every element in the domain), then there exists a set ${\displaystyle b}$ which contains at least one image under ${\displaystyle \phi }$ of every element of the domain - and this formulation then moreover states that only such images are elements of that codomain set. The last clause makes the axiom - in this constructive context - stronger than the standard formulation of Collection. It is guaranteeing that ${\displaystyle b}$ does not overshoot the codomain of ${\displaystyle \phi }$ and thus the axiom is expressing some power of a Separation procedure. The axiom may be expressed as saying that for every total relation, there exists a set ${\displaystyle b}$ such that the relation is total in both directions.

The axiom is an alternative to the Replacement schema and indeed supersedes it, due to not requiring the binary relation definition to be functional, but possibly multi-valued.

#### Metalogic

This theory without ${\displaystyle {\mathrm {LEM} }}$, unbounded separation and "naive" Power set enjoys various nice properties. For example, as opposed to ${\displaystyle {\mathsf {CZF}}}$ below, it has the Existence Property: If, for any property ${\displaystyle \Phi }$, the theory proves that a set exist that has that property, i.e. if the theory proves the statement ${\displaystyle \exists x.\Phi (x)}$, then there is also a property ${\displaystyle \Psi }$ that uniquely describes such a set instance. I.e., the theory then also proves ${\displaystyle \exists !x.\Psi (x)\land \Phi (x)}$. This can be compared to Heyting arithmetic where theorems are realized by concrete natural numbers and have these properties. In set theory, the role is played by defined sets. For contrast, recall that in ${\displaystyle {\mathsf {ZFC}}}$, the Axiom of Choice implies the Well-ordering theorem, so that total orderings with least element for subsets of sets like ${\displaystyle \mathbb {R} }$ are formally proven to exist, even if provably no such ordering can be described.

### Constructive Zermelo–Fraenkel

One may approach Power set further without losing a type theoretical interpretation. The theory known as ${\displaystyle {\mathsf {CZF}}}$ is the axioms above plus a stronger form of Exponentiation. It is by adopting the following alternative, which can again be seen as a constructive version of the Power set axiom:

 Axiom schema of Subset Collection: For any predicate ${\displaystyle \phi }$, ${\displaystyle \forall a.\forall b.\ \ \exists u.\forall z.{\big (}\forall (x\in a).\exists (y\in b).\phi (x,y,z){\big )}\implies \exists (v\in u).{\big (}\forall (x\in a).\exists (y\in v).\phi (x,y,z)\;\land \;\forall (y\in v).\exists (x\in a).\phi (x,y,z){\big )}}$

This Subset Collection axiom schema is equivalent to a single and somewhat clearer alternative Axiom of Fullness. To this end, let ${\displaystyle a\Sigma {b}}$ is the class of all total relations between a and b, this class is given as

${\displaystyle r\in a\Sigma {b}\iff {\big (}\forall (x\in a).\exists (y\in b).\langle x,y\rangle \in r{\big )}\,\land \,{\big (}\forall (p\in r).\exists (x\in a).\exists (y\in b).p=\langle x,y\rangle {\big )}}$

With this, state ${\displaystyle {\mathrm {Fullness} }}$, an alternative to Subset Collection. It guarantees that there exists at least some set ${\displaystyle c\subset a\Sigma {b}}$ holding the a good amount of the desired relations. More concretely, between any two sets ${\displaystyle a}$ and ${\displaystyle b}$, there is a set ${\displaystyle c}$ which contains a total sub-relation ${\displaystyle s}$ for any total relation ${\displaystyle r}$ from ${\displaystyle a}$ to ${\displaystyle b}$.

Axiom of Fullness:
${\displaystyle \forall a.\forall b.\ \ \exists (c\subset a\Sigma {b}).\forall (r\in a\Sigma {b}).\exists (s\in c).s\subset r}$

The Fullness axiom is in turn implied by the so called Presentation Axiom about sections, which can also be formulated category theoretically.

Fullness implies the binary refinement property. This is necessary to prove that the class of Dedekind cuts is a set and this does not require Induction or Collection. Over ${\displaystyle {\mathsf {ECST}}}$, binary refinement also proves the existence of all characteristic function spaces ${\displaystyle 2^{A}}$.

Neither linearity of ordinals, nor existence of power sets of finite sets are derivable in this theory. Assuming either implies Power set in this context.

#### Metalogic

This theory has the numerical existence property and the disjunctive property. It lacks the existence property due to the Schema/Fullness, unless this is replaced by the weaker Exponentiation axiom.

In 1977 Aczel showed that ${\displaystyle {\mathsf {CZF}}}$ can still be interpreted in Martin-Löf type theory,[4] using the propositions-as-types approach, providing what is now seen a standard model of ${\displaystyle {\mathsf {CZF}}}$ in type theory, ${\displaystyle {\mathsf {ML_{1}V}}}$.[5] This is done in terms of images of its functions as well as a fairly direct constructive and predicative justification, while retaining the language of set theory. Conversely, ${\displaystyle {\mathsf {CZF}}}$ interprets ${\displaystyle {\mathsf {ML_{1}V}}}$. All statements validated in the subcountable model of the set theory can be proven exactly via ${\displaystyle {\mathsf {CZF}}}$ plus the choice principle ${\displaystyle \Pi \Sigma }$-${\displaystyle AC}$, stated further above. With a type theoretical model, ${\displaystyle {\mathsf {CZF}}}$ has modest proof theoretic strength, see ${\displaystyle {\mathsf {IKP}}}$: Bachmann–Howard ordinal. Those theories with choice have the existence property for a broad class of set in common mathematics. Martin-Löf type theories with additional induction principles validate corresponding set theoretical axioms.

#### Breaking with ZF

One may further add the non-classical claim that all sets are subcountable as an axiom. Then ${\displaystyle \omega \to \omega }$ is a set (by Infinity and Exponentiation) while the class ${\displaystyle {\mathcal {P}}\omega }$ or even ${\displaystyle {\mathcal {P}}\{0\}}$ is provably not a set, by Cantor's diagonal argument. So this theory then logically rejects Powerset and ${\displaystyle {\mathrm {LEM} }}$.

In 1989 Ingrid Lindström showed that non-well-founded sets obtained by replacing Set Induction, the constructive equivalent of the Axiom of Foundation, in ${\displaystyle {\mathsf {CZF}}}$ with Aczel's anti-foundation axiom (${\displaystyle {\mathsf {CZFA}}}$) can also be interpreted in Martin-Löf type theory.[6] The theory ${\displaystyle {\mathsf {CZFA}}}$ may be studied by also adding back mathematical induction, as well as the assertion that every set is member of a transitive set.

### Intuitionistic Zermelo–Fraenkel

The theory ${\displaystyle {\mathsf {IZF}}}$ is ${\displaystyle {\mathsf {CZF}}}$ with the standard Separation and Power set. As elaborated in the section on Exponentiation, these axioms are strong enough so that full ${\displaystyle {\mathrm {LEM} }}$ is already implied by ${\displaystyle {\mathrm {LEM} }}$ for bounded formulas, or in fact by ${\displaystyle \forall x.{\big (}0\in x\lor 0\notin x{\big )}}$.

Here, in place of the Axiom schema of replacement, one may use the

 Axiom schema of collection: For any predicate ${\displaystyle \phi }$, ${\displaystyle \forall z.{\big (}\forall (x\in z).\exists y.\phi (x,y){\big )}\implies \exists w.\forall (x\in z).\exists (y\in w).\phi (x,y)}$

While the axiom of replacement requires the relation ${\displaystyle \phi }$ to be functional over the set ${\displaystyle z}$ (as in, for every ${\displaystyle x}$ in ${\displaystyle z}$ there is associated exactly one ${\displaystyle y}$), the Axiom of Collection does not. It merely requires there be associated at least one ${\displaystyle y}$, and it asserts the existence of a set which collects at least one such ${\displaystyle y}$ for each such ${\displaystyle x}$. ${\displaystyle {\mathrm {LEM} }}$ together with the Collection implies Replacement.

As such, ${\displaystyle {\mathsf {IZF}}}$ can be seen as the most straight forward variant of ${\displaystyle {\mathsf {ZF}}}$ without ${\displaystyle {\mathrm {LEM} }}$.

The theory is consistent with ${\displaystyle \omega \to \omega }$ being subcountable as well as with Church's thesis for number theoretic functions. But, as implied above, the subcountability property cannot be adopted for all sets, given the theory proves ${\displaystyle {\mathcal {P}}\omega }$ to be a set.

#### Metalogic

Changing the Axiom schema of Replacement to the Axiom schema of Collection, the resulting theory has the Numerical Existence Property.

Even without ${\displaystyle {\mathrm {LEM} }}$, the  proof theoretic strength of ${\displaystyle {\mathsf {IZF}}}$ equals that of ${\displaystyle {\mathsf {ZF}}}$.

While ${\displaystyle {\mathsf {ZF}}}$ is based on intuitionistic rather than classical logic, it is considered impredicative. It allows formation of sets using the Axiom of Separation with any proposition, including ones which contain quantifiers which are not bounded. Thus new sets can be formed in terms of the universe of all sets. Additionally the power set axiom implies the existence of a set of truth values. In the presence of excluded middle, this set exists and has two elements. In the absence of it, the set of truth values is also considered impredicative.

#### History

In 1973, John Myhill proposed a system of set theory based on intuitionistic logic[7] taking the most common foundation, ${\displaystyle {\mathsf {ZFC}}}$, and throwing away the Axiom of choice and the law of the excluded middle, 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 {LEM} }}$. In those cases, the intuitionistically weaker formulations were then adopted for the constructive set theory.

### Intuitionistic Z

Again on the weaker end, as with its historical counterpart Zermelo set theory, one may denote by ${\displaystyle {\mathsf {IZ}}}$ the intuitionistic theory set up like ${\displaystyle {\mathsf {IZF}}}$ but without Replacement, Collection or Induction.

### Intuitionistic KP

Let us mention another very weak theory that has been investigated, namely Intuitionistic (or constructive) Kripke–Platek set theory ${\displaystyle {\mathsf {IKP}}}$. The theory has not only Separation but also Collection restricted, i.e. it is similar to ${\displaystyle {\mathsf {BCST}}}$ but with Induction instead of full Replacement. It is especially weak when studied without Infinity. The theory does not fit into the hierarchy as presented above, simply because it has Axiom schema of Set Induction from the start. This enables theorems involving the class of ordinals.

## Sorted theories

### Constructive set theory

As he presented it, Myhill's system ${\displaystyle {\mathsf {CST}}}$ is a theory using constructive first-order logic with identity and three sorts, namely sets, natural numbers, functions. Its axioms are:

• The usual Axiom of Extensionality for sets, as well as one for functions, and the usual Axiom of union.
• The Axiom of restricted, or predicative, separation, which is a weakened form of the Separation axiom from classical set theory, requiring that any quantifications be bounded to another set, as discussed.
• A form of the Axiom of Infinity asserting that the collection of natural numbers (for which he introduces a constant ${\displaystyle \omega }$) is in fact a set.
• The axiom of Exponentiation, asserting that for any two sets, there is a third set which contains all (and only) the functions whose domain is the first set, and whose range is the second set. This is a greatly weakened form of the Axiom of power set in classical set theory, to which Myhill, among others, objected on the grounds of its impredicativity.

And furthermore:

One can roughly identify the strength of this theory with a constructive subtheories of ${\displaystyle {\mathsf {ZF}}}$ when comparing with the previous sections.

### Bishop style set theory

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

A lot of analysis and module theory has been developed in this context.

### Category theories

Not all formal logic theories of sets need to axiomize the binary membership predicate "${\displaystyle \in }$" directly. And an Elementary Theory of the Categories Of Set (${\displaystyle {\mathsf {ETCS}}}$), e.g. capturing pairs of composable mappings between objects, can also be expressed with a constructive background logic (${\displaystyle {\mathsf {CETCS}}}$). Category theory can be set up as a theory of arrows and objects, although first-order axiomatizations only in terms of arrows are possible.

Good models of constructive set theories in category theory are the pretoposes mentioned in the Exponentiation section - possibly also requiring enough projectives, an axiom about surjective "presentations" of set, implying Countable Dependent Choice.

Beyond that, topoi also have internal languages that can be intuitionistic themselves and capture a notion of sets.

## References

1. ^ Gambino, N. (2005). "PRESHEAF MODELS FOR CONSTRUCTIVE SET THEORIES" (PDF). In Laura Crosilla and Peter Schuster (ed.). From Sets and Types to Topology and Analysis (PDF). pp. 62–96. doi:10.1093/acprof:oso/9780198566519.003.0004. ISBN 9780198566519.
2. ^ Scott, D. S. (1985). Category-theoretic models for Intuitionistic Set Theory. Manuscript slides of a talk given at Carnegie-Mellon University
3. ^ Peter Aczel and Michael Rathjen, Notes on Constructive Set Theory, Reports Institut Mittag-Leffler, Mathematical Logic - 2000/2001, No. 40
4. ^ Aczel, Peter: 1978. The type theoretic interpretation of constructive set theory. In: A. MacIntyre et al. (eds.), Logic Colloquium '77, Amsterdam: North-Holland, 55–66.
5. ^ Rathjen, M. (2004), "Predicativity, Circularity, and Anti-Foundation" (PDF), in Link, Godehard (ed.), One Hundred Years of Russell ́s Paradox: Mathematics, Logic, Philosophy, Walter de Gruyter, ISBN 978-3-11-019968-0
6. ^ Lindström, Ingrid: 1989. A construction of non-well-founded sets within Martin-Löf type theory. Journal of Symbolic Logic 54: 57–64.
7. ^ Myhill, "Some properties of Intuitionistic Zermelo-Fraenkel set theory", Proceedings of the 1971 Cambridge Summer School in Mathematical Logic (Lecture Notes in Mathematics 337) (1973) pp 206-231