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

Размещено на http://www.allbest.ru/

Размещено на http://www.allbest.ru/

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

Олег Доманов

Теория типов Мартин-Лёфа опирается одновременно на логико-онтологические идеи Фреге и Рассела и на феноменологию Гуссерля. В статье исследуется этот промежуточный характер теории типов на примере синтактико-семантического метода Мартин-Лёфа и роли очевидности и канонических объектов в его теории. Синтактико-семантический метод заимствуется Мартин-Лёфом у Фреге и расширяется с опорой на теорию значения Гуссерля. Этот метод приводит в теории типов к совпадению (изоморфизму) синтаксиса и семантики (формальной логики и формальной онтологии). В отличие от традиционной формальной логики, теория типов является изначально интерпретированной системой. Будучи интуиционистской, теория Мартин-Лёфа построена на понятии доказательства, а не истинности. С точки зрения теории значения, она представляет собой вариант теоретико-доказательной семантики (Генцен, Правиц, Даммит), в которой смысл понимается как объект, построенный по определённым правилам. Так понятое доказательство опирается на очевидность, что позволяет связать его с теорией интенциональности Гуссерля. В статье проводится сопоставление теории типов и теории интенциональности Гуссерля, особенно её ноэматической стороны. Правила конструирования объектов и оперирования с ними в теории типов можно рассматривать как конкретизацию и формализацию феноменологического понятия ноэмы. То и другое является экспликацией более общего понятия смысла или значения. В статье рассмотрено соотношение понятий смысла и значения (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). Фреге называет то, с чем имеет дело этот язык, просто мыслями. Формализм для Фреге и Рассела не является самоцелью и не проводится ради «математизации». Он позволяет достичь точности и определённости в записи нашего мышления (как формулирует Витгенштейн в «Трактате», форма языка позволяет избегать многих ошибок просто потому, что они не могут быть записаны). То же самое касается Мартин-Лёфа. Хотя исходные его работы принадлежат математике (или, возможно, метаматематике), позднее его интерес смещается в сторону философской теории значения (среди тех, кто в наибольшей мере повлиял на этот сдвиг, Сандхолм называет Витгенштейна и Даммита¹). Причём речь идёт не столько о философских основаниях теории типов, сколько о самой этой теории как языке мышления, записывающем процесс и результат понимания и смыслополагания. Формализация в этом подходе связана с актами понимания как усмотрения формы, приведения к форме. Именно на этом пути Мартин-Лёф встречает Гуссерля с его теорией языка и значения. В этом отношении он фактически проделывает ту же работу по построению формального языка мышления, что Фреге и Рассел, однако на других философских основаниях. Именно этим его работа интересна с точки зрения исследования связи аналитической философии и феноменологии. Из феноменологии он заимствует гуссерлевские разработки теории значения и роли очевидности в понимании. Со стороны же аналитической философии его интерес направлен на методологию построения и обоснования формального языка (отсюда его синтактико-семантический метод, см. ниже), а также на витгенштейновскую идею значения как употребления (не считая того факта, что сама теория типов была предложена Расселом на раннем этапе становления аналитической философии). Характер этого интереса определяет то, что мы в нашем рассмотрении ниже будем обращать внимание не столько на результаты и понятия ранней аналитической философии, сколько на её методологию, явленную в ходе построения формального языка как языка мышления.

