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 and 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, constructive set theories often require some universal quantifiers 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 the law of excluded middle, i.e. that the disjunction 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. 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, 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. 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.

Subtheories of ZF

Axioms that are virtually always deemed uncontroversial and part of all theories considered in this article are are
and
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:
also called Bounded Separation, i.e. the Separation for bounded quantifiers only.
With the Replacement scheme, this theory proves that the Cartesian product of two sets,, is a set, and so are equivalence classes or indexed sums.

Metalogic

Constructive theories often have Axiom schema of Replacement. However, when other axioms are dropped, this schema is actually often strengthened - not beyond ZF, but instead merely to gain back some provability strength.
Replacement and the axiom of Set Induction suffices to axiomize hereditarily finite sets constructively and that theory is also studied without Infinity.
For comparison, the very weak classical theory interpreting the class of natural numbers and their arithmetic via just Extensionality, Adjunction and full Separation, see General set theory.

ECST

Let denote as usual and some fixed predicate.
Denote by the Inductive property, e.g..
The statement expresses that is the smallest set among all sets for which holds true.
The Elementary constructive Set Theory ECST has the axiom of BCST as well as
Other formulations of the axiom of infinity are possible as well.
In the program of Predicative Arithmetic, even the axiom scheme of induction for natural numbers, with its universal quantifiers has been criticized as possibly being impredicative, when natural numbers are defined as the object which fulfill this scheme. ECST has infinite objects but not Induction.

Metalogic

Replacement is not required to prove induction over the set of naturals, but it is for their arithmetic modeled within the set theory.
Nevertheless, despite having the Replacement axiom, ECST still does not proof the addition to be a set function and the theory does not interpret full primitive recursion yet.
But note that also here in ECST, many statement can be proven per individual set 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. In the next step, induction and Function spaces relate the theory to Peano arithmetic, or, more precisely, Heyting arithmetic.

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.
Let denote the class of relations that are functional, i.e. with with.
With this, we consider the axiom Exp:
In words, the axioms says that given two sets, the class of all functions is, in fact, also a set.
Recall that the class of all subsets of is related to the class of "characteristic functions" from to a two-element set. For classical sets, this is in bijection with the power set of , e.g.. We see that while the subset relation is concise to express in the language of set theory with its primitive symbol, statements involving functions needs some unpacking. Membership is also written, a primitive notion in type theory.
As with exponential objects and subobjects in category theory, function spaces are easier to realize than classes of subsets. These sets naturally appear, for example, as the type of the currying bijection given by the adjunction. Constructive set theories are also studied in the context of applicative axioms.
Even weaker forms of Exponentiation interpret Heyting arithmetic or provide tools to uniquely characterize a set of rationals, for example.
Finally, we consider an induction scheme for sets
The Axiom of regularity implies set induction but also 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 gives a theory proving the same theorems as ZF minus Regularity!
Thus, adding LEM to all the axioms listed so far gives ZF.
Similarly, adding the Axiom of Choice to the axioms listed so far 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 strengthens the collection scheme as follows:
This is a stronger alternative for the Replacement scheme in terms of binary relations. It states that if is a relation between sets which is total over a certain domain set, then there exists a set which contains at least one image under of every element of the domain.
In CZFE one can reason about shrinking interval sequences in 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, but CZFE 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, the theory proves that a set exist that has that property, i.e. if the theory proves the statement, then there is also a property that uniquely describes such a set instance.
I.e., the theory then also proves.
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 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:
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.
Here is the class of all total relations between a and b. With a typical set encoding of the ordered pair is assumed, this class is given as
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 is still not proven in this theory and assuming it 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, providing what is now seen a standard model of CZF in type theory.
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.
In 1989 Ingrid Lindström showed that non-well-founded sets obtained by replacing the equivalent of the Axiom of Foundation in CZF with Aczel's anti-foundation axiom can also be interpreted in Martin-Löf type theory.

Intuitionistic Zermelo–Fraenkel

As with CZF, the theory IZF has the usual axioms of Extensionality, Pairing, Union, Infinity and Set Induction.
However, IZF also has the standard Separation and Power set.
In place of the Axiom schema of replacement, we use the
While the axiom of replacement requires the relation φ to be functional over the set a, 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 taking the most common foundation, 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 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 Kripke–Platek set theory IKP.
It does not fit into the hierarchy as presented above, simply because it has Axiom schema of Set Induction from the start.
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.

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:
And furthermore: