Thanks to Andrzej Trybulec, as well as Czeslaw Bylinski, Grzegorz Bancerek and Roman Matuszewski, for many interesting discussions and for looking after me during my visit to Bialystok, where this paper was started. For making this and other meetings of researchers possible, Bob Boyer deserves every credit; I am grateful too for his encouragement to write this paper. I have also benefited from conversations with Mike Gordon and with other people at the QED conference, and with members of the Programming Methodology group at Åbo Akademi. My visit to Poland was funded by the U.S. Office of Naval Research, and my later work was supported by the U.K. Physical Sciences and Engineering Research Council, the Isaac Newton Trust, and more recently by the European Commission under the Human Capital and Mobility programme. Comments on early drafts from Rob Arthan, Jim Grundy, Ken Kunen, Witold Marciszewski, Norm Megill, Larry Paulson, Randy Pollack and Piotr Rudnicki have led to several important improvements and corrections; I am also grateful for encouraging reactions from many others. Thanks also to Roger Jones for undertaking an HTML translation of an earlier version of this paper and to Witold Marciszewski for arranging electronic publication in Mathesis Universalis.⁵²

John Harrison 96/8/13; HTML by 96/8/16