С этим связано ещё одно обстоятельство, на которое следует указать. Формальная семантика в современном её понимании имеет дело с формальными неинтерпретированными языками, которые затем интерпретируются -- чаще всего на множествах, но также и на категориях. В частности, (экстенсиональная) теория типов Мартин-Лёфа может интерпретироваться на локально декартово замкнутых категориях (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, также понимая под ним утверждение истинности или ложности. Это сужение понятия суждения, а также то, что у Фреге имеется только один его вид, приводит к тому, что оно вытесняется из языка логики в метаязык в пользу анализа пропозиций и их истинности. Напротив, Мартин-Лёф восстанавливает суждение в своём формализме и различает четыре их вида (записанных здесь в сокращённой форме):

Первое суждение означает, что A является типом, второе -- что объект a относится к типу A, третье -- что объекты а и b типа A равны и, наконец, четвёртое -- что типы A и B равны. Как и у раннего Фреге, вынесение суждения означает признание некоторого положения дел, что означает, что мы поняли нечто, признали его имеющим место, узнали нечто: «судить это то же самое, что знать» (Martin-Lof, 1996, 20). Поэтому суждение фактически эквивалентно знанию (если, конечно, как говорит Фреге, мы выносим его «серьёзно»). Вынося суждение, мы утверждаем или подтверждаем, что нечто знаем или опознаём. Основанием для вынесения суждения A: type является наше знание того, что A -- тип, которое, в свою очередь, является знанием того, что значит для объектов относиться к данному типу и что значит для двух таких объектов быть равными. Как видно, первые три вида суждений связаны: если мы знаем, что A -- тип, то мы знаем, как выносить суждения вида а: A для объектов а и суждения вида а = b: A для объектов а и b. Такое понимание типа похоже на определение множества в конструктивистской математике См., например: (Bishop & Bridges, 1985).. Это не случайно, так как множество является одним из примеров типа. Другим таким примером, как мы увидим ниже, является пропозиция.

В системе Мартин-Лёфа объект всегда относится к какому-то типу (причём только к одному, что, в частности, затрудняет расширение этой системы за пределы математики). Это определяет форму объекта, а также то, какие действия с ним допустимо совершать. Как мы видели, суждение о принадлежности к типу относится к одному из основных суждений и записывается как а: A. Это современное обозначение, сам Мартин-Лёф в первоначальных формулировках теории использовал запись а Є A и указывал, что Є здесь происходит от греческого слова готі, поэтому а: A является, фактически, формализацией предложения «а есть A» (Martin-Lof, 1993, 8). Таким образом, относиться к типу означает быть чем-то, и объекты никогда не бывают «ничем»: «[Объект] всегда есть нечто, и это “нечто”, которое он есть, мы называем его типом. Таким образом, когда мы вообще имеем какой-либо объект, он всегда есть нечто, объект определённого типа» (Martin-Lof, 1993, 20). Это «нечто» есть то, в качестве чего мы опознаём объект, когда встречаемся с ним.

Таким образом, вопрос о типе является онтологическим, и этот онтологический аспект позволяет Мартин-Лёфу говорить об отождествлении типов с категориями Аристотеля (Martin-Lof, 1993, 20 ff.). Это, однако, не вполне точно. Действительно, категории, как их понимает Аристотель, появляются у него как экспликация различных форм «быть» в выражениях вида «... есть...». Однако каждая из них отвечает на свой вопрос: «Что (есть)?», «Какое (есть)?», «Сколько (есть)?», «Где (есть)?» и т. д. -- каждая из них говорит о сущем своим способом (Brentano, 2012). На вопрос «Что?» при этом отвечает лишь одна категория -- усия, ошіа. Этот термин имеет несколько смыслов в аристотелевской онтологии, один из которых позднее обозначается как сущность. В языке сущность представлена определением, которое в схоластике связывается с чтойностью (лат. quidditas). Чтойность и является ответом на вопрос «Что есть это?». Поэтому, хотя Мартин-Лёф отождествляет типы с аристотелевскими категориями, они, скорее, соответствуют лишь одной из них -- сущности. Он сам, впрочем, указывает на прямую связь с чтойностью и в дальнейшем говорит именно о сущности: «То, о чём этот вопрос спрашивает, есть сущность, и ответ на этот вопрос, то есть вербальная формулировка ответа на вопрос, называется определением» (Martin-Lof, 1993, 29).

Следуя схоластической терминологии, Мартин-Лёф различает два вида определений: реальное определение, определение вещи (definitio quid rei) и номинальное определение, определение имени (definitio quid nominis). Последние формулируются через равенство, когда мы полагаем, что определяемый термин равен такому-то определяющему выражению. Определение типа не может быть дано в таком виде, оно должно быть, в некотором смысле, независимо, то есть являться реальным определением. Мартин-Лёф называет такие определения объяснением смысла (meaning explanation). Чтобы объяснить смысл типа, то есть ответить на вопрос «Что такое (данный) тип?» нам нужно объяснить две вещи: 1) как могут выглядеть объекты типа; 2) что означает для этих объектов быть равными. Метод такого объяснения Мартин-Лёф называет синтактико-семантическим методом. Это метод объяснения некоторой синтаксической формы, предположительно схватывающей объясняемый объект. Чтобы лучше понять, о чём здесь идёт речь, рассмотрим примеры объяснений.

Объяснение того, что такое тип пар A х B, Мартин-Лёф начинает с записи синтаксических форм:

Смысл первого выражения объясняется следующим образом: A х B является типом, если A и B являются типами. Смысл же второго выражения объясняется так: если а относится к типу A, а b -- к типу B, то пара (a, b) относится к типу A х B. Тем самым объясняется, как выглядит тип пар и как выглядят его элементы (пары). Объяснение содержит в себе формы, относящиеся к объясняемому типу: форму типа и форму (или формы) его элементов (для простоты я опускаю правила, связанные с определением равенства объектов или типов). Как видно, синтаксические формы имеют вид правил, которые являются правилами построения соответствующих типов и их объектов. С другой стороны, эти правила содержат суждения, поэтому они представляют собой правила вывода суждений из других суждений (или вывода знания из другого знания).

В качестве другого примера рассмотрим тип натуральных чисел N:

