×
Klev, Ansten

Spiritus asper versus lambda: on the nature of functional abstraction. (English) Zbl 07720263

Notre Dame J. Formal Logic 64, No. 2, 205-223 (2023).
Summary: The spiritus asper as used by Frege in a letter to Russell from 1904 bears resemblance to Church’s lambda. It is natural to ask how they relate to each other. An alternative approach to functional abstraction developed by Per Martin-Löf some thirty years ago allows us to describe the relationship precisely. Frege’s spiritus asper provides a way of restructuring a unary function name in Frege’s sense such that the argument place indicator occurs all the way to the right. Martin-Löf’s alternative approach shows that this is only half of what lambda does. The other half is the deletion of the argument place indicator, resulting in what Frege would have called an isolated function name.

MSC:

03A05 Philosophical and critical aspects of logic and foundations
00A30 Philosophy of mathematics
03B40 Combinatory logic and lambda calculus
03B38 Type theory

Keywords:

functional abstraction; Gottlob Frege; typed lambda calculus

Software:

Automath
Cite Review PDF
Full Text: DOI

References:

[1] Abadi, M., L. Cardelli, P.-L. Curien, and J.-J. Lévy, “Explicit substitutions,” Journal of Functional Programming, vol. 1 (1991), pp. 375-416. · Zbl 0941.68542 · doi:10.1017/S0956796800000186
[2] Aspinall, D., and M. Hofmann, “Dependent types,” pp. 45-86 in Advanced Topics in Types and Programming Languages, edited by B. C. Pierce, MIT Press, Cambridge, MA, 2005.
[3] Bentzen, B., “Frege’s theory of types,” preprint, arXiv.2006.16453v2 [math.HO]. · Zbl 1451.03009
[4] Carnap, R., Abriss der Logistik, Springer, Vienna, 1929. · JFM 55.0030.06
[5] Church, A., “A formulation of the simple theory of types,” Journal of Symbolic Logic, vol. 5 (1940), pp. 56-68. · JFM 66.1192.06 · doi:10.2307/2266170
[6] Church, A., Introduction to Mathematical Logic, I, Princeton University Press, Princeton, 1956. · Zbl 0073.24301
[7] Curry, H. B., and R. Feys, Combinatory Logic, vol. 1 of Studies in Logic and the Foundations of Mathematics, North-Holland, Amsterdam, 1958. · Zbl 0081.24104
[8] de Bruijn, N. G., “A survey of the project AUTOMATH,” pp. 579-606 in To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, edited by J. R. Hindley and J. P. Seldin, Academic Press, London, 1980.
[9] de Bruijn, N. G., “On the roles of types in mathematics,” pp. 27-54 in The Curry-Howard Isomorphism, edited by P. de Groote, vol. 8 of Cahiers du Centre de Logique, Academia, Louvain-la-Neuve, 1995. · Zbl 0977.03504
[10] Dedekind, R., Was sind und was sollen die Zahlen?, Vieweg, Braunschweig, 1888. · JFM 36.0087.04
[11] Euler, L., Introductio in analysin infinitorum, Bousquet, Lausanne, 1748. · Zbl 0096.00303
[12] Frege, G., Begriffsschrift, Louis Nebert, Halle, 1879.
[13] Frege, G., Funktion und Begriff, Hermann Pohle, Jena, 1891.
[14] Frege, G., Grundgesetze der Arithmetik, I, Hermann Pohle, Jena, 1893. · JFM 25.0101.02
[15] Frege, G., Grundgesetze der Arithmetik, II, Hermann Pohle, Jena, 1903. · JFM 34.0071.05
[16] Frege, G., “Was ist eine Funktion?,” pp. 656-66 in Festschrift Ludwig Boltzmann: Gewidmet zum sechzigsten Geburtstage, Johann Ambrosius Barth, Leipzig, 1904. · JFM 35.0977.01
[17] Frege, G., Wissenschaftlicher Briefwechsel, Felix Meiner, Hamburg, 1976. · Zbl 0341.01019
[18] Klement, K. C., “Russell’s 1903-1905 anticipation of the lambda calculus,” History and Philosophy of Logic, vol. 24 (2003), pp. 15-37. · Zbl 1044.03002 · doi:10.1080/0144534031000076237
[19] Klev, A., “A comparison of type theory with set theory,” pp. 271-92 in Reflections on the Foundations of Mathematics, edited by S. Centrone, D. Kant, and D. Sarikaya, vol. 407 of Synthese Library, Springer, Cham, 2019. · Zbl 1528.03109 · doi:10.1007/978-3-030-15655-8_12
[20] Klev, A., “Eta-rules in Martin-Löf type theory,” Bulletin of Symbolic Logic, vol. 25 (2019), pp. 333-59. · Zbl 1486.03028 · doi:10.1017/bsl.2019.21
[21] Klev, A., “The name of the sinus function,” pp. 149-59 in Logica Yearbook 2018, edited by I. Sedlár and M. Blicha, College Publications, London, 2019. · Zbl 1505.03032
[22] Martin-Löf, P., “About models for intuitionistic type theories and the notion of definitional equality,” pp. 81-109 in Proceedings of the Third Scandinavian Logic Symposium (Uppsala, 1973), edited by S. Kanger, vol. 82 of Studies in Logic and the Foundations of Mathematics, North-Holland, Amsterdam, 1975. · Zbl 0334.02017
[23] Martin-Löf, P., “An intuitionistic theory of types: Predicative part,” pp. 73-118 in Logic Colloquium ’73 (Bristol, 1973), edited by H. E. Rose and J. C. Shepherdson, vol. 80 of Studies in Logic and the Foundations of Mathematics, North-Holland, Amsterdam, 1975. · Zbl 0334.02016
[24] Martin-Löf, P., Intuitionistic Type Theory, Bibliopolis, Naples, 1984. · Zbl 0571.03030
[25] Martin-Löf, P., “Philosophical aspects of intuitionistic type theory,” transcript of a lecture course given at Leiden University, Leiden, Netherlands, 1993. Published at https://pml.flu.cas.cz.
[26] Martin-Löf, P., “Comments on Prof. Kazuyuki Nomoto’s paper,” Annals of the Japan Association for Philosophy of Science, vol. 14 (2006), pp. 98-99. · Zbl 1111.03006 · doi:10.4288/jafpos1956.14.98
[27] Martin-Löf, P., “The sense/reference distinction in constructive semantics,” Bulletin of Symbolic Logic, vol. 27 (2021), pp. 501-13. · Zbl 1529.03066 · doi:10.1017/bsl.2021.61
[28] Nomoto, K., “The methodology and structure of Gottlob Frege’s logico-philosophical investigations,” Annals of the Japan Association for Philosophy of Science, vol. 14 (2006), pp. 73-99. · Zbl 1111.03007 · doi:10.4288/jafpos1956.14.73
[29] Russell, B., “Mathematical logic as based on the theory of types,” American Journal of Mathematics, vol. 30 (1908), pp. 222-62. · JFM 39.0085.03 · doi:10.2307/2369948
[30] Russell, B., Foundations of Logic 1903-05, vol. 4 of The Collected Papers of Bertrand Russell, edited by A. Urquhart, Routledge, London, 1994. · Zbl 1066.01519
[31] Schönfinkel, M., “Über die Bausteine der mathematischen Logik,” Mathematische Annalen, vol. 92 (1924), pp. 305-16. · JFM 50.0023.01 · doi:10.1007/BF01448013
[32] Scott, D., “Some philosophical issues concerning theories of combinators,” pp. 346-66 in λ-Calculus and Computer Science Theory (Rome, 1975), edited by C. Böhm, vol. 37 of Lecture Notes in Computer Science, Springer, Berlin, 1975. · Zbl 0342.02019
[33] Simons, P., “Functional operations in Frege’s Begriffsschrift,” History and Philosophy of Logic, vol. 9 (1988), pp. 35-42. · Zbl 0643.03003 · doi:10.1080/01445348808837123
[34] Simons, P., “Abstraction, structure, and substitution: Lambda and its philosophical significance,” Polish Journal of Philosophy, vol. 1 (2007), pp. 81-100. · doi:10.5840/pjphil20071122
[35] Simons, P., “Double value-ranges,” pp. 167-81 in Essays on Frege’s “Basic Laws of Arithmetic”, edited by P. A. Ebert and M. Rossberg, Oxford University Press, Oxford, 2019. · Zbl 1465.03021 · doi:10.1093/oso/9780198712084.003.0007
[36] Sundholm, B. G., “Implicit epistemic aspects of constructive logic,” Journal of Logic, Language, and Computation, vol. 6 (1997), pp. 191-212. · Zbl 0873.03003 · doi:10.1023/A:1008266418092
[37] Sundholm, B. G., “ ‘Inference versus consequence’ revisited: Inference, consequence, conditional, implication,” Synthese, vol. 187 (2012), pp. 943-56. · Zbl 1275.03061 · doi:10.1007/s11229-011-9901-0
[38] Wittgenstein, L., Tractatus Logico-Philosophicus, Routledge, London, 1922. · JFM 48.1128.13
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.