Информация о Статье/Публикации
Просмотров: 1687

ТЕОРИЯ ТИПОВ МАРТИН-ЛЁФА: МЕЖДУ ФЕНОМЕНОЛОГИЕЙ И АНАЛИТИЧЕСКОЙ ФИЛОСОФИЕЙ

Аннотация
Теория типов Мартин-Лёфа опирается одновременно на логико-онтологические идеи Фреге и Рассела и на феноменологию Гуссерля. В статье исследуется этот промежуточный характер теории типов на примере синтактико-семантического метода Мартин-Лёфа и роли очевидности и канонических объектов в его теории. Синтактико-семантический метод заимствуется Мартин-Лёфом у Фреге и расширяется с опорой на теорию значения Гуссерля. Этот метод приводит в теории типов к совпадению (изоморфизму) синтаксиса и семантики (формальной логики и формальной онтологии). В отличие от традиционной формальной логики, теория типов является изначально интерпретированной системой. Будучи интуиционистской, теория Мартин-Лёфа построена на понятии доказательства, а не истинности. С точки зрения теории значения, она представляет собой вариант теоретико-доказательной семантики (Генцен, Правиц, Даммит), в которой смысл понимается как объект, построенный по определённым правилам. Так понятое доказательство опирается на очевидность, что позволяет связать его с теорией интенциональности Гуссерля. В статье проводится сопоставление теории типов и теории интенциональности Гуссерля, особенно её ноэматической стороны. Правила конструирования объектов и оперирования с ними в теории типов можно рассматривать как конкретизацию и формализацию феноменологического понятия ноэмы. То и другое является экспликацией более общего понятия смысла или значения. В статье рассмотрено соотношение понятий смысла и значения (Sinn, Bedeutung) у Фреге, Гуссерля и Мартин-Лёфа. Показана неопределённость позиции Мартин-Лёфа по отношению к теориям значения Фреге и Гуссерля.

Ключевые слова
теория типов, феноменология, аналитическая философия, формальная семантика, Мартин-Лёф, смысл, значение.

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.