Первое из этих правил выводит суждение 0: N из пустого множества предпосылок. Иначе говоря, оно просто утверждает, что 0 относится к натуральным числам. Второе правило показывает, что из натурального числа n: N мы можем построить натуральное число s(n): N -- число, следующее за п. Такое определение напоминает определение натуральных чисел посредством аксиом Пеано. Имеется, однако, существенное различие. Аксиоматическое определение имеет приблизительный вид: «Множеством натуральных чисел N называется множество, в котором определены выделенный элемент 0 и функция s: N^ N (функция следующего числа), такие, что удовлетворяются аксиомы Пеано». Аксиомы, таким образом, формулируются на изначально не интерпретированном языке, который затем может быть интерпретирован на некотором множестве; и если интерпретация успешна (аксиомы выполняются), то это множество называется множеством натуральных чисел. Такой способ определения, вообще говоря, допускает интерпретацию на неизоморфных множествах, то есть допускает неизоморфные модели (это неверно в случае самих аксиом Пеано, но верно для их первопорядковой формулировки). Так, например, мы получаем нестандартные числа, не совпадающие с натуральными, но подчиняющиеся аксиомам арифметики (Skolem, 1934). Напротив, в теории типов мы рассматриваем 0 и s как конструкторы, которые последовательно конструируют натуральные числа, начиная с нуля. Определив конструирование, мы затем можем показать, что так построенный тип удовлетворяет всем аксиомам Пеано. Аналогично в случае типа пар мы рассматриваем (--, --) как конструктор, конструирующий пару из заданных элементов. Тем самым, определяя тип, мы не просто вводим новые синтаксические выражения, но и одновременно строим модель для них. В теории типов речь не идёт просто о построении нового языка для записи математических утверждений и доказательств. Мартин-Лёф называет свою теорию интерпретированной логической системой (Martin-Lof, 1993, 1). В ней не существует традиционное для современной формальной семантики разделение неинтерпретированного языка, заданного правилами манипуляции символами, и его интерпретации. Язык теории типов не отделён от его интерпретации, он с самого начала «призван что-то сказать». Хотя этот подход отличается от принятого в современной формальной семантике, Мартин-Лёф в нём следует, тем не менее, Фреге, который, давая синтаксическую (языковую) форму, всегда сопровождал её семантическим объяснением. Проблема, однако, состоит в том, что логический язык Фреге интерпретируется на множествах и был с самого начала разработан с ориентацией на эту интерпретацию. При таком подходе остаётся неясным, каков статус языка самой теории множеств. Если интерпретация языка логики -- это перевод её на язык теории множеств, то должен ли этот последний быть интерпретирован для своего понимания? Очевидно, что нет, и этот язык должен быть интерпретирован или понятен с самого начала. Мартин-Лёф в своём формализме стремится учесть эту «всегда-уже-интерпретированность» языка. Поэтому, хотя он начинает с синтаксической записи, в объяснении он говорит о том, как устроены объекты. Здесь имеется тесная связь синтаксического и семантического уровней.

Важно заметить, что конструкторы задают форму конструируемых объектов. Если, например, число 2 определяется как s(s(0)), то в этом выражении мы видим не только способ построения этого числа, но и его форму. Форма выражения (синтаксис) повторяет здесь форму объекта (семантика). Объяснить смысл и задать правила построения -- это одно и то же (Martin-Lof, 1993, 48), и иногда Мартин-Лёф даёт объяснение сразу в виде правил. Они задают правила конструирования объектов, а также правила оперирования с ними, основанные на их форме (например, мы можем определить правила извлечения составляющих из пары и пр.).

В итоге, Мартин-Лёф описывает синтактико-семантический метод следующим образом:

Мы хотим достичь ясности, мы хотим понять механизм, который приводит нас к схватыванию этого объекта. [...] Ответ даётся путём синтактико-семантического прояснения, а именно, путём структурирования a [...].

Это большая проблема: структурировать а так, чтобы он стал комплексом атомов, комплексом примитивов. Затем мы даём объяснение смысла (meaning explanation) всем этим примитивам и видим, как эти атомы соединяются так, что их целое получает смысл из способа соединения. [...] Ясно, что всё изложенное содержит две части: синтаксическую часть и семантическую часть. Вместе они дают ответ на вопрос, который исходно был задан в терминах сущностей. (Martin-Lof, 1993, 83)

Результатом применения описанного метода является сущностная структура:

[Т]о, что я делаю здесь в современной форме синтактико-семантического анализа, есть, на самом деле, разработка теории сущности (Wesenslehre). Именно её реализация толкнула Гуссерля назвать его способ действий, его метод в «Логических исследованиях» Wesensschau. Мой метод, таким образом, есть в точности способ исследования сущностей, приведения к видению сущностей (coming to see essences). (Martin-Lof, 1993, 34)

Как и многое в своём подходе, Мартин-Лёф возводит этот метод к Фреге. Гуссерль, также прибегая к этому методу, расширяет его за пределы языковых форм. Действительно, в «Идеях» он прямо говорит, что термин «значение» им используется не только в контексте обсуждения языка При цитировании «Идей I» я пользуюсь преимущественно переводом (Husserl, 2009) и соот-ветствующей терминологией. В редких случаях моего собственного перевода используется (Husserl, 1976).:

