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.

Apart from rejecting the law of excluded middle (LEM), constructive set theories often require some universal quantifiers ${\displaystyle \forall }$ in their axioms to be bounded, motivated by results tied to impredicativity.

Overview

The logic of the theories discussed here is constructive in that it rejects LEM, i.e. that the disjunction ${\displaystyle \phi \lor \neg \phi }$ automatically holds for all propositions. This requires rejection of strong choice principles and the rewording of some standard axioms. For example, the Axiom of Choice implies LEM by Diaconescu's theorem, and so does the Axiom of Regularity in its standard form. In turn, constructive theories often do not allow for proofs of properties that are provably computationally undecidable and also often do not prove the existence of relations that can not 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 )}$. This in turn affects the proof theoretic strength defined in ordinal analysis.

The subject of constructive set theory begun by John Myhill's work on the CST set theory, a theory of several sorts and bounded quantification, aiming to provide a formal foundation for Errett Bishop's program of constructive mathematics. Below we list a sequence of theories in the same language as ZF, leading up to Peter Aczel's well studied constructive Zermelo-Fraenkel,[1] CZF and beyond. This theory 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. The system, which has come to be known as Intuitionistic Zermelo–Fraenkel set theory, IZF, is a strong set theory without LEM. It is similar to CFZ, but less conservative or predicative. The theory denoted IKP is the constructive version of KP, the classical Kripke–Platek set theory where even Collection is bounded.

Many theories studied in constructive set theory are mere restrictions, with respect to their axiom as well as their underlying logic, of Zermelo–Fraenkel set theory (ZF). Such theories can then also be interpreted in any model of ZF. Adding LEM to a theory like CZFE recovers ZF, as detailed below. Thus, adding Choice to such theories recovers ZFC. In this way, CZFE theory is a version of ZFC without Choice characterized by lacking full, unbounded separation, existence of arbitrary power sets and, of course, being constructive.

As far as constructive realizations go there is a realizability theory and Aczel's CZF has been interpreted in a Martin Löf type theories, as described below. In this way, set theory theorems provable in 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.[2][3]

Subtheories of ZF

Axioms that are virtually always deemed uncontroversial and part of all theories considered in this article are:-

• Extensionality, a means of proving equality of two sets

${\displaystyle \forall x.\forall y.\ \ \forall z.(z\in x\iff z\in y)\implies x=y}$

• Pairing

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

and

• Union

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

A sort of blend between pairing and union, an axiom more readily related to the successor operation that is relevant for the standard modeling of individual Neumann ordinals is the Axiom of adjunction. This axiom would also readily be accepted, but is not relevant in the context of stronger axioms below.

BCST

Basic constructive set theory BCST consists of several axioms also part of standard set theory, except the Separation axiom is weakened. Beyond the three axioms above, it adopts:

• Axiom schema of predicative separation, separating subsets form given sets

For any bounded predicate ${\displaystyle \phi }$ with ${\displaystyle y}$ not free in it:

${\displaystyle \forall y.\ \ \exists s.\forall x.(x\in s\iff (x\in y\land \phi (x)))}$

also called Bounded Separation, i.e. the Separation for bounded quantifiers only.

• Axiom schema of replacement, granting existence, as sets, of range of function-like predicates (the quantifier ${\displaystyle \exists$ !} denotes unique existence, as usual), obtained via their domains

For any predicate ${\displaystyle \phi }$:

${\displaystyle \forall d.\ \ \forall (x\in d).\exists !y.\phi (x,y)\implies \exists r.\forall y.(y\in r\iff \exists (x\in d).\phi (x,y))}$

With the Replacement scheme, this theory proves that the equivalence classes or indexed sums are sets. In particular, the Cartesian product of two sets is a set, e.g. with their elements ${\displaystyle \langle u,v\rangle \in x\times y}$ given via the standard ordered pair model ${\displaystyle \{\{a\},\{a,b\}\}}$.

Constructive theories often have Axiom schema of Replacement, sometimes even restricted to bounded formulas. However, when other axioms are dropped, this schema is actually often strengthened - not beyond ZF, but instead merely to gain back some provability strength.

