3.2. Доказательства как морфизмы

В разделе 2 были описаны различные категории: начиная от простых в чистом виде и  заканчивая моноидальными категориями, сплетёнными моноидальными категориями, симметричными моноидальными категориями и т. д., то есть категориями с дополнительными структурами. Тем не менее, авторы представили лишь часть чрезвычайно подробной классификации. Фактически же каждый тип категорий с дополнительными структурами соответствует некоторой логической системе со своими собственными правилами вывода!

Для подтверждения вышеупомянутого факта, далее в качестве объектов будут рассматриваться высказывания, а в качестве морфизмов — доказательства. Пусть  и  являются высказываниями. В этом случае доказательство, которое от предпосылки  ведёт к заключению , можно рассматривать в качестве морфизма . В следующем подразделе будет показано, что морфизмом на самом деле является класс эквивалентности доказательств, однако на данный момент это не представляет особой важности.

Пусть факт того, что имеется цепочка доказательств, которая из высказывания  получает высказывание , обозначается как . Правилом вывода называется метод получения нового доказательства из имеющихся. Например, практически в каждой логической системе верно, что если из  можно получить , а из  в свою очередь можно получить , то и из  можно получить . Данное правило вывода записывается следующим образом:

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

Также практически в каждой логической системе имеется доказательство, которое выводит высказывание из самого себя. Это правило вывода может быть записано так, что от ничего выводится существование доказательства из высказывания  в :

Это правило вывода должно напомнить то, что для каждого объекта в категории существует морфизм тождества: для произвольного объекта  автоматически имеется морфизм . Действительно, данное правило иногда называют «правилом тождества».

Если продолжить размышления в том же ключе, можно взять определение замкнутой симметричной моноидальной категории и вычленить из него набор правил вывода. Каждое правило будет описывать способ получения нового морфизма из имеющихся в замкнутой симметричной моноидальной категории. Существует несколько различающихся в деталях, но общих в сути способов перечисления таких правил. Вот один из них:

Звёздочка около метки правила (показанной справа от горизонтальной линии) обозначает, что обратное правило также действительно. Как было ранее указано, правила  и  соответствуют морфизму тождества и операции композиции в категории. Правила , ,  и  получены из определений тензорного произведения, ассоциатора и левого и правого определителей моноидальной категории. Правило  получено из определения переключателя в сплетённой моноидальной категории, а правило  получено из определения каррирования в замкнутой моноидальной категории.

Как же записать вышеперечисленные правила, используя термины логики? Данные правила описывают небольшой фрагмент исчисления высказываний. Для того чтобы это увидеть, необходимо читать связку  как «И», связку  как импликацию, а высказывание  как «ИСТИНА».

Тогда, например, правило  говорит о том, что доказательство от предположения « и » к заключению  можно преобразовать в доказательство от предположения  к заключению «из  следует »Так в оригинале. — прим. перев. . Обратное преобразование доказательств также верно. Данное правило верно в классической, интуиционистской и линейной логиках, как верны и другие правила. Правила  и , например, говорят о том, что связка «И» ассоциативна и коммутативна. Правило  утверждает, что доказательство из некоторого утверждения  в заключение «ИСТИНА и » может дать доказательство из утверждения  в заключение , и наоборот. Правило  говорит о том же.

Что дают эти правила? С их помощью можно строить цепочки вывода, «дедукции». Например:

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

Это правило называется Modus Ponens.

В общем виде дедукцию можно представить как дерево, созданное на основе правил вывода. Разветвления появляются при применении правила  или . Например:

Данную цепочку вывода можно так же использовать в сокращённом виде как дополнительное правило. Фактически, эта цепочка обратима:

Как более громоздкий пример можно рассмотреть высказывание . Цепочка вывода, которая ведёт к доказательству данного  высказывания, вряд ли даже поместится на странице, если не использовать дополнительные правила вывода:

Поскольку каждое из использованных правил вывода присутствует в замкнутой моноидальной категории (здесь не использовано правило переключения), следовательно во всех таких категориях существуют морфизмы внутренней композиции: . Эти морфизмы играют такую же роль для внутренних -морфизмов, какую играет композиция для обычных морфизмов: .

Можно пойти дальше и получить дополнительные цепочки вывода в данной логической системе, однако больший интерес для изучения представляет вопрос о том, что данная теория не допускает. Для начала можно указать, что в ней отсутствует связка «ИЛИ» и высказывание «ЛОЖЬ», а также два правила вывода, которые обычно полагаются данными «по умолчанию» — дублирование:

и ослабление:

