Demonstrations Versus Proofs, Being an Afterword to Constructions, Proofs, and the Meaning of the Logical Constants

  • Göran SundholmEmail author
Part of the Logic, Epistemology, and the Unity of Science book series (LEUS, volume 31)


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-Löf, 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.


Type Theory Sequent Calculus Philosophical Logic Existential Quantifier Construction Object 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. Beeson, Michael. 1979. A Theory of Constructions and Proofs. Preprint No. 134. Dept. of Mathematics, Univ. of Utrecht.Google Scholar
  2. Diller, J., and A. Troelstra. 1984. Realizability and intuitionistic logic. Synthese 60: 253–282.CrossRefGoogle Scholar
  3. Gentzen, G. 1936. Die Widerspruchsfreihet der reinen Zahlentheorie. Mathematische Annalen 112: 493–565.CrossRefGoogle Scholar
  4. Kreisel, G. 1962. Foundations of Intuitionistic Logic. In Logic, Methodology and Philosophy of Science, eds. Nagel, Suppes and Tarski, 198–210. Stanford: Stanford Univ. Press.CrossRefGoogle Scholar
  5. Martin-Löf, Per. 1982. Constructive mathematics and computer programming. In Logic, methodology and philosophy of science VI, Hannover 1979, ed. L.J. Cohen et al., 153–175. Amsterdam: North-Holland.CrossRefGoogle Scholar
  6. Martin-Löf, Per. 1984. Intuitionistic type theory. Naples: Bibliopolis.Google Scholar
  7. Martin-Löf, Per. 1985. On the meanings of the logical constants and the justifications of the logical laws. Lectures delivered in Siena 1983, first distributed in 1985, and printed in Nordic Journal of Philosophical Logic I, 1996, 11–60.Google Scholar
  8. Martin-Löf, Per. 1994. Analytic and synthetic judgements in type theory. In Kant and contemporary epistemology, ed. P. Parrini, 87–99. Dordrecht: Kluwer.CrossRefGoogle Scholar
  9. Mulligan, Kevin, Peter Simons, and Barry Smith. 1984. Truth-makers. Philosophy and Phenomenological Research 44: 287–321.CrossRefGoogle Scholar
  10. Sundholm, Göran. 1990. Sätze der Logik: An alternative conception. In Wittgenstein – Towards a re-evaluation, Proceedings 14th International Wittgenstein Symposium, Kirchberg am Wechsel, 13–20 August 1989, ed. Rudolf Haller and J. Brandl, 59–61. Wien: Verlag Hölder-Pichler-Tempsky.Google Scholar
  11. Sundholm, Göran. 1993. Questions of proof. Manuscrito (Campinas) 16: 47–70.Google Scholar
  12. Sundholm, Göran. 1994a. Existence, proof and truth-making: A perspective on the intuitionist conception on truth. Topoi 13: 117–126.CrossRefGoogle Scholar
  13. Sundholm, Göran. 1994b. Ontologic versus epistemologic: Some strands in the development of logic, 1837–1957. In Logic and philosophy of science in Uppsala, ed. Dag Prawitz and Dag Westerståhl, 373–384. Dordrecht: Kluwer.Google Scholar
  14. Sundholm, Göran. 1997. Implicit epistemic aspects of constructive logic. Journal of Logic, Language and Information 6: 191–212.CrossRefGoogle Scholar
  15. Sundholm, Göran. 2004. Antirealism and the roles of truth. In Handbook of epistemology, ed. I. Niniluoto, M. Sintonen, and J. Wolenski, 437–466. Dordrecht: Kluwer.Google Scholar
  16. Sundholm, Göran. 2006. Semantic values of natural deduction derivations. Synthese 148: 623–638.CrossRefGoogle Scholar
  17. Sundholm, Göran. 2009. A century of judgment and inference: 1837–1936’. In The development of modern logic, ed. L. Haaparanta, 262–317. Oxford: Oxford University Press.Google Scholar
  18. Sundholm, Göran. 2012. Error. Topoi 31(1): 87–92.CrossRefGoogle Scholar
  19. Sundholm, Göran, and Mark van Atten. 2008. The proper explanation of intuitionistic logic: On Brouwer’s demonstration of the Bar theorem. In One hundred years of intuitionism (1907–2007), ed. M. van Atten, P. Boldini, G. Heintzmann, and M. Bordeau, 60–77. Birkhäuser: Basel.CrossRefGoogle Scholar
  20. Tait, W.W. 2006. Gödel’s interpretation of intuitionism. Philosophia Mathematicae (III) 14: 208–228.CrossRefGoogle Scholar
  21. Weinstein, Scott. 1983. The intended interpretation of intuitionistic logic. Journal of Philosophical Logic 12: 216–270.CrossRefGoogle Scholar

Copyright information

© Springer Science+Business Media Dordrecht 2013

Authors and Affiliations

  1. 1.Faculty of PhilosophyLeiden UniversityLeidenThe Netherlands

Personalised recommendations