Metalogic

In this context of BCST, the Bounded Separation scheme merely amounts to asserting that intersections of sets are sets.

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.

ECST

Denote by ${\displaystyle Sx}$ the successor set ${\displaystyle x\cup \{x\}}$ and by ${\displaystyle \mathrm {Ind} (A)}$ the Inductive property, e.g. ${\displaystyle \{\}\in A\land \forall (n\in A).Sn\in A}$.

Let ${\displaystyle A\subset B}$ denote ${\displaystyle \forall x.x\in A\implies x\in B}$ as usual. 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 ECST has the axiom of BCST as well as

• Strong Infinity, saying that there is a smallest inductive set,

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

A weaker form, sufficient when Powerset and full seperation is available, reads

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

In this set, generally called ${\displaystyle \omega }$ ECST proves induction for bounded, but not on all formulas. In the program of Predicative Arithmetic, even the mathematical induction on the natural numbers, with its universal quantifiers ${\displaystyle \forall n}$ has been criticized as possibly being impredicative, when natural numbers are defined as the object which fulfill this scheme.

Metalogic

This theory still does not interpret full primitive recursion yet. But note that also here in ECST, many statement can be proven per individual set (as opposed to expressions involving a universal quantifier, as e.g. available with an induction axiom) and objects of mathematical interest can be made use of at the class level on an individual bases. As such, the axioms listed so far suffice as a working theory for a good portion of basic mathematics.

So despite having the Replacement axiom, ECST still does not proof the addition to be a set function. To this end, an axiom for a simple notion of iteration must be added, i.e. recursive definitions of functions on ${\displaystyle \omega }$ via other functions, effectively granting existence of natural numbers objects. This then lets the theory interpret Peano arithmetic, or, more precisely, Heyting arithmetic, HA. With this, the rational number arithmetic can then also be defined and its properties, like countability, be proven. The required iteration capability is implied by a Exponentiation (even when restricted to finite domains), discussed next.

Adding the remaining variants of ZF axioms

We already considered a weakened form of the Separation scheme, and two more of the standard ZF axioms shall be weakened for a more predicative and constructive theory, namely Powerset and Regularity.

Firstly, note that 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\implies u\in {\mathcal {P}}x}$. Here ${\displaystyle \subset }$ has been defined in terms of the membership predicate ${\displaystyle \in }$ above. So in such a set theoretical framework, the power class is defined not in a bottom-up construction from its constituents (like an algorithm on lists) but via a comprehension over all sets. Write ${\displaystyle \bot$ :=\{\}} , ${\displaystyle \top$ :=\{\bot \}} and ${\displaystyle \Omega$ :={\mathcal {P}}\top } , which is the power class of a particular singleton set. Note that for any formula ${\displaystyle \phi }$, the class ${\displaystyle \{x\mid x=\bot \land \phi \}}$ equals ${\displaystyle \bot }$ when ${\displaystyle \phi }$ can be rejected and ${\displaystyle \top }$ when ${\displaystyle \phi }$ can be proven, but ${\displaystyle \phi }$ may also not be decidable at all. In this view, the class ${\displaystyle \Omega =\{\bot ,\top ,\dots \}}$ is called the truth value algebra. Classically, all formulas are decidable and one can show not only that ${\displaystyle \Omega }$ is a set, but more concretely that ${\displaystyle \Omega =\{\bot ,\top \}}$.

Recall that in the classical context, the powerset class is then is in bijection with the class of functions from ${\displaystyle A}$ to a two-element set, the so-called characteristic functions. That said, while the subset relation is concise to express in the language of set theory with its primitive symbol ${\displaystyle \in }$, statements involving functions needs some unpacking. Let ${\displaystyle B^{A}}$ (also written ${\displaystyle {}^{A}B}$) denote the class of relations ${\displaystyle f}$ that are total functional, i.e. ${\displaystyle f\subset A\times B}$ with ${\displaystyle \forall (c\in A).\exists$ !(d\in B).\langle c,d\rangle \in f} . With this, we consider the axiom Exp:

• Exponentiation

${\displaystyle \forall x.\forall y.\ \ \exists h.h=y^{x}}$

