Notes to Set Theory: Constructive and Intuitionistic ZF

1. Note that one could also choose to leave out foundation (and set-induction) altogether. One may then wish to add an axiom, called antifoundation, which allows for the formation of non-well-founded sets, also called hypersets (see Aczel 1988 or Barwise and Moss 1996). In fact, a constructive treatment of non-well-founded sets can be given which mirrors the classical one (see for example Rathjen 2004). Further, by using a construction by Hällnas and Lindström of non-well-founded sets as limits of finite approximations (Lindström 1989), one can see that in constructive contexts the antifoundation axiom comes as proof-theoretically “inexpensive” if compared with set induction (Rathjen 2003).

2. In the practice of constructive type and set theory stronger and stronger principles have been introduced which are considered by the practitioners of the field to be predicatively justifiable (see the section on Large sets in constructive and intuitionistic ZF). In our opinion, despite the great technical achievements we still lack clear criteria for the assessment of the constructive predicativity of extensions of foundational systems for constructive mathematics (see Rathjen 2005a for a discussion touching upon this point).

3. We remark that the axiom of choice also holds in so-called “extensional” type theories like the one of (Martin-Löf 1984), as they retain some intensional features which ensure the validity of the Curry-Howard correspondence. Note, however, that the presence of a form of intensionality is no guarantee for the validity of the axiom of choice. In Feferman's explicit mathematics (see Feferman 1975), where a different kind of intensionality occurs, the assumption of the axiom of choice gives rise to inconsistencies (note also that the standard argument makes use of self-reference, which is available in this theory).