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 "$=$" and "$\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 (${\mathrm {PEM} }$), constructive set theories often require some logical quantifiers in their axioms to be set bounded. The latter is motivated by results tied to impredicativity.

Introduction

Constructive outlook

Preliminary on the use of intuitionistic logic

The logic of the set theories discussed here is constructive in that it rejects the principle of excluded middle ${\mathrm {PEM} }$, i.e. that the disjunction $\phi \lor \neg \phi$ automatically holds for all propositions $\phi$. This is also often called the law of excluded middle (${\mathrm {LEM} }$) in contexts where it is assumed. Constructively, as a rule, to prove the excluded middle for a proposition $P$, i.e. to prove the particular disjunction $P\lor \neg P$, either $P$ or $\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 $Q(x)$ for $x$ in a domain $X$ is said to be decidable when the more intricate statement $\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 $P$ (and/or $Q$) in the sense that they prove excluded middle for $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 $\neg P$, one valid De Morgan's law thus implies $\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 $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 $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 $P\lor \exists (x\in X).\neg Q(x)$ implies the existence claim $\exists (x\in X).(Q(x)\to P)$, which in turn implies ${\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 $P$ is rejected, one deals with a counter-example existence claim $\exists (x\in X).\neg Q(x)$, which is generally constructively stronger than a rejection claim $\neg \forall (x\in X).Q(x)$: Exemplifying a $t$ such that $Q(t)$ is contradictory of course means it is not the case that $Q$ holds for all possible $x$. But one may also demonstrate that $Q$ holding for all $x$ would logically lead to a contradiction without the aid of a specific counter-example, and even while not being able to construct one. In the latter case, constructively, here one does not stipulate an existence claim.

Imposed restrictions on a set theory

Compared to the classical counterpart, one is generally less likely to prove the existence of relations that cannot be realized. A restriction to the constructive reading of existence apriori leads to stricter requirements regarding which characterizations of a set $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 ${\mathrm {PEM} }$ for the formulas permitted in one's adopted Separation schema, by Diaconescu's theorem. Similar results hold for the Axiom of Regularity existence claim, as shown below. The latter has a classically equivalent inductive substitute. So a genuinely intuitionistic development of set theory requires the rewording of some standard axioms to classically equivalent ones. Apart from demands for computability and reservations regrading of impredicativity, technical question regarding which non-logical axioms effectively extend the underlying logic of a theory is also a research subject in its own right.

Metalogic

With computably undecidable propositions already arising in Robinson arithmetic, even just Predicative separation lets one define elusive subsets easily. In stark contrast to the classical framework, constructive set theories may be closed under the rule that any property that is decidable for all sets is already equivalent to one of the two trivial ones, $\top$ or $\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 $(\alpha \in \beta )\lor (\alpha =\beta )\lor (\beta \in \alpha )$. This determines whether the relation is trichotomous. A weakened theory of ordinals in turn affects the proof theoretic strength defined in ordinal analysis.

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

A set theory does not only express theorems about numbers, and so one may consider a more general so-called strong existence property that is harder to come by, as will be discussed. A theory has this property if the following can be established: For any property $\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 $\psi$ that uniquely describes such a set instance. More formally, for any predicate $\phi$ there is a predicate $\psi$ so that

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

Anti-classical principles

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

