Douglas S. Bridges: Morse Set Theory as a Foundation for Constructive Mathematics
Time: Wed 2015-01-14 10.00 - 11.45
Location: Room 16, building 5, Kräftriket, Department of mathematics, Stockholm university
Participating: Douglas S. Bridges, University of Canterbury, Christchurch, New Zealand
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 proof-checking and for the extraction of programs from proofs. 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 late last year.
In this talk I sketch some of the salient features of this updated development of CMST, paying particular attention to where it deviates from Morse's classical theory and to those results of the latter that are essentially nonconstructive.