Теория типов Мартин-Лёфа: между феноменологией и аналитической философией

Мы видим, как Мартин-Лёф занимает неопределённую позицию по отношению к теориям значения Фреге и Гуссерля. Очевидность доказательства в теории типов состоит в переживании совпадения предполагаемой формы с формой имеющегося объекта, поскольку, например, он сконструирован определённым образом. Гуссерлевское понимание очевидности работает здесь, как кажется, вполне успешно. Мартин-Лёф, однако, сохраняет теорию смысла Ср. у Фреге смысл как способ указания на значение, «в чем выражается конкретный способ задания обозначаемого (worin die Art des Gegebenseins enthalten ist)» (Frege, 2000b, 231). и значения/референции Фреге и пытается совместить её с предыдущим путём трансформации понятия референции. Насколько такая попытка может быть успешной, остаётся открытым вопросом. Можно предположить, что теории типов следует в большей степени ориентироваться на феноменологическую теорию значения, которая плохо совместима с семантической теорией, лежащей в основании логики Фреге и Рассела. Это, однако, требует дальнейшего исследования.

ЗАКЛЮЧЕНИЕ

теория тип феноменология аналитический

Мы видим, что теорию Мартин-Лёфа можно рассматривать как формальную экспликацию теории интенциональности Гуссерля. Мартин-Лёф опирается, с одной стороны, на идею формального языка мышления Фреге и теорию типов Рассела, а с другой, на разработку Гуссерлем интенциональности, значения и очевидности. Эта одновременная опора становится возможной благодаря интуиционистской по своим основаниям теоретико-доказательной семантике Генцена, Правица и Даммита. Можно сказать, что последняя позволяет надеяться провести формализацию гуссерлевской феноменологии «с нуля», не опираясь на заранее данный формальный язык, такой как предоставляемый первопорядковой логикой, а выстраивая такой язык «из самих вещей», усматривая форму в самих вещах. Мартин-Лёф, в этом смысле, использует не столько результаты и схемы феноменологии и аналитической философии, сколько их методологические подходы. Разумеется, следует признать, что проведённая параллель между теорией типов и феноменологией описана выше очень схематично. За рамками остаётся множество аспектов и нюансов этого соответствия, которые присутствуют у Гуссерля, но отсутствуют у Мартин-Лёфа, такие как степени очевидности совпадения, модальности, переживания несовпадения и пр. Кроме того, здесь не учтены эффекты, связанные со сложностью синтаксиса, такие как синтаксические трансформации, грамматические формы, разнообразие выражений в разных языках и т. д. С другой стороны, теория типов в определённой мере восполняет нехватку, имеющуюся в гуссерлевской феноменологии, предлагая более точный и развитый язык для описания ноэматической стороны интенции, то есть для описания смысла. Нельзя сказать, что в исследовании того, как это происходит, мы достигли полной ясности. Тем не менее мы увидели неопределённость позиции Мартин-Лёфа, связанную, вероятно, с синтетическим характером его подхода. Это не означает, что от последнего следует отказаться. Поздние работы Мартин-Лёфа позволяют посмотреть на теорию типов как на попытку проделать работу Фреге и Рассела по построению языка мышления на иных философских основаниях. И хотя детали этого предприятия и даже возможность его осуществимости не до конца ясны, попытка Мартин-Лёфа «начать преодолевать раскол между аналитической и континентальной философией», безусловно, заслуживает внимания исследователя.

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, 5861. 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 (97138). Oxford: Oxford University Press.

Dummett, M. (1978). The Philosophical Basis of Intuitionistic Logic. In Truth and Other Enigmas (215-247). Cambridge: Harvard University Press.

Follesdal, D. (1969). Husserl's Notion of Noema. The Journal of Philosophy, 66, 680-687. https://doi. org/10.2307/2024451

Follesdal, 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 (230246). Rus. Ed. Moscow: Aspekt Press Publ. (In Russian)

Husserl, E. (1921). Logische Untersuchungen. Zweiter Band. Elemente einer phdnomenologischen Aufkldrung 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 5) (M. Biemel, Ed.). Den Haag: Martinus Nijhoff. https://doi.org/10./007/978-94-0/0-2967-4

Husserl, E. (1976). Ideen zu einer reinen Phanomenologie und phdnomenologischen Philosophie I: Erstes Buch. Allgemeine Einfdhrung in die reine Phanomenologie (Hua 3/1) (K. Schuhmann, Ed.). Den Haag: Martinus Nijhoff.

Husserl, E. (2009). Ideen zu einer reinen Phanomenologie undphanomenologischen Philosophie. Rus. Ed. Moscow: Akademicheskii proekt Publ. (In Russian)

Husserl, E. (2011). Logische Untersuchungen. Zweiter Band. Elemente einer phdnomenologischen Aufkldrung der Erkenntnis. I. Teil. 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-Lof, P. (1984). An Intuitionistic Type Theory: Notes by Giovanni Sambin of a Series of Lectures Given in Padua, June 1980. Napoli: Bibliopolis.

Martin-Lof, 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-Lof, 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-Lof, 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-Lof, 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-Lof 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). Uber die Nicht-charakterisierbarkeit der Zahlenreihe mittels endlich oder abzahlbar 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-Lof. In P.Dybjer, S. Lindstrom, E. Palmgren, & G. Sundholm (Eds.), Epistemology Versus Ontology: Essays on the Philosophy and Foundations of Mathematics in Honour of Per Martin-Ldf (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.

Размещено на Allbest.ru