Constructive set theory

Abstract

This paper is the third in a series collectively entitled Formal systems of intuitionistic analysis. The first two are [4] and [5] in the bibliography; in them I attempted to codify Brouwer's mathematical practice. In the present paper, which is independent of [4] and [5], I shall do the same for Bishop's book [1]. There is a widespread current impression, due partly to Bishop himself (see [2]) and partly to Goodman and the author (see [3]) that the theory of Gödel functionals, with quantifiers and choice, is the appropriate formalism for [1]. That this is not so is seen as soon as one really tries to formalize the mathematics of [1] in detail. Even so simple a matter as the definition of the partial function 1/x on the nonzero reals is quite a headache, unless one is prepared either to distinguish nonzero reals from reals (a nonzero real being a pair consisting of a real x and an integer n with ∣x∣ > 1/n) or, to take the Dialectica interpretation seriously, by adjoining to the Gödel system an axiom saying that every formula is equivalent to its Dialectica interpretation. (See [1, p. 19], [2, pp. 57–60] respectively for these two methods.) In more advanced mathematics the complexities become intolerable.