In words, the axioms says that given two sets ${\displaystyle x,y}$, the class ${\displaystyle y^{x}}$ of all functions is, in fact, also a set.

Assuming LEM for bounded formulas, the characteristic functions and Separation let one demonstrate that any powerset is the set. Alternatively, full Powerset is also implied by merely assuming that the class of all subsets of ${\displaystyle \top }$ forms a set.

When functions are understood as just function graphs, the membership proposition ${\displaystyle f\in B^{A}}$ is also written ${\displaystyle f\colon A\to B}$. In type theory, the expression "${\displaystyle A\to B}$" exists on its own and denotes function spaces, a primitive notion. Thus, in that context, functions are more readily studied than classes of subsets. As with exponential objects resp. subobjects in category theory. These sets naturally appear, for example, as the type of the currying bijection given by the adjunction ${\displaystyle ((z\times x)\to y)\cong (z\to y^{x})}$. Constructive set theories are also studied in the context of applicative axioms.

Secondly, we consider a full induction scheme for sets

• Axiom schema of Set induction

For any predicate ${\displaystyle \phi }$:

${\displaystyle (\forall y.\forall (x\in y).\phi (x)\implies \phi (y))\implies \forall z.\phi (z)}$

This axiom is also studied just for bounded formulas. Naturally, full Set Induction implies full mathematical induction over the natural numbers. Replacement is not required to prove induction over the set of naturals, but it is for their arithmetic modeled within the set theory.

The Axiom of Regularity together with (bounded) Separation implies set induction but also (bounded) LEM, so Regularity is non-constructive. Conversely, LEM together with set induction implies Axiom of regularity.

Metalogic

This now covers all of the Zermeolo-Freankel axioms, but without full Separation, full Regularity, full Powerset and of course without the law of excluded middle. The theory ECST+Exp is not stronger than Heyting arithmetic but adding LEM at this stage would lead to a theory beyond the strength of typical type theory:

Adding LEM to ECST+Exp and full Separation gives a theory proving the same theorems as ZF minus Regularity! Thus, adding LEM to these axioms gives ZF. Similarly, adding the Axiom of Choice to the axioms gives ZFC.

The added proof-theoretical strength attained with induction in the constructive context is significant, even if dropping Regularity in the context of ZF does not reduce the proof-theoretical strength. Note that Aczel was also one of the main developers or Non-well-founded set theory, which contradicts rejects this last axiom.

CZFE

With all the weakened axioms of ZF and now going beyond those axioms also seen in Myhill's typed approach, the theory called CZFE (a theory with Exponentiation) strengthens the collection scheme as follows:

• Axiom schema of strong collection

For any predicate ${\displaystyle \phi }$:

${\displaystyle \forall a.\ \ [\forall (x\in a).\exists y.\phi (x,y)]\implies [\exists b.(\forall (x\in a).\exists (y\in b).\phi (x,y))\wedge (\forall (y\in b).\exists (x\in a).\phi (x,y))]}$

This is a stronger alternative for the Replacement scheme in terms of binary relations. It states that if ${\displaystyle \phi }$ is a relation between sets which is total over a certain domain set (that is, it has at least one image of every element in the domain), then there exists a set which contains at least one image under ${\displaystyle \phi }$ of every element of the domain (and only such images of elements of the domain).

In CZFE one can reason about shrinking interval sequences in ${\displaystyle ({\mathbb {Q} }\times {\mathbb {Q} })^{\mathbb {N} }}$ and large portion of standard math can be developed in this theory. However, in this context the standard construction of the Dedekind class is still not leading to a set. So the theory does not formally show the set of Cauchy reals to be equivalent to the class of Dedekind reals. This is indeed known to be provable using LEM or countable choice.

As a rule, questions of moderate cardinality are more subtle in a constructive setting. As arithmetic is well available in CZFE, the theory has dependent products, proves that the set of all subsets of natural numbers is not subcountable and also proves that countable unions of function spaces of countable sets remain countable.

Metalogic