Данные правила аналогичны операциям дублирования и удаления в декартовой категории. Их отсутствие является отличительной особенностью линейной логики [43]. Слово «линейный» должно напомнить о категории . Как указано в разделе 2.3, данная категория с её обычным тензорным произведением не является декартовой, так что в ней не разрешены дублирования и удаления. Однако как выражается отсутствие данных правил при оперировании терминами логики?

Обычная логика оперирует высказываниями, так что чаще всего высказывания используются и в вышеприведённой логической системе. Однако линейная логика оперирует не только высказываниями, но и другими типами «ресурсов» — например, физическими объектами! В отличие от высказываний в обычной логике, данные типы ресурсов нельзя так просто дублировать и удалять. В классической логике если известно, что высказывание  истинно, то его можно использовать столько раз, сколько необходимо для доказательства высказывания . Однако если имеется некоторое количество молока, его невозможно использовать вначале как ингредиент для кекса, а потом сбить масло из этого же количества молока. Также нельзя сделать так, чтобы данное количество молока бесследно исчезло: даже если его вылить, молоко должно куда-то деться.

Фактически, эти идеи знакомы по курсу химии. Например, пусть имеются:

•  — одна молекула водорода;

•  — одна молекула кислорода;

•  — одна молекула воды.

Можно сжечь водород, чтобы соединить одну молекулу кислорода с двумя молекулами водорода, чтобы получить две молекулы воды. Специалист по теории категорий может описать данную реакцию в виде морфизма:

Специалист по линейной логике может записать: 

для обозначения существования такого морфизма. Однако нет возможности дублирования или удаления молекул, так что, например:

равно как и:

где  обозначает единицу тензорного произведения (а не атом йода), то есть отсутствие молекул вообще.

По сути, обычные химические реакции являются морфизмами в симметричной моноидальной категории, в которой объекты суть наборы молекул. Как обычно представляют себе химики, данная категория не является замкнутой. Она подчиняется ещё более ограниченной логической системе, нежели той, что была описана ранее, — системе, в которой отсутствует связка . Для получения замкнутой категории — фактически, компактной, — необходимо вспомнить одно из величайших физических открытий XX века: антиматерию. Это позволяет определить  как «анти- и »: . В этом случае действительно правило каррирования:

Большинство химиков нечасто имеют дело с антиматерией, в отличие от физиков, работающих в области квантовых частиц. Они не используют понятия линейной логики или теории категорий, однако им известно, что поскольку нейтрино и нейтрон могут при столкновении породить протон и электрон — , то нейтрон может распасться на антинейтрино вместе с протоном и электроном: . Это есть проявление правила каррирования, правила . 3.3. Логические теории из категорий Выше было упомянуто, как различные логические системы могут быть получены из различных типов категорий. Для наглядности будет введена новая логическая система, правила вывода которой основаны на методах получения новых морфизмов из имеющихся в замкнутой симметричной моноидальной категории. Таким же способом можно использовать другие типы категорий и получить новые логические системы.

Для того чтобы сделать взаимосвязь между теорией доказательств и теорией категорий более ярко выраженной, ниже будет описан способ получения логической теории из произвольной замкнутой симметричной моноидальной категории. Понятие  будет использоваться для обозначения множества доказательств — точнее, классов эквивалентности доказательств, ведущих от предположения  к заключению . Ранее понятие  использовалось только в случае, если множество доказательств непусто; в противном случае использовалось понятие . Польза от трактовки выражения  в качестве множества заключается в полном соответствии с  — множеством морфизмов в категории.

Если принять, что выражение  обозначает множество морфизмов, то правило вывода становится функцией из произведения множеств морфизмов в одиночное множество морфизмов. Например, правило сечения:

становится ещё одним способом выражения композиции функций: , в то время как правило тождества:

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

Далее, если трактовать правила вывода в качестве функций из произведений множеств морфизмов в множества морфизмов, цепочки выводов становятся более сложными функциями того же вида, построеными на основе базовых функций. Например, следующая цепочка вывода:

определяет функцию, которая отображает  в множество морфизмов  и построена на основе базовых правил, обозначаемых отметками сбоку горизонтальных линий. Данная цепочка:

даёт ещё одну функцию из  в то же множество морфизмов .

Если размышлять о цепочках вывода как о функциях, то возникает вопрос, когда такие функции эквивалентны. В вышеприведённом примере треугольное правило в определении моноидальной категории (Определение 7):

говорит о том, что две данные функции эквивалентны. В самом деле, треугольное правило является в точности утверждением того, что две данные функции согласуются (доказательство предоставляется читателю).

