Оно является выражением в настоящем смысле слова, только если было получено путём формализации из чего-то, что с самого начала было осмысленно. Именно поэтому каждый раз, когда мы имеем выражение, мы можем смело говорить о его смысле, поскольку этот смысл есть попросту объект, из которого выражение было получено путём формализации. (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» и «22» являются неканоническими объектами, равными одному и тому же каноническому объекту 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)11. Однако в «Идеях» Гуссерль подчёркивает, что предмет может присутствовать в феноменологии только как переживаемый предмет, то есть в своей смысловой форме. Различие между исполненным и неисполненным смыслом состоит не в том, что в одном случае имеется, а в другом не имеется «реального» предмета референции. Речь, скорее, идёт об одном и том же предмете, но по-разному данном. Исполненность, оригинальная данность представляет собой особый род интенциональности, характеризуемый «живым» переживанием. Подход Гуссерля здесь онтологичен, и он прямо ассоциирует исполненность с бытием (Husserl, 2009, 425). По этой причине попытка Мартин-Лёфа представить эту структуру в терминах референции, пусть и переосмысленной в теории типов, вряд ли может быть успешной. Он опирается в своём анализе (Martin-Lof, 2002) на традиционное различение выражения, смысла и объекта, но остаётся большим вопросом, насколько оно применимо в феноменологии и даже в самой теории типов.