Article/Publication Details
Views: 1309

MARTIN-LÖF’S TYPE THEORУ: BETWEEN PHENOMENOLOGY AND ANALYTICAL PHILOSOPHY

Abstract
Martin-Löf’s type theory stems simultaneously from Frege and Russell’s logic-ontological ideas and Husserl’s phenomenology. The article examines this intermediate status of type theory using as examples Martin-Löf ’s syntactical-semantic method and the role of evidence and canonical objects in his approach. Martin-Löf borrows the syntactical-semantic method from Frege and extends it drawing on Husserl’s theory of meaning. In type theory this method leads to the identity (isomorphism) of syntax and semantics (formal logic and formal ontology). Unlike traditional formal logic the type theory is an interpreted system from the very beginning. Being intuitionistic, Martin-Löf ’s theory is based on the notion of proof, not truth. From the meaning theory point of view, it is a variant of proof-theoretic semantics (Gentzen, Prawitz, Dummett) which understands meaning as an object constructed according to certain rules. So understood, the proof is based on evidence, which allows us to associate it with the theory of intentionality by Husserl. The article compares Martin-Löf ’s type theory with Husserl’s intentionality theory, especially with the latter’s noematic component. We may consider type-theoretical rules for constructing objects and operating with them as a concretization and formalization of the phenomenological notion of noema. Both are explications of the more general concept of meaning. The article discusses the interrelation between notions of sense and meaning (Sinn, Bedeutung) in Frege, Husserl and Martin-Löf. This reveals the uncertainty of Martin-Löf ’s position in relation to meaning theories of Frege and Husserl.

Keywords
type theory, phenomenology, analytic philosophy, formal semantics, Martin-Löf, sense, meaning.

References