Итак, даже если две цепочки вывода кажутся различными, они могут дать одну и ту же функцию из произведения множеств морфизмов во множество морфизмов, если есть требование, что данные множества морфизмов находятся в замкнутой симметричной моноидальной категории. Именно поэтому утверждается, что выражение — это множество классов эквивалентности доказательств, а не просто доказательство, что вынуждает использование теории категорий. Этого можно избежать, если использовать 2-категории с доказательствами в качестве морфизмов и «эквивалентностями между доказательствами» в качестве 2-морфизмов [84], что ведёт далее по периодической системе (Таблица 3). Однако прежде всего необходимо сделать несколько важных определений в качестве обобщения.

Здесь и далее объекты ,  и т. д. будут называться «высказываниями», несмотря на то, что они могут представлять собой более общие понятия. Также для упрощения разъяснений далее будет использоваться слово «доказательство» в значении «класс эквивалентности доказательств». Отношение эквивалентности должно быть достаточно приблизительным, чтобы выражения из следующего определения были истинными:

Определение 19. Замкнутая моноидальная теория состоит из следующих компонентов:

• Набор высказываний. Набор должен содержать высказывание , а также высказывания  и  для двух произвольных высказываний  и .

• Для каждой пары высказываний  и  множество  доказательств, ведущих от высказываний  к высказыванию . Если , то это записывается как .

• Некоторые функции, записанные в виде правил вывода:

Двойная линия обозначает, что правило обращаемо. Тогда, к примеру, для произвольной тройки объектов ,  и  имеется функция  и биекция .

• Определённые выражения, которые должны подчиняться правилам вывода. Правила вывода  и  должны подчиняться выражениям, описывающим законы ассоциативности и наличия левой и правой единицы. Правило  должно подчиняться выражению, которое утверждает, что оно является функтором. Правила , ,  и  должны подчиняться выражению, которое утверждает, что данные правила являются естественными преобразованиями. Правила , ,  и  также должны подчиняться треугольному и пятиугольному выражениям.

Определение 20. Замкнутая сплетённая моноидальная теория является замкнутой моноидальной теорией с дополнительным правилом вывода:

Требуется, чтобы данное правило подчинялось выражению для естественных преобразований и шестиугольному выражению.

Определение 21. Замкнутая симметричная моноидальная теория является замкнутой сплетённой моноидальной теорией, в которой правило  является своим собственным обращением.

Это определения различных видов замкнутых категорий — моноидальной, сплетённой и симметричной, но записанные иначе, что позволяет создавать данные категории на основе логических систем. Для этого в качестве объектов берутся высказывания, а в качестве морфизмов берутся классы эквивалентности доказательств, где отношение эквивалентности генерируется уравнениями, перечисленными в определениях.

Однако наиболее полно плюсы нового способа записи проявятся, если основательней исследовать теорию доказательств и обобщить выражения вроде  до последовательностей вроде . Подобные последовательности можно приблизительно представить как выражения вида . Польза от применения данных последовательностей заключается в том, что у всех правил вывода, кроме правил сечения и тождества, имеется правило подформулы, которое было упомянуто в разделе 3.1.

Логика замкнутых симметричных моноидальных категорий, сформулированная с применением правил вывода известна под названием «мультипликативная интуиционистская линейная логика», для краткости  МИЛЛ [48, 82]. Для МИЛЛ справедлива теорема о удалении правила сечения, утверждающая, что при должном выборе иных правил вывода правило сечения становится излишним: любое доказательство, которое можно провести с его помощью, можно провести и без него. Это очень знаменательно, поскольку правило сечения соответствует операции композиции морфизмов в теории категорий. Одним из следствий данной теоремы является то, что в свободной симметричной моноидальной замкнутой категории над любым множеством объектов множество морфизмов между произвольной парой объектов конечно. Также имеется процедура, при помощи которой можно проверить, являются ли два морфизма эквивалентными. Подобное описание можно найти в диссертации Т. Тримбла [95] и статьях К. Б. Джея [54] и С. Соловьёва [90]. Также можно изучить теорему о когерентности Келли и МакЛейна для замкнутых симметричных моноидальных категорий [61], а также схожую теорему для компактных симметричных моноидальных категорий [62].

МИЛЛ является одной из многих сходных логических систем. Большинство из них включают в себя дополнительные возможности, однако некоторые, наоборот, возможности исключают. Вот несколько примеров:

• Алгебраические теории. В своей знаменитой диссертации Ф. В. Лаувер [69] определил алгебраическую теорию как декартову категорию, в которой каждым объектом является -арное декартово произведение  () определённого объекта . Он показал, как такие категории соотносятся с логическими системами простого вида — ранее они изучались под названием «универсальных алгебр» [25]. Данная работа положила начало теоретико-категориальну подходу к изучению логики, который был кратко описан в настоящей работе. Книга Р. Л. Крола [34] даёт небольшое введение в алгебраические теории и более сложные логические системы. В более широком понимании произвольная декартова категория является обобщённой алгебраической теорией.

