Demonstrations versus proofs, being an afterword to constructions, proofs, and the meaning of the logical constants

Abstract

The spring of 1980 I spent as visiting lecturer at Utrecht. The volume of Heyting’s Collected Papers. had not yet been put together, and his philosophical papers could not be found at Oxford. Accordingly, I availed myself of the opportunities offered by Dutch libraries and read the relevant papers. A couple of years earlier, I had learned about Constructive Type Theory from Per Martin-Lof, and Michael Beeson, who had just written a paper on a theory of constructions, was an eager sparring partner in almost daily discussions at Utrecht. The outcome of these ponderings was this chapter on which you are reading now as an afterword. It was ready toward the end of the summer 1981, and my Oxford Professor Dana Scott suggested to me that I should submit it to Richmond Thomason, the editor of the Journal of Philosophical Logic ., at a meeting of authors for the Handbook of Philosophical Logic. at Bad Homburg. I did so and the paper was readily accepted; however, a special issue on intuitionism was being prepared, and Thomason suggested that I might want to wait in order to have it appear in that issue. Thus, the paper appeared only in 1983 but had circulated rather widely in the intervening time.