• Bentzen, B. (2023). Propositions as Intentions. Husserl Studies, 39, 143–160. https://doi.org/10.1007/s10743-022-09323-3
• Bishop, E., & Bridges, D. (1985). Constructive Analysis. Berlin, Heidelberg: Springer-Verlag.
• Borisov, E. V. (2018). Quine’s Problem is Coming Back. Epistemology & Philosophy of Science, 55, 58–61. https://doi.org/10.5840/eps201855467 (In Russian)
• Brentano, F. (2012). On the Several Senses of Being in Aristotle. Rus. Ed. St. Petersburg: Vysshaia religiozno-filosofskaia shkola Publ. (In Russian)
• Domanov, O. A. (2018). Type Theory in the Semantics of Propositional Attitudes. Epistemology & Philosophy of Science, 55 (4), 26–37. https://doi.org/10.5840/eps201855462 (In Russian)
• Dummett, M. (1975). What is a Theory of Meaning? In S. Guttenplan (Ed.), Mind and Language (97– 138). Oxford: Oxford University Press.
• Dummett, M. (1978). The Philosophical Basis of Intuitionistic Logic. In Truth and Other Enigmas (215–247). Cambridge: Harvard University Press.
• Føllesdal, D. (1969). Husserl’s Notion of Noema. The Journal of Philosophy, 66, 680–687. https://doi.org/10.2307/2024451
• Føllesdal, D. (1990). Noema and Meaning in Husserl. Phenomenology and Philosophical Research, 50, 263–271. https://doi.org/10.2307/2108043
• Frege, G. (1966). Grundgesetze der Arithmetik. Hildesheim: Olms.
• Frege, G. (2000a). Concept Script, a Formal Language of Pure Thought Modelled Upon That of Arithmetic. In Logika i logicheskaia semantika: Sbornik trudov (65–142). Rus. Ed. Moscow: Aspekt Press Publ. (In Russian)
• Frege, G. (2000b). On Sense and Reference. In Logika i logicheskaia semantika: Sbornik trudov (230– 246). Rus. Ed. Moscow: Aspekt Press Publ. (In Russian)
• Husserl, E. (1921). Logische Untersuchungen. Zweiter Band. Elemente einer phänomenologischen Aufklärung der Erkenntnis. II. Teil. Halle: Max Niemeyer.
• Husserl, E. (1971). Ideen zu einer reinen Phanomenologie und phanomenologischen Philosophie: Drittes Buch. Die phanomenologie und die fundamente der Wissenschaften (Hua V) (M. Biemel, Еd.). Den Haag: Martinus Nijhoff. https://doi.org/10./007/978-94-0/0-2967-4
• Husserl, E. (1976). Ideen zu einer reinen Phänomenologie und phänomenologischen Philosophie I: Erstes Buch. Allgemeine Einführung in die reine Phänomenologie (Hua III/I) (K. Schuhmann, Ed.). Den Haag: Martinus Nijhoff.
• Husserl, E. (2009). Ideas Pertaining to a Pure Phenomenology and to a Phenomenological Philosophy. Rus. Ed. Moscow: Akademicheskii proekt Publ. (In Russian)
• Husserl, E. (2011). Logical Investigations. Vol. II. Elements of a Phenomenological Elucidation of Cognition. Part I. Rus. Ed. Moscow: Akademicheskii proekt Publ. (In Russian)
• Johnstone, P. T. (2002). Sketches of an Elephant: A Topos Theory Compendium. Oxford: Clarendon Press.
• Kant, I. (1994). Critique of Pure Reason. Rus. Ed. Moscow: Mysl’ Publ. (In Russian)
• Lamberov, L. D. (2018). New Analytic Philosophy: A Comment on O. A. Domanov’s Paper. Epistemology & Philosophy of Science, 55, 48–52. https://doi.org/10.5840/eps201855465 (In Russian)
• Martin-Löf, P. (1984). An Intuitionistic Type Theory: Notes by Giovanni Sambin of a Series of Lectures Given in Padua, June 1980. Napoli: Bibliopolis.
• Martin-Löf, P. (1987). Truth of a Proposition, Evidence of a Judgement, Validity of a Proof. Synthese, 73, 407–420. https://doi.org/10.1007/BF00484985
• Martin-Löf, P. (1993). Philosophical Aspects of Intuitionistic Type Theory: Lectures Given at the Faculteit der Wijsbegeerte, Rijksuniversiteit Leiden, 23 September—16 December 1993. Retrieved from https://pml.flu.cas.cz/uploads/PML-LeidenLectures93.pdf
• Martin-Löf, P. (1996). On the Meanings of the Logical Constants and the Justifications of the Logical Laws. Nordic Journal of Philosophical Logic, 1 (1), 11–60.
• Martin-Löf, P. (2002). Husserl’s Correlation Between Formal Logic and Formal Ontology: Lecture Given at Bern, 17 January 2002. Retrieved from https://pml.flu.cas.cz/uploads/PML-Bern17Jan02.pdf
• Mikirtumov, I. B. (2018). Type Theoretical Grammar, Intensional Entities and Epistemic Attitudes. Epistemology & Philosophy of Science, 55, 53–57. https://doi.org/10.5840/eps201855466 (In Russian)
• Rodin, A. V. (2018). Martin-Löf Type Theory as a Multi-Agent Epistemic Formal System. Epistemology & Philosophy of Science, 55, 44–47. https://doi.org/10.5840/eps201855464 (In Russian)
• Skolem, T. (1934). Über die Nicht-charakterisierbarkeit der Zahlenreihe mittels endlich oder abzählbar unendlich vieler Aussagen mit ausschliesslich Zahlenvariablen. Fundamenta Mathematicae, 23, 150–161. https://doi.org/10.4064/fm-23-1-150-161
• Sundholm, G. (2012). On the Philosophical Work of Per Martin-Löf. In P. Dybjer, S. Lindström, E. Palmgren, & G. Sundholm (Eds.), Epistemology Versus Ontology: Essays on the Philosophy and Foundations of Mathematics in Honour of Per Martin-Löf (xvii–xxiv). Dordrecht: Springer. https://doi.org/10.1007/978-94-007-4435-6
• Tiskin, D. B. (2018). New Machinery, Olden Tasks? Epistemology & Philosophy of Science, 55, 38–43. https://doi.org/10.5840/eps201855463 (In Russian)
• Univalent Foundations Program. (2013). Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study. Retrieved from http://homotopytypetheory.org/book.