Мы же будем устремлять свой взор исключительно на «означивание» (Bedeuten) и «значение» (Bedeutung). Первоначально оба эти слова сопряжены со сферой языка, со сферой, в которой что-либо «выражается». Однако почти неизбежный и одновременно важный шаг состоит в расширении и подходящей модификации значения этих слов, вследствие чего они известным образом находят применение во всей ноэтически-ноэматической сфере, -- следовательно, применяются ко всем актам, сплетены таковые с актами выражения или же нет. (Husserl, 2009, 385)

Таким образом, «означивание» (Гуссерль берёт здесь слово в кавычки) имеет место во всех интенциональных актах, связано это со сферой языка или нет. В третьем томе «Идей» он говорит: «ноэма вообще есть не что иное, как обобщение идеи значения на область актов» (Husserl, 1971, 89). Даже предложение имеет расширенное значение, выходящее за пределы языка: «понятия “смысл” (Sinn) и “предложение” (Satz) не содержат для нас ничего от выражения и понятийного значения, зато обнимают собою все выраженные предложения и, соответственно, значения предложений» (Husserl, 2009, 412). Так, например, существуют предложения созерцания.

Таким образом, значение (ноэма), вообще говоря, внелингвистично. Оно достигается в особом акте усмотрения или созерцания сущностей (Wesensschau, Wesensanschau). Однако, в то же самое время, имеется тесная связь между выражением (которое Гуссерль связывает с логикой) и значением:

Гласящие слова могут именоваться выражением только потому, что выражают принадлежное им значение -- в таковом изначально заключено выражающее. «Выражение» -- форма примечательная; она позволяет приспособить себя ко всякому «смыслу» (ноэматическому «ядру»), возвышая таковой до царства «логоса», до царства понятийного, а тем самым «всеобщего». (Husserl, 2009, 386)

Гуссерль не поясняет, как конкретно происходит это приспособление выражения к смыслу (которые к тому же здесь помещены в кавычки). В то же время у Мартин-Лёфа они, как кажется, «приспособлены» с самого начала. Рассмотрим внимательнее, что он понимает под выражением.

Согласно Мартин-Лёфу, при обычном обращении с языком мы рассматриваем его как говорящий об объектах. Чтобы обратить внимание на само языковое выражение, нужна смена установки:

Мы находимся внутри мира с объектами, и требуется сознательное усилие для того, чтобы сменить естественную установку, чтобы обратить внимание не на объект, а на вид (look) объекта, то есть рассматривать объект чисто формально. Это процесс формализации или удаления смысла (divesting of sense). (Martin-Lof, 1993, 82)

Мы видим, что сменить установку означает перевести внимание на вид или форму объекта. Несмотря на очевидные отсылки к Гуссерлю, вопрос о том, насколько это описание смены установки ему следует, требует отдельного исследования. Но в любом случае формальное здесь понимается в гуссерлевском смысле -- как относящееся к форме, а не обязательно выраженное в каком-то формализованном языке. Формализация -- это приведение к форме, усмотрение формы.

Но, с другой стороны, в ходе формализации предметы преобразуются в выражения (object expressions или type expressions) (Martin-Lof, 1993, 84). Следовательно, выражение -- это то, каким образом или в чём представлена форма объекта: «Выражение, в самом общем смысле слова, -- это не что иное, как форма, то есть нечто, что мы можем пассивно опознать как то же самое в её многочисленных проявлениях и активно репродуцировать во многих копиях» (Martin-Lof, 1996, 18). В результате формализации форма синтаксического и семантического совпадают благодаря тому, что имеют один и тот же вид (look, а также shape или form -- но, вероятно, лучше всего здесь подошёл бы термин «эйдос»).

Эти рассуждения Мартин-Лёфа могут показаться проблематичными. Мы, возможно, лучше их поймём, если обратимся к Фреге. В Исчислении понятий Фреге определяет функцию на уровне выражений: функция -- это выражение, в котором есть пустые места для заполнения другими выражениями. Однако в «Основных законах арифметики» он стремится строго разграничить предметы и их выражения в языке, поэтому функция определяется теперь на уровне предметов (в случае арифметики -- чисел): «Сущность функции проявляется скорее в связи, которую она устанавливает между числами, чьи знаки мы помещаем на место “x”, и числами, которые оказываются затем значениями (Bedeutungen) нашего выражения» (Frege, 1966, 5). Фреге не конкретизирует эту связь, но мы можем попытаться её восстановить. Пусть, например, мы имеем выражение/функцию «x + 2». Мы хотим посчитать его значение при x = 2. Для этого мы берём имя «2» и подставляем его в исходное выражение. Получаем «2 + 2». Вычисляя его по правилам арифметики, получаем выражение «4». Искомый результат будет референтом последнего, то есть числом 4. Мы видим, что для вычисления значения мы начинаем с объекта, который хотим подставить на место аргумента. Мы подставляем соответствующее ему выражение, получая некоторое (полное) выражение. После этого мы должны проделать вычисление на уровне выражения и получить какое-то имя в качестве результата. Искомое значение будет тогда значением этого имени. Но не означает ли это, что мы тем самым проделали некоторое вычисление на уровне объектов? Действительно, мы, как кажется, взяли число 2, прибавили к нему 2 и получили 4. Мы наблюдаем, таким образом, параллелизм вычислений на двух уровнях -- уровне объекта и уровне выражения, то есть уровне синтаксиса и уровне семантики. Благодаря этому параллелизму мы фактически производим операции с объектами посредством операций со знаками. Спросим теперь: какова форма связи, устанавливаемая этой функцией на предметном уровне? Мы знаем эту форму на уровне выражения, она задана правилами арифметики, содержащимися в её синтаксисе. В силу описанного параллелизма мы должны, следовательно, полагать, что функция на уровне самих чисел имеет ту же самую форму.