• Интуиционистская линейная логика (ИЛЛ). ИЛЛ дополняет МИЛЛ операциями, известными из интуиционистской логики, а также оператором , который преобразует произвольное высказывание (или ресурс)  в «бесконечный склад копий ». Существует удобная теоретико-категориальная интерпретация. Диссертация Дж. Бирмана [23] даёт неплохой обзор, включая доказательство теоремы об удалении сечения для ИЛЛ и доказательство результата, изначально выдвинутого Ж.-И. Жираром, что интуиционистская логика может быть погружена в ИЛЛ.

• Линейная логика (ЛЛ). Полноценная линейная логика является удачной отправной точкой для изучения (неплохой обзор в сети Интернет — статья Р. Ди Космо и Д. Миллера [37]). Для более детального изучения можно просмотреть оригинальную статью Ж.-И. Жирара [43] и книгу А. С. Троельстры [96]. Обзорная статья Р. Блута и П. Скотта [24] может стать новым Розеттским камнем для линейной логики и теории категорий. Этой же цели послужат лекции А. Шалка [82].

• Интуиционистская логика (ИЛ). Классическая книга Дж. Ламбека и П. Дж. Скотта [67] до сих пор остается отличным введением в интуиционистскую логику и замкнутые декартовы категории. Обзорная статья Дж. Московакиса [77], доступная в сети Интернет, содержит множество ссылок для дальнейшего изучения.

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

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

С этой точки зрения большинство правил вывода являются естественными преобразованиями. Например, правило вывода  является естественным преобразованием между двумя функторами из  в , а именно из функторов  в функторы . Это естественное преобразование переводит произвольное доказательство  в доказательство . Поскольку данное преобразование является естественным, это обозначает, что оно изменяется симметричным образом при использовании различных , ,  и . Коммутирующее квадратное правило в определении естественного преобразования делает придаёт утверждению точность.

Правила вывода , ,  и  дают естественные преобразования такого же вида. Правило  даёт естественное преобразование между двумя функторами из  в , а именно между  и . Данное естественное преобразование отображает произвольный элемент  в .

Правила тождества и сечения другие: они не дают естественных преобразований, потому что над горизонтальной линией данных правил находится иное количество переменных, по сравнению с количеством переменных под линией. Правило вывода  утверждает, что для каждого объекта  существует константная функция , которая возвращает морфизм тождества . Что значит естественность преобразования в ? Правило  утверждает, что для тройки произвольных объектов  существует функция . Что значит естественность преобразования в ,  и ? Ответ на оба вопроса приводит к обобщению естественных преобразований, называемому «диестественным» преобразованиемВ английском языке существует логичная связь между словами natural и dinatural, в связи с чем введён термин «диестественный» — прим. перев.  [71].

По Определению 4 естественные преобразования  между двумя функторами  коммутируют некоторые квадраты в категории . Если фактически , то в категории  появляются коммутирующие кубы. А именно: естественное преобразование  назначает каждому объекту  такой морфизм , что для каждого морфизма  в категории  следующий куб коммутирует:

Если , то можно выбрать один объект  и один морфизм , после чего использовать их в обоих слотах. Как показано на Рисунке 1, существует два пути из одного угла куба в противоположный угол, которые применяют  к повторяющимся элементам, то есть  и , но не  или . Эти пути составляют коммутирующий шестиугольник, что дает основание следующему:

Определение 22. Диестественным преобразованием  между двумя функторами , назначающими каждому объекту  морфизм  такой, что для каждого морфизма  шестиугольник на Рисунке 1 коммутирует.

Рисунок 1. Естественное преобразование между функторами  даёт коммутирующий куб в категории  для каждого морфизма , и существует ровно два пути в кубе, которые применяют  к повторяющимся элементам

В случае правила тождества коммутирующий шестиугольник появляется из-за того, что морфизм тождества является левой и правой единицей для композиции — см. Рисунок 2. Для правила сечения коммутирующий шестиугольник утверждает, что операция композиции ассоциативна — см. Рисунок 3.

Рисунок 2. Диестественность правила вывода , где . Здесь  обозначает единственный элемент в синглетоне

Рисунок 3. Диестественность правила сечения, где , , 

Таким образом, обсуждаемый вид логических теорий затрагивает следующие понятия:

• Категорию  высказываний и доказательств.

• Функтор , который отображает произвольную пару высказываний во множество доказательств от первого ко второму.

• Множество диестественных преобразований, описывающих правила вывода.