Теория типов Мартина-Лёфа как мультиагентная формальная эпистемическая система

Эпистемология и философия науки 2018. Т. 55. № 4. С. 44-47 УДК 161.22

Epistemology & Philosophy of Science 2018, vol. 55, no. 4, pp. 44-47 DOI: 10.5840/eps201855464

I ЕОРИЯ ТИПОВ МАРТИНА-ЛЁФА КАК МУЛЬТИАГЕНТНАЯ ФОРМАЛЬНАЯ ЭПИСТЕМИЧЕСКАЯ СИСТЕМА*

Родин Андрей Вячеславович - кандидат философских наук, старший научный сотрудник.

Институт философии РАН. Российская Федерация, 109240, г. Москва, ул. Гончарная, д. 12, стр. 1. Национальный исследовательский университет «Высшая школа экономики». Российская Федерация, 105066, г. Москва, Старая Басманная ул., д. 21/4; email: andrei@philomatica.org

Ранта безосновательно называет произвольные подстановки переменных из одних контекстов ТТМЛ в другие «расширениями контекстов», предполагая при этом, что контексты всегда формируют частичный порядок. Однако хорошо известно, что это не так: в общем случае категория контекстов ТТМЛ представляет собой локально декартово замкнутую категорию. Поэтому предложенное Домановым понимание таких подстановок как взаимных интерпретаций знаний, относящихся к различными эпистемическими агентам, является более адекватным. Предложенный Домановым анализ может быть усовершенствован, если эта точка зрения будет проведена более последовательно, чем это сделал Доманов в обсуждаемой статье.

Ключевые слова: конструктивная теория типов, интерпретации контекстов, эпистемический агент

M ARTIN-LÖF TYPE THEORY AS A MULTI-AGENT EPISTEMIC FORMAL SYSTEM

Andrei V. Rodin - Ph.D in Philosophy, senior research fellow.

Institute of Philosophy, Russian Academy of Sciences. 12/1 Goncharnaya St., Moscow, 109240, Russian Federation.

National Research University "Higher School of Economics". Staraya Basmannaya Str., 21/4, Moscow, 105066, Russian Federation; e-mail: andrei@philomatica.org

Ranta's view that all substitutions of variables between MLTT contexts in some sense "extend" these contexts, so the MLTT contexts always form a partial order, is not justified. It is well known that the category of MLTT contexts is, generally, locally Cartesian closed but not necessarily a poset. Thus, Domanov's reading of such general substitutions as mutual interpretations between contexts, which represent their corresponding epistemic agents, is more adequate. The formal analysis offered by Domanov can be improved if this latter viewpoint is developed more systematically than the author does it in his paper.

Keywords: constructive type theory, interpretations of contexts, epistemic agent

Статья Олега Доманова представляет собой оригинальную попытку формального анализа пропозициональных установок эпистемическо-го характера с помощью конструктивной теории типов Мартина-Лёфа (ТТМЛ) [Martin-Löf, 1984] - на конкретном примере проблематичного предложения, который автор заимствует у Куайна. Этот анализ основан на прочтении синтаксических выражений вида а:А в ТТМЛ как суждений "А известно на основании свидетельства (доказатель-

* Статья подготовлена при поддержке РФФИ, проект № 16-03-00364-0гн «Логические и эпистемологические аспекты конструктивного знания».

44 © Родин А.В.

ТЕОРИЯ ТИПОВ МАРТИНА-ЛЁФА...

ства) а". Доманов также использует техническое понятие контекста как ТТМЛ-выражения особого рода, которое представляет сумму некоторого наличного знания.

