×

Lorenzen and constructive mathematics. (English) Zbl 1490.03001

Heinzmann, Gerhard (ed.) et al., Paul Lorenzen – mathematician and logician. Contributions presented at the workshop, Konstanz, Germany, March 8–9, 2018. Cham: Springer. Log. Epistemol. Unity Sci. 51, 47-61 (2021).
The paper is devoted to P.Lorenzen’s contributions to constructive mathematics showing their influence on recent developments in mathematical logic and constructive algebra. The author also presents some results in measure theory connected to Lorenzen’s work. In particular the author discusses Lorenzen’s research on Gentzen’s logic, e.g., his modification of Grentzen’s consistency proof “as a proof about an infinitary cut-free calculus showing that the cut rule is admissable” (p.48) and later contributions using, e.g., inductive definitions “quantifying only over the (denumerable) totality of sets previously obtained” (p.49). The author also discusses Lorenzen’s inversion principle and his research on applying proof theory to distributive lattices using the concept of an entailment relation. Other topics concern Lorenzen’s proof-theoretic analysis of point free spaces. In respect to measure theory the author discusses Lorenzen’s contributions on Borel subsets of Cantor spaces. This is applied to an inductive solution of Borel’s measure problem. The short final section of the paper hints at Lorenzen’s game semantics. The author shows that these contributions inspired recent research in these fields.
For the entire collection see [Zbl 1470.03010].

MSC:

03-03 History of mathematical logic and foundations
03F50 Metamathematics of constructive systems
03F60 Constructive and recursive analysis
01A60 History of mathematics in the 20th century
01A70 Biographies, obituaries, personalia, bibliographies
03A05 Philosophical and critical aspects of logic and foundations
03F03 Proof theory in general (including proof-theoretic semantics)
03F45 Provability logics and related algebras (e.g., diagonalizable algebras)
06-03 History of ordered structures
28-03 History of measure and integration

Biographic References:

