Constructive Set Theory - Myhill's Constructive Set Theory

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. 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 function in cases where the choice is already made. Together these act like the usual replacement axiom in classical set theory.
• 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.
• 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.