$\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 $n$ being mapped to the number $f(n)$ is, through $w$, witnessed to be a computable mapping. Here ${\mathbb {N} }$ now denotes a set theory model of the standard natural numbers and $e$ is an index with respect to a fixed program enumeration. Stronger variants have been used, which extend this principle to functions $f\in {\mathbb {N} }^{X}$ defined on domains $X\subset {\mathbb {N} }$ of low complexity. The principle rejects decidability for the predicate $Q(e)$ defined as $\exists (w\in {\mathbb {N} }).T(e,e,w)$, expressing that $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 $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 ${\mathsf {RCA}}_{0}$, a subsystem of the two-sorted first-order theory ${\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 ${\mathbb {N} }^{\mathbb {N} }$ holds also other functions than the computable ones. For example, there is a proof in ${\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 (${\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 $\forall (x\in X).\neg \neg {\big (}Q(x)\lor \neg Q(x){\big )}$ for any $Q$. And so for any given element $x$ of $X$, the corresponding excluded middle statement for the proposition cannot be negated. Indeed, for any given $x$, by noncontradiction it is impossible to rule out $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 $\neg \forall (x\in X).{\big (}Q(x)\lor \neg Q(x){\big )}$. Adopting this does not necessitate providing a particular $t\in X$ witnessing the failure of excluded middle for the particular proposition $Q(t)$, i.e. witnessing the inconsistent $\neg {\big (}Q(t)\lor \neg Q(t){\big )}$. Predicates $Q(x)$ on an infinite domain $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 $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 $Q(x)$ states that a sequence $x$ is everywhere zero. Concerning this property, of being conclusively identified as the sequence which is forever constant, adopting Brouwer's continuity principle strictly rules out that this could be proven decidable for all the sequences.

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

History and overview

Historically, the subject of constructive set theory (often also "${\mathsf {CST}}$") begun with John Myhill's work on the theories also called ${\mathsf {IZF}}$ and ${\mathsf {CST}}$. In 1973, he had proposed the former as a first-order set theory based on intuitionistic logic, taking the most common foundation ${\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 ${\mathsf {ZFC}}$ axioms which are equivalent in the classical setting are inequivalent in the constructive setting, and some forms imply ${\mathrm {PEM} }$, as will be demonstrated. In those cases, the intuitionistically weaker formulations were consequently adopted. The far more conservative system ${\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 ${\mathsf {ZF}}$, leading up to Peter Aczel's well studied ${\mathsf {CZF}}$, and beyond. Many modern results trace back to Rathjen and his students. ${\mathsf {CZF}}$ is also characterized by the two features present also in Myhill's theory: On the one hand, it is using the Predicative Separation instead of the full, unbounded Separation schema. Boundedness can be handled as a syntactic property or, alternatively, the theories can be conservatively extended with a higher boundedness predicate and its axioms. Secondly, the impredicative Powerset axiom is discarded, generally in favor of related but weaker axioms. The strong form is very casually used in classical general topology. Adding ${\mathrm {PEM} }$ to a theory even weaker than ${\mathsf {CZF}}$ recovers ${\mathsf {ZF}}$, as detailed below. The system, which has come to be known as Intuitionistic Zermelo–Fraenkel set theory (${\mathsf {IZF}}$), is a strong set theory without ${\mathrm {PEM} }$. It is similar to ${\mathsf {CZF}}$, but less conservative or predicative. The theory denoted ${\mathsf {IKP}}$ is the constructive version of ${\mathsf {KP}}$, the classical Kripke–Platek set theory without a form of Powerset and where even the Axiom of Collection is bounded.

Models

Many theories studied in constructive set theory are mere restrictions of Zermelo–Fraenkel set theory (${\mathsf {ZF}}$) with respect to their axiom as well as their underlying logic. Such theories can then also be interpreted in any model of ${\mathsf {ZF}}$.

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

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

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

Notation

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

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

Language

The propositional connective symbols used to form syntactic formulas are standard. The axioms of set theory give a means to prove equality "$=$" of sets and that symbol may, by abuse of notation, be used for classes. A set in which the equality predicate is decidable is also called discrete. Negation "$\neg$" of equality is sometimes called the denial of equality, and is commonly written "$\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, "$\in$". As with equality, negation of elementhood "$\in$" is often written "$\notin$".

Variables

Below the Greek $\phi$ denotes a proposition or predicate variable in axiom schemas and $P$ or $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 "$Q(z)$". Unique existence $\exists !x.Q(x)$ here means $\exists x.\forall y.{\big (}y=x\leftrightarrow Q(y){\big )}$.

Classes

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

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

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

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

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

Extensional equivalence

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

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

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

Subtheories of ZF

Main article: Constructive subtheories of Zermelo–Fraenkel set theory

Sorted theories

Constructive set theory

As he presented it, Myhill's system ${\mathsf {CST}}$ is a theory using constructive first-order logic with identity and two more sorts beyond sets, namely natural numbers and 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 $\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:

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

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

And finally the theory adopts

• An Axiom of dependent choice, which is much weaker than the usual Axiom of choice.

Bishop style set theory

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

A lot of 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 "$\in$" directly. A theory like the Elementary Theory of the Categories Of Set (${\mathsf {ETCS}}$), e.g. capturing pairs of composable mappings between objects, can also be expressed with a constructive background logic. Category theory can be set up as a theory of arrows and objects, although first-order axiomatizations only in terms of arrows are possible.

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

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

See also

• Axiom schema of predicative separation
• Constructive mathematics
• Constructive analysis
• Constructive Church's thesis rule and principle
• Computable set
• Diaconescu's theorem
• Disjunction and existence properties
• Epsilon-induction
• Hereditarily finite set
• Heyting arithmetic
• Impredicativity
• Intuitionistic type theory
• Law of excluded middle
• Ordinal analysis
• Set theory
• Subcountability

Further reading

• Troelstra, Anne; van Dalen, Dirk (1988). Constructivism in Mathematics, Vol. 2. Studies in Logic and the Foundations of Mathematics. p. 619. ISBN 978-0-444-70358-3.
• Aczel, P. and Rathjen, M. (2001). Notes on constructive set theory. Technical Report 40, 2000/2001. Mittag-Leffler Institute, Sweden.

External links

• Crosilla, Laura (13 February 2019). "Set Theory: Constructive and Intuitionistic ZF". In Zalta, Edward N. (ed.). Stanford Encyclopedia of Philosophy.
• Van den Berg, Benno (7 September 2012). "Constructive set theory – an overview" (PDF). Slides from Heyting dag, Amsterdam