Таковы, по-видимому, рассуждения Фреге. Мартин-Лёф соглашается с ними в целом, однако меняет в них порядок. Если Фреге от выражений переходит к объектам, то Мартин-Лёф начинает с объектов и переходит к выражениям. Мы всегда начинаем с предмета, и Мартин-Лёф, снова соглашаясь с Гуссерлем, подчёркивает, что выражение является выражением, только если выражает нечто:

Оно является выражением в настоящем смысле слова, только если было получено путём формализации из чего-то, что с самого начала было осмысленно. Именно поэтому каждый раз, когда мы имеем выражение, мы можем смело говорить о его смысле, поскольку этот смысл есть попросту объект, из которого выражение было получено путём формализации. (Martin-Lof, 1993, 84)

Здесь, однако, имеется неясность. С одной стороны, Гуссерль, как мы видели, предполагает, что существует уровень смысла, предшествующий выражению. В то же время этот «“не-эксплицированно” ноэматический смысл [...] всегда возможно эксплицировать» (Husserl, 2009, 414). Это, как кажется, совпадает с описанием формализации у Мартин-Лёфа. Однако, с другой стороны, мы можем понимать последнюю и так, что сама форма появляется как результат этого процесса. Тогда то структурирование, о котором говорит Мартин-Лёф выше, является, скорее, появлением формы для изначально неструктурированного объекта. И тогда остаётся неясным, предполагает ли Мартин-Лёф, подобно Гуссерлю, осмысленный (то есть структурированный) объект прежде и помимо его выражения. В любом случае они оба, как мы видим, полагают возможным «извлечение» формы объекта, приводящее к параллелизму синтаксического и семантического. Чтобы лучше понять характер этого параллелизма, нам нужно рассмотреть, что Мартин-Лёф понимает под очевидностью.

2. ОЧЕВИДНОСТЬ. СМЫСЛ И ПРЕДМЕТ

Одно из ключевых отличий интуиционистской математики от классической состоит в том, что она опирается на понятие доказательства, а не истинности. Истина же понимается как производная от доказательства: истинно то, что доказано или может быть доказано. Будучи интуиционистской системой, теория типов Мартин-Лёфа также основана на понятии доказательства. Это приводит к переосмыслению понятия пропозиции. Если традиционно под пропозицией понимается то, чему мы приписываем истинность или ложность, то в теории типов пропозиция -- это то, что может быть доказано или опровергнуто (причём опровержение также сводится к доказательству -- доказательству особой пропозиции). При этом не только истинность, но и смысл пропозиции также основан на доказательстве: понимать пропозицию -- значит понимать, что может служить её доказательством. В своей интерпретации интуиционистской логики Гейтинг понимает пропозицию как ожидаемое доказательство. Например, ожидаемое доказательство для конъюнкции A ЛB состоит из пары, состоящей из доказательства A и доказательства B, ожидаемое доказательство для импликации A ^ B состоит из способа, каким из каждого доказательства A можно вычислить доказательство B, и т.д. В аналогичной интерпретации интуиционистской логики Колмогоровым пропозиция понимается как задача, определяемая возможными (то есть ожидаемыми) решениями. Этот подход получает свою формулировку в теоретико-доказательной семантике, которая возникает в логике Герхарда Генцена и Дага Правица и философски осмысляется Майклом Даммитом (Dummett, 1975). Последний даёт следующую сводку этой семантики:

Мы должны, таким образом, заменить понятие истины как центральное понятие теории смысла (meaning) математических утверждений на понятие доказательства (proof): схватывание смысла утверждения состоит в способности опознать его доказательство, когда оно нам представлено, а схватывание смысла любого выражения, меньшего предложения, должно состоять в знании способа, каким его присутствие в предложении вносит вклад в определение того, что следует считать доказательством этого предложения. (Dummett, 1978, 225-226)

Здесь доказательство пропозиции представляет собой объект (в частности, положение вещей), который мы способны опознать как таковой. Именно это понимание позволяет Гейтингу ссылаться на Гуссерля и понимать доказательство как объект, исполняющий интенцию См. уже цитированную статью: (Bentzen, 2023).. Мы вернёмся к этому ниже, а сейчас продолжим рассмотрение понятия пропозиции.

Всё сказанное позволяет понимать пропозицию как множество -- точнее говоря, тип -- её доказательств См., например: (Martin-Lof, 1984, 13).. В логике это приводит к соответствию Карри-Ховарда или принципу «пропозиция как тип». Таким образом, тип оказывается общим понятием, разновидностями которого служат множества и пропозиции (а кроме них также задачи, компьютерные программы и пр.). Аналогично типу вообще, чтобы понять или объяснить пропозицию, нам нужно понять или объяснить, что может служить её доказательством и какие два доказательства считаются равными. Мы можем считать пропозицию одним из вариантов множества (множеством доказательств), но можем, эквивалентно, считать множество особым родом пропозиции (например, такой, доказательством которой является просто объект, а не ситуация или положение вещей). В любом случае, объяснения их смысла и правила обращения с ними оказываются одинаковыми с точностью до замены слов. Это приводит к слиянию логики и теории множеств, они оказываются просто одной и той же теорией (Martin-Lof, 1993, 162-163). Например, приведённое выше правило построения пары можно понимать либо как правило построения элемента множества пар (то есть декартова произведения множеств A и B), либо как правило доказательства конъюнкции, которое говорит, что для доказательства конъюнкции пропозиций A и B следует составить пару из доказательства A и доказательства B. Построение доказательства -- это построение определённого объекта по определённым правилам.

Здесь требуется терминологическое пояснение. Мы можем понимать доказательство в трёх смыслах (Martin-Lof, 1987). Доказательством пропозиции является объект (например, пара доказательств для конъюнкции). Однако в некотором смысле мы можем говорить и о доказательстве суждения как о том, что служит основанием для его вынесения. Что может выступать доказательством суждения? Мартин-Лёф различает прямое и непрямое доказательство. Непрямое состоит в сведении суждения по определённым правилам к некоторой элементарной форме, которая уже допускает прямое доказательство. Таковы обычные доказательства в математике, они обозначаются термином demonstration в отличие от proof. Прямое же доказательство требует очевидности: «настоящее объяснение понятия доказательства суждения состоит в том, что оно есть то, что делает утверждение или суждение очевидным, или, если угодно, просто в том, что доказательство суждения -- это его очевидность (evidence). Таким образом, доказательство и очевидность -- это то же самое» (Martin-Lof, 1987, 417). Доказательство суждения -- это акт знания, понимания или узнавания, который основан на очевидности: «очевидность суждения есть сам акт его познания» (Martin-Lof, 1987, 418). Если доказательство пропозиции мы можем назвать свидетельством (одно из возможных значений нем. Evidenz и англ. evidence -- улика), то доказательство суждения есть знание о том, что это свидетельство действительно является свидетельством в пользу данной пропозиции. Речь здесь идёт об опознании или узнавании (Erkennen), на что, в частности, указывает и Гуссерль в «Логических исследованиях» (Husserl, 1921, VI, § 6). Именно в этом смысле акт суждения отождествляется с актом знания, понимания, схватывания, видения О терминологическом различении истинности пропозиции, очевидности суждения и пра-вильности доказательства см.: (Martin-Lof, 1987).. Например, непрямое доказательство математической теоремы -- это процесс доказывания этой теоремы, представленный деревом вывода (demonstration). В результате этого процесса мы получаем какой-то объект (доказательство как объект (proof)). Чтобы убедиться, что этот объект доказывает именно нужную нам теорему, нам требуется очевидность; нам должно быть ясно с очевидностью, что данное доказательство доказывает именно данную теорему. С аналогичным доказательством как очевидностью свидетельства мы также встречаемся, когда доказываем существование объектов какого-то типа предъявлением одного из таких объектов.

Описанный параллелизм логики и теории множеств делает проблематичным гуссерлевское разграничение формальной логики (теории значения) и формальной онтологии (теории предметов как таковых). Действительно, Гуссерль различает формы значения, к которым относятся формы составления пропозиций, связи пропозиций и пр., и формы предметности, которые относятся к описанию предметов как таковых. Понимание пропозиции как типа, напротив, приводит Мартин-Лёфа к слиянию логики и онтологии: имеется не просто корреляция, но тождество или изоморфизм логики и онтологии (Martin-Lof, 2002, 6). Выше мы уже встречались с этим изоморфизмом -- хотя и с другим его аспектом -- в понятии конструктора. Мы видели, что конструкторы задают форму -- как синтаксическую, то есть логическую, так и онтологическую, то есть форму объекта. При этом различаются канонические и неканонические объекты. Неканонические объекты могут быть редуцированы к каноническим и, в этом смысле, относятся к соответствующему типу, однако смысл типа определяется только его каноническими объектами, то есть конструкторами. Например, выражения «2 + 2» и «2²» являются неканоническими объектами, равными одному и тому же каноническому объекту s(s(s(s(0)))) (то есть 4), к которому они могут быть сведены (редуцированы) благодаря вычислению. Если Фреге в этом случае говорит, что эти выражения являются разными смыслами, указывающими на одно и то же значение (Frege, 1966, 7), то Мартин-Лёф рассматривает их как один и тот же объект, но по-разному выраженный: «Фреге, таким образом, всегда начинает с выражений, но сдвигая центр тяжести с выражений на объекты, мы получаем более естественный способ описания этой ситуации: мы просто говорим, что объекты те же самые, рассматриваемые как объекты, но они по-разному выражены» (Martin-Lof, 1993, 113). Это позволяет ему говорить:

Тогда как у Гуссерля имелся разрыв между Bedeutung und Gegenstand и Bedeutungskategorien und gegenstandliche Kategorien, у нас нет такого разрыва между двумя видами категорий. С другой стороны, внутри этих категорий мы имеем различие между объектами, которые представлены канонически и которые представлены неканонически. (Martin-Lof, 2002, 11)

Насколько, однако, непреодолим у Гуссерля разрыв, о котором здесь идёт речь? Как формальная логика, так и формальная онтология являются эйдетическими дисциплинами Используя немного другую терминологию, Гуссерль в Формальной и трансцендентальной логике говорит о формальной апофантике (учении о выражениях) и формальной онтологии (учении о предметах) как двух сторонах формальной логики.. Их различие состоит в фокусе -- на формах знаний либо на формах предметов. Но в то же время мы можем переходить от первого ко второму «путём поворота»:

Любой формально-логический закон можно обратить путём поворота в закон формально-онтологический. Тогда мы судим: вместо суждений -- о положениях дел, вместо членов суждения (например, именных значений) -- о предметах, вместо значений предиката -- о признаках и т. д. И речь уже не идёт об истине, о значимости предложений суждения, но о составе положений дел, о бытии предметов и т. д. (Husserl, 2009, 458)

Гуссерль добавляет, что формальная онтология превышает то, что задано этим соответствием; она также содержит различные субстантивации, которые Гуссерль называет номинализациями (так, например, множественное число на уровне выражения переходит в множество как объект на уровне онтологии). Однако логико-онтологический параллелизм у него, как мы видим, имеет место. Другое дело, что он отличается от изоморфизма, который мы встречаем у Мартин-Лёфа. Впрочем, сам Мартин-Лёф признаёт как наличие корреляции, так и её отличие от описанного изоморфизма.

Таким образом, о доказательстве как объекте мы говорим применительно к пропозициям, относительно же суждения мы говорим об очевидности или доказательстве в несобственном смысле. Хотя Мартин-Лёф здесь прямо ссылается на Гуссерля, ситуация не столь проста. Обсуждая в «Идеях» феноменологическую очевидность, Гуссерль указывает на несколько её разновидностей. Какую из них мы можем соотнести с очевидностью доказательства? Гуссерль выделяет «первозданно/оригинально дающее “видение”» (das origindr gebende „Sehen“), которое есть «живое усмотрение», «исключающее бытие-иначе (Anderssein)» (Husserl, 1976, 314 ff.). Оно представляет собой первичное переживание предмета, в отличие от вторичного воспоминания, воображения и т. д. Оно характеризуется исполнением (Erfullung), которое Гуссерль называет очевидностью или переживанием очевидности (Evidenzerlebnis). В ней происходит совпадение смысла и предмета:

Однако там, где дающее созерцание адекватно и имманентно, там совпадают не смысл и предмет, но скорее первозданно исполненный смысл и предмет. Предмет есть именно то, что в адекватном созерцании как оригинальное «то самое» (Selbst) схвачено, положено, в силу первозданности усмотрено, в силу смысловой полноты и полного первозданного смыслового исполнения усмотрено абсолютно. (Husserl, 1976, 332)

Текст Гуссерля в этих параграфах «Идей» насыщен метафорами и кавычками, он с большим трудом подбирает подходящую терминологию. В любом случае его задача состоит в том, чтобы описать смысл как характеристику интенции, не зависящую от его исполненности или неисполненности. Важно понимать, что как смысл, так и предмет являются составляющими ноэмы, поэтому их сопряжение происходит «внутри» неё: «говоря о сопряжении (и специально “направлении”) сознания на его предметное, мы отсылаемся к наивнутреннейшему моменту ноэмы» (Husserl, 2009, 404). В чём состоит этот момент? Исполненность -- это характеристика смысла, его способа данности (Husserl, 2009, 424 ff.). Она характеризуется непосредственностью, очевидностью и достоверностью, когда мы понимаем, что исполненное, осуществлённое и есть то самое, что имеется в виду. Исполненность «мотивирована» «живым явлением» (Leibhaft-Erscheinen), то есть первозданной данностью, и состоит в единстве с мотивирующим: «по своему “ядру” очевидность есть единство разумного полагания со всем мотивирующим её по мере сущности» (Husserl, 2009, 426). Таким образом, исполненность характеризуется особой интенциональностью, в которой переживается не столько совпадение каких-то независимо данных сущностей, сколько единство смысла и его осуществления, реализации, исполнения.

