Первое суждение означает, что 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. Мы наблюдаем, таким образом, параллелизм вычислений на двух уровнях -- уровне объекта и уровне выражения, то есть уровне синтаксиса и уровне семантики. Благодаря этому параллелизму мы фактически производим операции с объектами посредством операций со знаками. Спросим теперь: какова форма связи, устанавливаемая этой функцией на предметном уровне? Мы знаем эту форму на уровне выражения, она задана правилами арифметики, содержащимися в её синтаксисе. В силу описанного параллелизма мы должны, следовательно, полагать, что функция на уровне самих чисел имеет ту же самую форму.
Таковы, по-видимому, рассуждения Фреге. Мартин-Лёф соглашается с ними в целом, однако меняет в них порядок. Если Фреге от выражений переходит к объектам, то Мартин-Лёф начинает с объектов и переходит к выражениям. Мы всегда начинаем с предмета, и Мартин-Лёф, снова соглашаясь с Гуссерлем, подчёркивает, что выражение является выражением, только если выражает нечто: