Constructive mathematics : its set theory and practice

• Main Author: Bridges, Douglas Sutherland
• Published: University of Oxford 1974
• Subjects: 510
• Online Access: http://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.479993

The thesis falls naturally into two parts, in the first of which (comprising Chapter 1) there is laid down a set-theoretic foundation for constructive mathematics as understood by Errett Bishop and his followers. The work of this part closely follows the lines of the corresponding classical development of set theory by Anthony Morse, highlights several classical definitions and results which are inadequate for a proper description of constructive mathematics, and develops constructive replacements for these where possible; of particular importance is the constructive proof of a general recursion theorem, from which the familiar theorems of simple and primitive recursion readily follow. The second part of the thesis (Chapters 2-5) is concerned with various problems of constructive analysis, the link between these problems being their involvement with compactness or local compactness at some stage. Chapter 2 serves as an introduction to this analysis, and includes the definition of metric injectiveness and the proof of a constructive substitute for the classical result that a continuous injection of a compact Hausdorff space onto a Hausdorff space has continuous inverse. In Chapter 3 we give an improved definition of one-point compactification of a locally compact space, and then develop the theory of existence and essential uniqueness of such compactifications of a given space. In turn, this is applied in Chapter 4, which deals in full with the space of continuous, complex-valued functions which vanish at infinity on a locally compact space, and with star homomorphisms between such spaces; interpolated within the main body of this chapter is the vital Backward Uniform Continuity Theorem, which leads to a discussion of possible constructive substitutes for the classical Uniform Continuity Theorem. The final chapter deals with constructive substitutes for various topologies associated with spaces of bounded linear mappings between normed linear spaces. The main results of this chapter concern the weak operator topology on the space Hom(H,H) of bounded linear operators on a Hilbert space H, and include a constructive proof of the weak operator precompactness of the unit ball of Hom(H,H), and a proof that the compactness of this ball is an essentially non-constructive proposition. The chapter ends with a discussion of linear functionals and the weak operator topology on Hom(H,H), and a partial substitute for the classical characterisa- of ultraweakly continuous linear functionals on a linear subset of Hom(H,H). In addition, there are five appendices, three of which develop material arising from that in the main body of the thesis. In the first of these three, we describe an axiomatic theory of proofs within the formal system of Chapter 1, and derive (amongst other results) a very satisfactory characterisation of proofs of 'p → q'; the second deals with connectedness, and builds up to a constructive proof that a closed ball in finite dimensional Banach space is connected; finally, the last makes a remark on metric injectiveness in the light of a conjecture in Chapter 2.