Мы находим схожую структуру у Мартин-Лёфа. Действительно, смысл типа (например, пропозиции) определяется правилами построения его элементов и обращения с ними. Таким образом, правила содержат в себе объекты, осуществление или исполнение которых и является доказательством. Мартин-Лёф, говоря об объектах, употребляет слово object, однако, когда он приводит немецкие термины, то в них мы встречаем Gegenstand, gegenstandlich и пр., что по-русски обычно передаётся как «предмет», «предметный» и пр.; англ. object переводит здесь нем. Gegenstand, а не нем. Object. Поэтому можно сказать, что система правил Мартин-Лёфа конкретизирует структуру ноэмы Гуссерля, уточняя понятия смысла и предмета и их отношений внутри ноэмы. Однако в том, что касается исполнения, имеются существенные различия. Рассмотрим их подробнее.

Мартин-Лёф при обсуждении отношений формальной логики и формальной онтологии у Гуссерля (Martin-Lof, 2002) проводит различение смысла и референции (или предмета). Используя пример Гуссерля, он говорит, что «победитель при Йене» и «побеждённый при Ватерлоо» обозначают один и тот же смысл, а именно «Наполеон», но последний отличается от самого Наполеона как предмета. Смысл «Наполеон» представляет собой канонический объект, тогда как «победитель при Йене» и «побеждённый при Ватерлоо» -- это неканонические объекты, которые могут быть сведены к нему в результате вычислений, принимающих во внимание соответствующие определения. Все подобные объекты (отличные от самого Наполеона) Мартин-Лёф здесь называет интенсиональными объектами, а в других местах -- логическими объектами. Сохраняя понятие референции, он в то же время указывает, что она сама разделяется надвое:

Отношение референции, которое вы имеете, когда ссылаетесь на нечто в реальном мире или на нечто реальное, на город, или страну, или человека, или что бы то ни было, может, таким образом, состоять из двух частей. В первой части вы переходите -- в терминологии, которую мы используем в связи с теорией типов -- к каноническому имени этого объекта, а вторая часть -- это переход от канонического имени к самому человеку, или городу, или стране, или что там оно есть. (Martin-Lof, 2002, 10)

Мартин-Лёф полагает, что в математике референция хотя и сохраняется, но не содержит второй из указанных выше частей -- то есть математика занимается «структурами», а не «действительными» объектами. Мы видим здесь классическое различение Фреге между смыслом (Sinn) и значением/референтом (Bedeutung), хотя и несколько модифицированное. С точки зрения Фреге, мы имеем в этом примере два сложных знака: «победитель при Йене» и «побеждённый при Ватерлоо», которые имеют разный смысл, но один и тот же референт, а именно Наполеона. У Мартин-Лёфа, вследствие синтактико-семантического параллелизма, эти знаки соответствуют (неканоническим) объектам, которые редуцируются к одному и тому же каноническому и в конечном счёте ссылаются на действительного Наполеона. Однако применима ли эта схема к феноменологии? Идея эквивалентности этих понятий Фреге гуссерлевским восходит к Фёллесдалю (Follesdal, 1969, 1990). Действительно, некоторые высказывания Гуссерля могут предоставить для этого основания. Хотя он в «Логических исследованиях» возражает против предложения Фреге различать значения терминов Sinn и Bedeutung (Husserl, 2011, 53), это возражение выглядит как чисто терминологическое, оно не исключает, что Гуссерль проводит различение, о котором говорит здесь Фреге. Гуссерль лишь возражает против того, чтобы вводить лишнюю и затемняющую дело терминологию, называя предмет (Gegenstand) значением (Bedeutung). В Идеях Гуссерль, по его словам, «отдаёт предпочтение» Bedeutung, когда речь идёт об узком лингвистическом значении, и Sinn -- когда имеется в виду вся сфера ноэматического (Husserl, 2009, 385). Однако в целом он не различает эти два термина. Тем не менее в «Логических исследованиях» различие между смыслом или значением (Sinn/Bedeutung) и предметом (Gegenstand) Гуссерль описывает практически теми же словами, что и Фреге: «выражение обозначает (называет) предмет посредством своего значения, или: акт придания значения определённым способом подразумевает соответствующий предмет -- только как раз этот способ подразумевать, придавая значение, и, таким образом, само значение могут меняться при фиксированном тождестве предметной направленности» (Husserl, 2011, 50)¹¹. Однако в «Идеях» Гуссерль подчёркивает, что предмет может присутствовать в феноменологии только как переживаемый предмет, то есть в своей смысловой форме. Различие между исполненным и неисполненным смыслом состоит не в том, что в одном случае имеется, а в другом не имеется «реального» предмета референции. Речь, скорее, идёт об одном и том же предмете, но по-разному данном. Исполненность, оригинальная данность представляет собой особый род интенциональности, характеризуемый «живым» переживанием. Подход Гуссерля здесь онтологичен, и он прямо ассоциирует исполненность с бытием (Husserl, 2009, 425). По этой причине попытка Мартин-Лёфа представить эту структуру в терминах референции, пусть и переосмысленной в теории типов, вряд ли может быть успешной. Он опирается в своём анализе (Martin-Lof, 2002) на традиционное различение выражения, смысла и объекта, но остаётся большим вопросом, насколько оно применимо в феноменологии и даже в самой теории типов.