Стандартный анализ примеров того типа, к которому принадлежит анализируемый автором пример Куайна, использует контраст между (0 положением дел, которое описывается стандартными логическими средствами и (и) тем, что об этом положении дел известно некоторому эпистемическому агенту (в примере Куайна его зовут Ральфом). Поскольку все суждения и все контексты в ТТМЛ имеют эпистемический характер, эта теория не дает возможности сначала оценивать истинность высказываний в чисто онтологической перспективе безотносительно к знаниям об этом положении дел, а уже потом включать в рассмотрение знания различных эпистемических агентов об этом положении дел, а также знания отдельных агентов о знаниях других агентов, как это делается в мультиагентных эписте-мических логиках, которые являются расширениями классической логики. Поскольку такой классический подход приводит к известным парадоксам, есть все основания испробовать альтернативные пути формализации, что и делает Доманов.

Доманов использует прием, который позволяет ему использовать ТТМЛ в качестве мультиагентной эпистемической системы. Для этого он использует введенное Ранта понятие расширения контекста Г как такого контекста Д, в котором контекст Г может быть интерпретирован [3]. С синтаксической точки зрения такая интерпретация представляет собой подстановку переменных из одного контекста в другой контекст.

Оригинальный ход Доманова в этом вопросе состоит в том, что он использует понятие расширения контекста для целей, которые Ранта перед собой не ставит. Ранта вводит понятие расширения контекста для описания приращения знаний по аналогии с тем, как это делается в семантиках в стиле Крипке для модальных и, в частности, эпистеми-ческих логик. Доманов же использует понятие расширения контекста для описания того, как данный эпистемический агент интерпретирует знания другого такого агента. Свой анализ примера Куайна Доманов начинает с того, что рассматривает «контекст Ральфа» и контекст, который он называет «актуальным», а в дальнейшем по техническим причинам вводит в рассмотрение еще один «общий» контекст. Актуальный контекст описывает у Доманова знания того агента, который делает анализируемое высказывание о Ральфе (то есть «наше» знание); общий контекст играет в конструкции Доманова вспомогательную роль и не приписывается какому-либо отдельному агенту.

Насколько правомочно такое расширительное использование Домановым понятия расширения контекста, которое он заимствует у Ранта? Ранта приходит к своему общему определению расширения

А.В. РОДИН

контекста как интерпретации, рассматривая различные способы приращения знаний и указывая на то, что всякое такое приращение можно описать как интерпретацию старого знания в новом. Далее Ранта аргументирует, что всякую интерпретацию одного данного контекста в другом можно и нужно понимать как приращение знания. Аргумент состоит в том, что если все пропозиции и их доказательства из контекста Г интерпретируются в новом контексте Д, то "все что мы знаем" в Г, «мы также знаем» в Д [Ranta, 1994, р. 147]. Но этот аргумент очевидно ошибочный. Если различные пропозиции и доказательства в Г интерпретируются в Д одинаково - что формально допустимо -то скорее нужно сказать происходит потеря знаний. Понятие расширения контекста с формальной стороны предполагает, что контексты частично упорядочены "по объему". Однако хорошо известно, что в общем случае это не так. Категория контекстов ТТМЛ в общем случае - это локально декартово замкнутая категория [Pitts, 2001], а не частичный порядок. Нетрудно построить простые примеры, когда Г интерпретируется в Д, а Д в свою очередь интерпретируется в Г, причем композиции этих интерпретаций слева и справа не являются тождествами, то есть Г и Д не равны и не изоморфны (нарушая таким образом свойство антисимметрии частичного порядка).

Таким образом, вопреки Ранта, вовсе не всякая интерпретация контекстов имеет характер приращения знаний, а только такая интерпретация, которая задана в виде инъективного отображения, которое позволяет полностью восстановить старый контекст по его образу в новом контексте. Поэтому использование Домановым технического понятия об интерпретации контекстов за пределами ситуации расширения знаний, на наш взгляд, совершенно оправдано. Более того, я думаю, что подход Доманова может быть более эффективным, если вместо «расширение контекста» просто использовать термин «интерпретация» и окончательно отказаться от идеи, что интерпретирующий контекст должен быть обязательно более широким по сравнению с интерпретируемым. Таким образом, по всей видимости, можно избавиться от введения искусственного «общего контекста» в предложенном Домановым анализе примера Куайна.

Как замечает Доманов в Заключении своей статьи, ни одно из предложенных им формальных реконструкций проблематичного предложения нельзя с очевидностью назвать чтением de re. Это важное замечание показывает, что предложенное Домановым решение проблемы Куайна с помощью конструктивной логической системы будет неудовлетворительным для любого логика и философа, который посчитает отказ от убедительного чтения de re уходом от проблемы, а не ее решением. Это замечание, разумеется, совсем не умаляет ценности чисто конструктивного решения, предложенного Домано-вым, но оно показывает, что это решение не является окончательным.

ТЕОРИЯ ТИПОВ МАРТИНА-ЛЕФА..

Подход Доманова также допускает критику с конструктивной точки зрения. Хотя МЛТТ и располагает существенными ресурсами для описания эпистемических контекстов, использование МЛТТ в ее первоначальном виде в качестве мультиагентной эпистемической системы может быть только очень ограниченным. Отождествление эписте-мического агента с конкретным контекстом представляется слишком прямолинейным; такое формальное представление эпистемического агента выглядит слишком упрощенным для многих эпистемических ситуаций; в частности такой агент не может получать новых знаний и забывать старые знания. Эти ограничения не играют роли для решения той ограниченной задачи, которую поставил перед собой Доманов, однако чтобы с помощью МЛТТ или подобных исчислений построить эффективную мультиагентную эпистемическую формальную систему требуются значительные дополнительные усилия.

Список литературы / References

Martin-Lof, 1984 - Martin-Lof, P. Intuitionistic Type Theory. Notes by Giovanni Sambin of a series of lectures given in Padua, June 1980. Napoli: Bibliopolis, 1984. 91 pp.

Pitts, 2001 - Pitts, A. "Categorical logic", in: Abramsky, S., Gabbay, D. M., Maibaum, T. S. E. (eds.), Handbook of Logic in Computer Science, vol. 5. Oxford: Oxford University Press, 2001, pp. 39-128.

Ranta, 1994 - Ranta, A. Type-Theoretical Grammar. Oxford: Clarendon Press, 1994. 226 pp.