Теория типов Мартин-Лёфа: между феноменологией и аналитической философией
Олег Доманов
Теория типов Мартин-Лёфа опирается одновременно на логико-онтологические идеи Фреге и Рассела и на феноменологию Гуссерля. В статье исследуется этот промежуточный характер теории типов на примере синтактико-семантического метода Мартин-Лёфа и роли очевидности и канонических объектов в его теории. Синтактико-семантический метод заимствуется Мартин-Лёфом у Фреге и расширяется с опорой на теорию значения Гуссерля. Этот метод приводит в теории типов к совпадению (изоморфизму) синтаксиса и семантики (формальной логики и формальной онтологии). В отличие от традиционной формальной логики, теория типов является изначально интерпретированной системой. Будучи интуиционистской, теория Мартин-Лёфа построена на понятии доказательства, а не истинности. С точки зрения теории значения, она представляет собой вариант теоретико-доказательной семантики (Генцен, Правиц, Даммит), в которой смысл понимается как объект, построенный по определённым правилам. Так понятое доказательство опирается на очевидность, что позволяет связать его с теорией интенциональности Гуссерля. В статье проводится сопоставление теории типов и теории интенциональности Гуссерля, особенно её ноэматической стороны. Правила конструирования объектов и оперирования с ними в теории типов можно рассматривать как конкретизацию и формализацию феноменологического понятия ноэмы. То и другое является экспликацией более общего понятия смысла или значения. В статье рассмотрено соотношение понятий смысла и значения (Sinn, Bedeutung) у Фреге, Гуссерля и Мартин-Лёфа. Показана неопределённость позиции Мартин-Лёфа по отношению к теориям значения Фреге и Гуссерля.
Ключевые слова: теория типов, феноменология, аналитическая философия, формальная семантика, Мартин-Лёф, смысл, значение.
MARTIN-LOF'S TYPE THEORY: BETWEEN PHENOMENOLOGY AND ANALYTICAL PHILOSOPHY
Oleg Domanov
Martin-Lof'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-Lof's syntactical-semantic method and the role of evidence and canonical objects in his approach. Martin-Lof 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-Lof'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-Lof'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-Lof. This reveals the uncertainty of Martin-Lof's position in relation to meaning theories of Frege and Husserl.
Keywords: type theory, phenomenology, analytic philosophy, formal semantics, Martin-Lof, sense, meaning.
ВВЕДЕНИЕ
Теория типов Мартин-Лёфа была разработана им как формализация интуиционистских математических рассуждений (Martin-Lof, 1984). Её развитие, однако, вышло за эти узкие рамки. В настоящее время ясно, что теория типов, по крайней мере в некоторых своих вариантах, может претендовать на замену теории множеств в основаниях математики. Существует большой проект по формулированию математики в языке теории типов (Univalent Foundations Program, 2013). Как можно надеяться, теория типов избегает основных проблем, обнаруженных в теории множеств и связанных с парадоксами, неполнотой и пр. Однако её значение не ограничивается математикой. Философские основания теории типов включают в себя не только логику и онтологию Фреге и Рассела, но и феноменологию Гуссерля. С известной долей условности можно сказать, что теория типов Мартин-Лёфа представляет собой формальную теорию, которую мог бы построить Гуссерль, если бы имел интерес к подобным формализованным языкам. И феноменология, и аналитическая философия вырастают из проблем логики и обоснования математики, однако их дороги со временем расходятся. Не в последнюю очередь причиной этого расхождения была опора аналитической философии на логику Фреге, за которой стояла определённая семантическая теория. Ранняя аналитическая философия, прежде всего Рассел, рассматривала логический анализ как способ разрешения философских проблем. И хотя понимание анализа в ней сильно трансформировалось, наследство Фреге остаётся существенным и сегодня (если сегодня вообще можно говорить о содержательном единстве аналитической философии). Однако сама система Фреге, как очень быстро выяснилось, оказалась противоречивой. Было предложено множество способов справиться с этим противоречием, которые, хотя и разрешили проблему на формальном уровне, но оставили вопросы на уровне философском. В этой ситуации интуиционистская -- и шире, конструктивистская -- математика указывает на корень проблем в самих основаниях логики Фреге. Опираясь на интуиционистские идеи, Мартин-Лёф возвращается к исходной ситуации и строит логику заново. Он развивает идею типов, предложенную Расселом для разрешения трудностей системы Фреге. В то же время он явным образом опирается на Гуссерля и рассматривает свою работу как продолжение линии, с одной стороны, логики Фреге и Principia Mathematica (Martin-Lof, 1993, 6), а с другой -- Брентано и Гуссерля. Как сообщает Горан Сандхолм, Мартин-Лёф считает свой синтактико-семантический метод (см. ниже) вариантом феноменологии (Sundholm, 2012, xx). Более того, свою работу он рассматривает как попытку согласовать между собой эти две линии философии: «Я считаю, что то углубление в эту область, которое я собираюсь предпринять, может оказаться одним из наиболее перспективных путей, на котором раскол между аналитической и континентальной философией можно сделать менее резким или начать его преодолевать» (Martin-Lof, 1993, 4). Таким образом, он сам ставит себя в промежуточную позицию между феноменологической и аналитической философией.
Теорию типов можно рассматривать как исключительно математическую теорию и использовать в своей работе, не заботясь о её философских основаниях и аспектах. Так делают, например, многие в математике и компьютерных науках. Однако так же, как и на логику вообще, на теорию типов возможен и иной взгляд. Для Фреге и Рассела разрабатываемая ими логика была не просто математической теорией, а языком мышления. Основополагающая книга Фреге называется «Исчисление понятий», что можно перевести также как Запись понятий (Begriffsschriff). Фреге называет то, с чем имеет дело этот язык, просто мыслями. Формализм для Фреге и Рассела не является самоцелью и не проводится ради «математизации». Он позволяет достичь точности и определённости в записи нашего мышления (как формулирует Витгенштейн в «Трактате», форма языка позволяет избегать многих ошибок просто потому, что они не могут быть записаны). То же самое касается Мартин-Лёфа. Хотя исходные его работы принадлежат математике (или, возможно, метаматематике), позднее его интерес смещается в сторону философской теории значения (среди тех, кто в наибольшей мере повлиял на этот сдвиг, Сандхолм называет Витгенштейна и Даммита1). Причём речь идёт не столько о философских основаниях теории типов, сколько о самой этой теории как языке мышления, записывающем процесс и результат понимания и смыслополагания. Формализация в этом подходе связана с актами понимания как усмотрения формы, приведения к форме. Именно на этом пути Мартин-Лёф встречает Гуссерля с его теорией языка и значения. В этом отношении он фактически проделывает ту же работу по построению формального языка мышления, что Фреге и Рассел, однако на других философских основаниях. Именно этим его работа интересна с точки зрения исследования связи аналитической философии и феноменологии. Из феноменологии он заимствует гуссерлевские разработки теории значения и роли очевидности в понимании. Со стороны же аналитической философии его интерес направлен на методологию построения и обоснования формального языка (отсюда его синтактико-семантический метод, см. ниже), а также на витгенштейновскую идею значения как употребления (не считая того факта, что сама теория типов была предложена Расселом на раннем этапе становления аналитической философии). Характер этого интереса определяет то, что мы в нашем рассмотрении ниже будем обращать внимание не столько на результаты и понятия ранней аналитической философии, сколько на её методологию, явленную в ходе построения формального языка как языка мышления.
С этим связано ещё одно обстоятельство, на которое следует указать. Формальная семантика в современном её понимании имеет дело с формальными неинтерпретированными языками, которые затем интерпретируются -- чаще всего на множествах, но также и на категориях. В частности, (экстенсиональная) теория типов Мартин-Лёфа может интерпретироваться на локально декартово замкнутых категориях (LCCC). Более того, в категорной семантике Cм.: (Sundholm, 2012, xix). теория типов выступает как «внутренний язык» категории, который, таким образом, интерпретируется на этой категории См., например: (Johnstone, 2002, D1.2). -- теория типов является здесь языком, а категория -- его моделью. Однако построения Мартин-Лёфа, обсуждаемые в настоящей статье, предполагают другой взгляд на теорию типов. С точки зрения теории моделей (хотя её применимость здесь можно обсуждать отдельно) теория типов выступает здесь тем, на чём проводится интерпретация. В этом смысле, если Фреге и Рассел предполагают, что формальный язык должен интерпретироваться на множествах, то в теории Мартин-Лёфа он интерпретируется на типах. Более существенное различие состоит, однако, в том, что если у Фреге и Рассела язык (логика предикатов) и интерпретация (теория множеств) разнесены, то у Мартин-Лёфа то и другое относится к теории типов. Этот параллелизм -- или даже совпадение -- синтаксического и семантического является характерной особенностью теории типов, которая нас и будет преимущественно интересовать. Непривычный для традиционной формальной семантики, этот параллелизм не остаётся, тем не менее, без прецедентов в истории философии. Действительно, Кант в первой Критике начинает поиск категорий (чистых рассудочных понятий) с построения списка форм суждений, а затем говорит:
Та же самая функция, которая придаёт единство различным представлениям в одном суждении, сообщает единство также и чистому синтезу различных представлений в одном созерцании; это единство, выраженное в общей форме, называется чистым рассудочным понятием. Итак, тот же самый рассудок и притом теми же самыми действиями, которыми он посредством аналитического единства создаёт логическую форму суждения в понятиях, вносит также трансцендентальное содержание в свои представления посредством синтетического единства многообразного в созерцании вообще. (Kant, 1994, 86)
Таким образом, с точки зрения формы кантовские категории относятся как к синтаксису (формы суждений), так и к семантике (формы объективности). Более того, Кант указывает на причину этой синтактико-семантической параллели: она состоит в том, что рассудок выполняет здесь одно и то же действие. Мартин-Лёф указывает на этот момент кантовского построения (Martin-Lof, 1993, 21), хотя и не разбирает его подробно.
Таким образом, в фокусе нашего интереса будет находиться семантическая теория Мартин-Лёфа в её соотнесении с аналитической философией и феноменологией. Разумеется, в кратком тексте невозможно провести сколько-нибудь полное рассмотрение этого соотнесения, поэтому мы ограничимся двумя сюжетами -- синтактико-семантическим методом Мартин-Лёфа и ролью очевидности в его теории. Нашей непосредственной задачей будет прояснение строения и способов обоснования описанного выше синтактико-семантического параллелизма в теории типов Мартин-Лёфа.
1. СИНТАКТИКО-СЕМАНТИЧЕСКОЕ ОБЪЯСНЕНИЕ
Мартин-Лёф строит свою теорию как интуиционистскую теорию типов (Martin-Lof, 1984) Литература по теории типов на русском языке не очень обширна. Среди примеров мож-но указать на статьи Л. Ламберова и А. Родина, а также на дискуссию о теоретико-типовой семантике в журнале «Эпистемология и философия науки» (Borisov, 2018; Domanov, 2018; Lamberov, 2018; Mikirtumov, 2018; Rodin, 2018; Tiskin, 2018).. На связь интуиционизма и феноменологии обратили внимание давно. Уже Аренд Гейтинг, один из основателей интуиционизма, интерпретирует понятие пропозиции, ссылаясь на интенциональность Гуссерля, с идеями которого он был знаком благодаря Оскару Беккеру См. подробности и обзор литературы: (Bentzen, 2023). Нужно заметить, что сам Бенцен оспаривает корректность такой связи интуиционизма и феноменологии.. Мартин-Лёф заимствует в интуиционизме идею доказательства как объекта, а также понимание самого доказательства как исполнения интенции. Чтобы понять, как он это делает, рассмотрим базовые принципы теории типов.
Одним из основных понятий теории типов Мартин-Лёфа является понятие суждения. Фреге в своей логике различает содержание (Inhalt) и акт утверждения этого содержания, который и называет суждением (Urteil). В исходной версии Записи в понятиях 1879 года (Frege, 2000a) суждение обозначает утверждение наличия некоторого положения дел Ф: «имеет место Ф». Позднее, в работе «Основные законы арифметики» 1893 года (Frege, 1966), Фреге существенно меняет свой подход, и суждение теперь понимается как акт утверждения истинности или ложности предложения. Рассел и Уайтхед в Principia Mathematica переводят Urteil на английский язык как assertion, также понимая под ним утверждение истинности или ложности. Это сужение понятия суждения, а также то, что у Фреге имеется только один его вид, приводит к тому, что оно вытесняется из языка логики в метаязык в пользу анализа пропозиций и их истинности. Напротив, Мартин-Лёф восстанавливает суждение в своём формализме и различает четыре их вида (записанных здесь в сокращённой форме):