Lorenzen, Paul
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] 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. · Zbl 0143.25502
[2] 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. · Zbl 0134.01201
[3] 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). · JFM 56.0356.01
[4] 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. · Zbl 1512.03073 · doi:10.1080/01445340.2020.1752034
[5] 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. · JFM 48.1121.01
[6] Artin, E., & Schreier, O. (1927). Eine Kennzeichnung der reell abgeschlossenen Körper. Abhandlungen aus dem Mathematischen Seminar der Universität Hamburg, 5, 225-231. · JFM 53.0144.01 · doi:10.1007/BF02952522
[7] Aschieri, F. (2017). Game semantics and the geometry of backtracking: A new complexity analysis of interaction. Journal of Symbolic Logic, 82(2), 672-708. · Zbl 1401.03100 · doi:10.1017/jsl.2016.48
[8] 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. · Zbl 1063.03537
[9] Beth, E. W. (1959). The foundations of mathematics: A study in the philosophy of science. Amsterdam: North-Holland. · Zbl 0085.24104
[10] Borel, É. (1894). Sur quelques points de la théorie des fonctions. Gauthier-Villars. · JFM 25.0705.02
[11] Buchholz, W., & Schütte, K. (1988). Proof theory of impredicative subsystems of analysis. Naples: Bibliopolis. · Zbl 0653.03039
[12] 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. · Zbl 0948.03056
[13] 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. · Zbl 1476.03035
[14] Cockx, J. (2017). Dependent pattern matching and proof-relevant unification.Ph.D. thesis, KU Leuven.
[15] Coquand, T. (1995). A semantics of evidence for classical arithmetic. Journal of Symbolic Logic, 60(1), 325-337. · Zbl 0829.03037 · doi:10.2307/2275524
[16] Coquand, T. (2004). A note on measures with values in a partially ordered vector space. Positivity, 8(4), 395-400. · Zbl 1065.28006 · doi:10.1007/s11117-004-7399-0
[17] 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. · Zbl 1496.06018 · doi:10.1216/rmj-2019-49-5-1449
[18] Coquand, T., & Persson, H. (2001). Valuations and Dedekind’s Prague theorem. Journal of Pure and Applied Algebra, 155(2-3), 121-129. · Zbl 0983.11061 · doi:10.1016/S0022-4049(99)00095-X
[19] Curry, H. B. (1976). Foundations of mathematical logic. Dover. · Zbl 0163.24209
[20] Feferman, S. (1964). Systems of predicative analysis. Journal of Symbolic Logic, 29, 1-30. · Zbl 0134.01101 · doi:10.2307/2269764
[21] Feferman, S. (1977). Review of Proof theory by G. Takeuti. Bulletin of the American Mathematical Society, 83(3), 351-361.
[22] 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. · Zbl 1252.03134
[23] Johnstone, P. T. (1982). Stone spaces. Cambridge studies in advanced mathematics (Vol. 3). Cambridge: Cambridge University Press. · Zbl 0499.54001
[24] 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. · Zbl 0635.68007
[25] 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.
[26] Lorenzen, P. (1951a). Algebraische und logistische Untersuchungen über freie Verbände. Journal of Symbolic Logic, 16, 81-106. http://www.jstor.org/stable/2266681. Translation by S. Neuwirth: Algebraic and logistic investigations on free lattices, http://arxiv.org/abs/1710.08138. · Zbl 0045.29502
[27] Lorenzen, P. (1951b). Über endliche Mengen. Mathematische Annalen, 123, 331-338. · Zbl 0042.28001 · doi:10.1007/BF02054956
[28] Lorenzen, P. (1953). Die Erweiterung halbgeordneter Gruppen zu Verbandsgruppen. Mathematische Zeitschrift, 58, 15-24. · Zbl 0051.25302 · doi:10.1007/BF01174126
[29] Lorenzen, P. (1955). Einführung in die operative Logik und Mathematik. Berlin: · Zbl 0066.24802 · doi:10.1007/978-3-662-01539-1
[30] Lorenzen, P. (1958). Logical reflection and formalism. Journal of Symbolic Logic, 23(3), 241-249. · Zbl 0086.00902 · doi:10.2307/2964281
[31] 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.
[32] Lorenzen, P., & Myhill, J. (1959). Constructive definition of certain analytic sets of numbers. Journal of Symbolic Logic, 24(1), 37-49. · Zbl 0091.01303 · doi:10.2307/2964572
[33] Lusin, N. (1930). Leçons sur les ensembles analytiques et leurs applications. Paris: Gauthier-Villars. · JFM 56.0085.01
[34] Martin-Löf, P. (1968). Notes on constructive mathematics. Stockholm: Almqvist & Wiksell. · Zbl 0273.02021
[35] 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. · doi:10.1007/978-3-7643-8653-5_15
[36] Neuwirth, S. (2020). Lorenzen’s reshaping of Krull’s Fundamentalsatz for integral domains (1938-1953). In this volume (pp. 141-180).
[37] Novikov, P. S. (1943). On the consistency of a certain logical calculus. Matematičeskij sbornik / Recueil mathématique, 12(54), 230-260.
[38] Peirce, C. S. (1885). On the algebra of logic: A contribution to the philosophy of notation. American Journal of Mathematics, 7(2), 180-202. · JFM 17.0044.02 · doi:10.2307/2369451
[39] Roquette, P. (2018). The Riemann hypothesis in characteristic p in historical perspective. Cham: Springer. · Zbl 1414.11003
[40] Schröder, E. (1890-1910). Vorlesungen über die Algebra der Logik(Vols. i-iii). Reprint Chelsea 1966. · Zbl 0188.30703
[41] Zeilberger, N. (2009). The logical basis of evaluation order and pattern-matching.Ph.D. thesis, Carnegie-Mellon University
[42] 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. · Zbl 0093.01401
[43] 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. · Zbl 0723.68028 · doi:10.1093/logcom/1.2.261
[44] Coquand, T. (1992). Pattern matching with dependent types. Informal Proceedings of Logical Frameworks, 66-79. https://doi.org/10.1.1.37.9541.
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.