Morse Set Theory as a Foundation for Constructive Mathematics

Douglas Bridges, University of Canterbury. Part of the proofs, constructions and computations seminar series.

In the northern autumn of 1972, I came across A.P. Morse's little book 'A Theory of Sets', and became absorbed by the idea of carrying through a constructive development of set theory (CMST) along the same lines, in which everything was expressed in a kind of pseudocode governed by strict rules of language and notation. Such a development would seem to be particularly suitable for the extraction of programs from proofs and for their subsequence implementation.

Chapter 1 of my D.Phil. thesis (Oxford, 1974) contained the fruits of my labours to that stage. After that, despite a brief foray into CMST for a conference paper in 1986, my plan to develop the set theory in greater depth was shelved until taken up again in the autumn of 2013.

In this talk I sketch some of the salient features of the substantially updated development of CMST over the last three-and-a-half years, paying particular attention to where the constructive theory deviates from Morse's classical counterpart and to those results of the latter that are essentially nonconstructive.

Douglas Bridges, University of Canterbury