Constructive set theory
From Wikipedia, the free encyclopedia
Constructive set theory is an approach to mathematical constructivism following the program of axiomatic set theory. That is, it uses the usual first-order language of classical set theory, and although of course the logic is constructive, there is no explicit use of constructive types. Rather, there are just sets, thus it can look very much like classical mathematics done on the most common foundations, namely the Zermelo-Fraenkel axioms (ZFC).
Contents |
[edit] Intuitionistic Zermelo-Fraenkel
The most obvious approach is to take the most common foundation, ZFC, and throw away the axiom of choice (AC) and the law of the excluded middle (LEM), leaving everything else as is. This is called IZF, or Intuitionistic Zermelo-Fraenkel; ZF refers to ZFC without the axiom of choice.
Symbolically we might write IZF + LEM = ZF, ZF + AC = ZFC. But, as described in the axiom of choice article, adding AC back to IZF allows us to prove LEM, i.e. IZF + AC = ZFC. This is a good illustration of the fact that there is more than one way to remove something from a theory. (Which is ZFC - AC, ZF or IZF?) And in fact, by removing LEM from ZF, there are different formulations of IZF which take different statements of some of the axioms of ZF which are not constructively equivalent (that is, proofs of their equivalence in ZF are non-constructive).
[edit] Collection
Replacement is usually stated as Collection
[edit] Set induction
Foundation is usually stated in terms of set induction
[edit] Predicativity
While IZF is based on constructive 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 (compare Gödel universe). In the absence of it, the set of truth values is also considered impredicative.
[edit] Myhill's constructive set theory
The subject was begun by John Myhill to provide a formal foundation for Errett Bishop's program of constructive mathematics. As he presented it, Myhill's system CST is a constructive first-order logic with three sorts: natural numbers, functions, and sets. However this distinction from a system with only sets is only technical.[dubious — see talk page] The system is:
- Constructive first-order predicate logic with identity, and basic axioms related to the three sorts.
- The usual Peano axioms for natural numbers.
- The usual axiom of extensionality for sets, as well as one for functions, and the usual axiom of union.
- 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.
- 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 functions in case where the choice is already made. Together these acts like the usual replacement axiom in classical set theory.
- The axiom of exponentation, 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.
- 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.
- An axiom of dependent choice, which is much weaker than the usual axiom of choice.
[edit] Aczel's constructive Zermelo-Fraenkel
Peter Aczel's CZF is essentially IZF, dropping the power set axiom and adding two collection schemes which entail the axiom of exponentation, as well as restricting the separation axiom as in Myhill's CST.