This theory without LEM, unbounded separation and "naive" Power set enjoys various nice properties. For example, 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 ZFC, the Axiom of Choice implies the Well-ordering theorem, so that total orderings with least element for 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 CZF is CZFE 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.(\forall (x\in a).\exists (y\in b).\phi (x,y,z)\implies \exists (v\in u).[\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)])}$

This Subset Collection axiom scheme is equivalent to a single and somewhat clearer alternative Axiom of Fullness. It states that between any two sets a and b, there is a set c which contains a total sub-relation of any total relation from a to b that can be encoded as a set of ordered pairs. Formally, using a class that is syntactic sugar, one can express this as follows.

• (Fullness, an alternative to Subset Collection)

${\displaystyle \forall a.\forall b.\ \ \exists (c\subseteq a\Sigma {b}).\forall (r\in a\Sigma {b}).\exists (s\in c).s\subseteq r}$

Here ${\displaystyle a\Sigma {b}}$ is the class of all total relations between a and b. With a typical set encoding of the ordered pair ${\displaystyle \langle x,y\rangle }$ is assumed, this class is given as

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

The Fullness axiom is in turn implied by the so called Presentation Axiom about sections, which can also be formulated category theoretically. Indeed theories beyond ECST are related to predicative topoi.

Linearity of ordinals, nor existence of power sets of finite sets are still not proven in this theory and assuming either implies Power set in this context.

Metalogic

This theory lacks the existence property due to the Schema, but in 1977 Aczel showed that 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 CZF in type theory.[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. As such, CZF has modest proof theoretic strength, see IKP: Bachmann–Howard ordinal.

Breaking with ZF

One may further add the non-classical axiom that all sets are subcountable, and this then logically rejects Powerset and LEM.

In 1989 Ingrid Lindström showed that non-well-founded sets obtained by replacing the equivalent of the Axiom of Foundation (Induction) in CZF with Aczel's anti-foundation axiom (CZFA) can also be interpreted in Martin-Löf type theory.[6]

Intuitionistic Zermelo–Fraenkel

The theory IZF is CZF with the standard Separation and Power set.

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

• Axiom schema of collection

${\displaystyle \forall z.[\forall (x\in z).\exists y.\phi (x,y)]\implies \exists w.\forall (x\in z).\exists (y\in w).\phi (x,y)}$

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

As such, IZF can be seen as the most straight forward variant of ZF without LEM.

Metalogic

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

Even without LEM, the proof theoretic strength of IZF equals that of ZF.

While IZF 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 LEM, 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, ZFC, and throwing away the Axiom of choice (AC) and the law of the excluded middle (LEM), leaving everything else as is. However, different forms of some of the ZFC axioms which are equivalent in the classical setting are inequivalent in the constructive setting, and some forms imply LEM. In those cases, the intuitionistically weaker formulations were then adopted for the constructive set theory.

Intuitionistic KP

Let us mention another very weak theory that has been investigated, namely Intuitionistic (or constructive) Kripke–Platek set theory IKP. The theory has not only Separation but also Collection restricted, i.e. it is similar to 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 CST is a constructive first-order logic with identity and three sorts, namely sets, natural numbers, functions:

• 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 in classical set theory, requiring that any quantifications be bounded to another set.
• A form of the Axiom of infinity asserting that the collection of natural numbers (for which he introduces a constant N) 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.
• An Axiom of dependent choice, which is much weaker than the usual Axiom of choice.

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.

See also

• Constructive mathematics
• Intuitionistic type theory
• Ordinal analysis
• Impredicativity
• Existence Property
• Law of excluded middle
• Subcountability

References

1. Peter Aczel and Michael Rathjen, Notes on Constructive Set Theory, Reports Institut Mittag-Leffler, Mathematical Logic - 2000/2001, No. 40
2. 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.
3. Scott, D. S. (1985). Category-theoretic models for Intuitionistic Set Theory. Manuscript slides of a talk given at Carnegie-Mellon University
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

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

• Laura Crosilla, Set Theory: Constructive and Intuitionistic ZF, Stanford Encyclopedia of Philosophy, Feb 20, 2009
• Benno van den Berg, Constructive set theory – an overview, slides from Heyting dag, Amsterdam, 7 September 2012