Применения логических исчислений к изучению естественных преобразований в категориях

Соловьев, Сергей Владимирович

Применения логических исчислений к изучению естественных преобразований в категориях тема автореферата и диссертации по математике, 01.01.06 ВАК РФ

Соловьев, Сергей Владимирович АВТОР

кандидата физико-математических наук УЧЕНАЯ СТЕПЕНЬ

Ленинград МЕСТО ЗАЩИТЫ

1984 ГОД ЗАЩИТЫ

01.01.06 КОД ВАК РФ

Диссертация по математике на тему «Применения логических исчислений к изучению естественных преобразований в категориях»

Содержание диссертации автор исследовательской работы: кандидата физико-математических наук, Соловьев, Сергей Владимирович

ВВЕДЕНИЕ

I. Одаой из важных тем общей теории категорий является изучение естественных преобразований б категориях, снабженных дополнительнойктурой, состоящей из выделенных объектов, выделенных функторов (чаще всего в этой роли фигурировали функторы типа тензорного произведения, внутреннего 1гопг -функтора, прямой суммы или прямого произведения) и выделенных естественных преобразований (типа естественного изоморфизма коммутативности тензорного произведения, естественного изоморфизма сопряженности тензорного произведения и внутреннего К^-функтора, или естественных проекций прямого произведения), при условии, что все эти данные подчиняются определенным соотношениям (скажем, ОС - \ , где С обозначает естественный изоморфизм коммутативности тензорного произведения)

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

Рассматривались в основном задачи, связанные с естественными преобразованиями, которые могут быть представлены некоторыми термами, построенными из символов выделенных естественных, преобразований при помощи символов выделенных функторов и символа композиции (тавив естественные преобразования мы будем называть, в духе работ С.Маклейна [2] , [25] каноническими естественными преобразованиями; их точное определение для рассматриваемых в этой работе типов категорий дается ниже, в

§ 2), в частности задачи о корегентнооти канонических естественных цреобразований (верно ли, что все диаграммы в том иди ином классе диаграмм канонических естественных цреобразований комздутативны).

Полученные результаты находили применение в различных областях математики: ври построении бесконечнократннх пространств петель в алгебраической топологии (см. [2] , [4] , [5] ); при построении "длинных точных последовательностей" в гомологической алгебре [6]; при определении операций Стинрода в абелевых категориях [7] и т.д. Н.П.Титов нашел неожиданные применения результатов о когерентности к вопросам описания работы систем ЭВМ [8 ] •

2. В ряде случаев для решения задач упомянутых типов с успехом применялась теория исчислений. Связующим звеном между теорией категорий и теорией исчислений служит тот факт, что с классом категорий, имеющих заданную дополнительную структуру, может быть связано (вообще говоря, многими способами) некоторое исчисление секвенциального типа, которое оказывается свободной категорией того же класса при следующем "распределении ролей": формулы играют роль объектов; роль морсоизмов из А в В отводится класоам эквивалентных друг другу выводов секвенции А-В (или их кодов) при некотором отношении эквивалентности =■ , оцределяемом на основании соотношений, выполнение которых требуется в рассматриваемом классе категорий (в частности, класс эквивалентности аксиомы А^А играет роль единичного морфизма); роль композиции играет правило сечэния ——^—^ ; роль функторов играют пропозициональные связки (на объектах) и правила введения соответствующей связки на морфизмах); роль естественных преобразований играют схемы аксиом или иногда (например, для изоморфизмов сопряженности) правила вывода.

Впервые, по-видимому, начал применять исчисления для изучения канонических естественных преобразований И.Ламбек (см. [9] - [И]), обнаруживший не только связь мевду исчислениями и категориями, имевшую описанный выше характер, но и то, что исчислениям, рассматриваемым в связи со шогими интересными классами категорий, можно придать формулировку, допускающую применение хорошо известных методов теории доказательств, например, устранение сечения. Ряд дальнейшие результатов можно найти в статьях [з] , [12] - [16] и в книге [17] • В [17] описываются исчисления, отвечающие большинству представленных в литературе вариантов дополнительной структуры в категориях. (В основном эти исчисления оказались близки к различным фрагментам интуиционистского исчисления высказываний).

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

В данной диссертации рассматривается и решается ряд новых задач теории категорий (и некоторые ранее известные); при этом используются некоторые методы теории исчислений, которые раньше в этой связи не применялись. Среди новых задач теории категорий рассматривается* например, задача описания всех (а не только канонических) естественных преобразований всевозможных суперпозиций виделенных функторов над данной категорией. В тех случаях, когда удается решить ее (скажем, для категории конечнопорозденных проективных модулей над кашутативным кольцом 1 с I и суперпозиций &х и кот; ) теория исчислений помогает свести общий случай к сравнительно несложным алгебраическим теоремам. Из ранее не применявшихся в такш направлении методов теории исчислений отметим преобразования выводов, включающие (в отличие от процедуры устранения сечения) преобразование конечной секвенции (особую роль будут играть операции, обладающие некоторыми свойствами обратимости); анализ "зацеплений" вхождений переменных в секвенцию; метод оценок (придания истинных значений пропозициональным переменным).

Рассматриваются три класса категорий о дополнительной структурой. Это, прежде всего, класс так называемых симметрических моно-дцальных замкнутых (далее - СМЗ-) категорий, и два подкласса класса СМЗ-категорий (дополнительная структура категорий, принадлежащих этим подклаосам, получается в результате обогащения структуры ШЗ-категорий в двух различных направлениях: класс компактных замкнутых (далее - КЗ-) категорий, и класс декартово замкнутых (далее - ДЗ-) категорий. Охарактеризуем коротко эти классы (определения даются в

§ I).

Г?] ). Имеется выделенный объект, обозначаемый обычно через Т , который является (с точностью до естественного изоморфизма) "тензорной единицей". Выделенными являются также некоторые естественные изоморфизмы, обеспечивающие выполнение перечисленных условий на I, Л и о . Эти естественные изоморфизмы должны удовлетворять определенным соотношениям.

В КЗ-категориях треюуется, кроме того, чтобы для любых объектов X , Y объекты , а также и были естественно изоморфны (к выделенным в СМЗ-категориях естественным изоморфизмам добавляются соответствующие естественные изоморфизмы, на которые накладываются некоторые дополнительные соотношения).

В ДЗ-категориях вместо этого требуется, чтобы функтор Л был произведением в обычном категорнсм смысле олова, а объект 1 - правым нулем (терминальным объектом). К структуре ШЗ-категории добавляются соответствующие данные, на которые накладываются определенные соотношения (выражащие терминальность 1 и т.п.).

Типичным примеров ШЗ-категории может служить категория модулей над коммутативным кольцом 1 о I, с функторами и 1готг в качестве А и "з соответственно [30} (эта категория будет обозначаться далее через МОД-I); примером КЗ-категории - подкатегория конечнопоровденных проективных модулей категории МОД-I со структурой СМЗ-категории, индуцированной структурой MOft-I, и двумя дополнительными (стандартными для таких модулей) естественными изоморфизмами указанного выше вида [29] (эта категория будет обозначаться через ШОД-1). Функторы X и (vom. вместе со стандартная! естественными цреобразованиями определяют структуру ДЗ-категории на категории множеств и отображений (эта категория будет обозначаться через Se-i* ). ДЗ-категориями являются также топосы. В

§ 15 будет указан еще ряд примеров СМЗ-, КЗ- и ДЗ-категорий.

Исчисление, на котором вводится структура ДЗ-категории, цредс-тавляет собой (л, э; -фрагмент интуиционистского исчисления высказываний с константой "истина". Для СМЗ-категорий подобную роль играет исчисление, получаемое из этого фрагмента некоторым ослаблением структурных правил. Исчисление для КЗ-категорий не является логический в том смысле, что в нем выводимы не только тавтологии; оно, по-видимому, ранее не рассматривалось. Исчисление для КЗ-категорий содержит исчисление для СМЗ-категорий.

4. Опишем коротко структуру диссертации и распределение содержания по

главам.

Диссертация состоит из Введения и 4-х глав. Гл.1 носит вводный, в основном обзорный характер. В гл.2 рассматриваются некоторые операции над каноническими морфизмами и над естественными преобразованиями, связанные с операциями над выводами в соответствующих исчислениях. В гл.З рассматриваются связи между свойствами "зацеплений" вхождений переменных в секвенцию и ее выводимостью. В гл.4 при помощи теорем глав 2 и 3 изучаются свойства цроизвольных естественных преобразований суперпозиций функторов А и о в СМЗ-и КЗ-категориях

§§ 11-13) и канонических морфизмов в ДЗ-категори-ях

§ 14).

§ 15 гл.4 содержит примеры применений теорем, полученных в

§§ 11-14«

Отметим, каков характер связи этой работы с конструктивным направлением в математике.

Аппаратное ядро" работы, как по языку, так и по способам понимания и доказательства утверждений лежит в рамках конструктивного направления в математике. Здесь имеется в виду все, что касается языка исчислений, описаний выводов и методов оперирования с ними. Однако в результатах, относящихся к характеризации естественных цреобразований, речь обычно идет об объектах, определяемых и рассматриваемых в теоре тико-множе ственной математике, и упомянутая конструктивная часть работы применяется в таких ситуациях в соответствии с традициями классической математики, В то же время "аппаратное ядро" представляет собой самостоятельную часть работы о некоторыми строго конструктивными применениями.

В главах 2-

§§ 7, 8 главы 2,-

глава 3 и

§ 14 главы 4 полностью лежат в рамках конструктивного направления в математике. В

§§ 5,6 главы 2 конструктивными являются все те утверждения, в формулировках которых не упоминаются интерпретации в категориях естественных преобразований (над какой-либо категорией).

§§11-13 главы 4 по используемым понятиям и методам доказательств утверждений относятся к теоретико-множественной математике

§ 15 носит обзорный характер)

5. Перечислим основные результаты работы и некоторые их следствия. Получено описание всех естественных преобразований (в этом принципиальное отличие от [29] , где рассматриваются только канонические естественные преобразования) произвольных суперпозиций функторов Лиз над произвольной КЗ-категорией К » при условии, что объект X является образуицим в К . А именно, кавдое естественное преобразование может быть получено из некоторых канонических естественных цреобразований и некоторого эндоморфизма объекта 1 при помощи функтора Л и композиции (теорема 12.1; эта теорема имеет место, в частности, в категории ЕМОД-1).

Из полученного описания следует критерий коммутативности произвольной диаграммы естественных цреобразований суперпозиций функторов Л и "Э над К : диаграмма коммутативна, если и только если она коммутативна, когда все аргументы суперпозиций, входящих в диаграмму, равны Г (теорема 12.2). Из него следует также коммутативность всех диаграмм канонических естественных преобразований над К (теорема 12.3).

О помощью этого описания получается также (при выполнении некоторых, сравнительно "широких", дополнительных условий) необходимое и достаточное условие продолжаемости ненулевого естественного преобразования над КЗ-категорией К до естественного преобразования над объемлющей ШЗ-категорией , "структурно согласованной" с категорией К . Это условие состоит в существовании канонического естественного преобразования (тех же функторов) над Ь , или, что эквивалентно, в выводимости некоторой секвенции (теорема 13,3). (Отметим, что в работе широко иопользуетоя понятие обобщенного естественного преобразования [24] (ср. [25] , р.214), и что теоремы, перечисленные выше, в действительности формулируются и доказываются для обобщенных естественных преобразований).

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

§ 2). Эта теорема была одновременно и независимо доказана автором и А. Бабаевым существенно различными методами (см. введение к [20] ).

Некоторые теоремы, доказанные в работе, являются "внутренними" теоремами теории логических исчислений, например, теорема 8.2, в которой говорится, по существу, о сохранении эквивалентности выводов в исчислении высказываний при понижении "глубины" секвенции; теорема 10.1, в которой устанавливается связь выводимости секвенции со структурой ее графа зацеплений; теорема когерентности для канонических морфизмов в ДЗ-категориях, которая может рассматриваться как теорема о существовании не более чем одного нормального вывода секвенции, содержащей не более двух вхоэдений каждой переменной в (л -фрагменте интуиционистского исчисления высказываний (ср. [13] ). в. Несколько слов о нумерации и обозначениях. В диссертации используется сквозная нумерация параграфов. Номер теоремы, леммы и т.п. состоит из номера параграфа и порядкового номера ее в этом параграфе, причем теоремы, леммы и т.п. нумеруются независимо. Параграфы разбиты на пункты, и при ссылке на тот или иной пункт указывается сначала номер параграфа, а затем номер пункта в этом параграфе.

Символ с] будет обозначать конец доказательства. Символ будет использоваться как сокращение для "тогда и только тогда, когда .". Символ "¡7 будет использоваться для переноса формальных выражений со строки на строку. Символ = будет обозначать графическое равенство синтаксических выражений. Остальные обозначения вводятся по ходу дела.

- II

Глава I. ОБЗОР НЕОБХОДИМЫХ ОБЩЕНИЙ ИЗ ТЕОРИИ КАТЕГОРИЙ и теории исчис.

Терминология теории категорий, иопользуемая в диссертации, в основном согласована с [25] t [26] ; терминология теории исчислений - о [27] , [28]

Коснемся одного формального момента, связанного с определением категории. Мы, следуя С.Маклейну [25], будем считать, что всякая категория гЧ включает, помимо класса объектов 0UK) и класса морфизмов Mnt {<) 9 также функции oiom. и cocí , ставящие в соответствие каждому морфизму F его область определения и область значений;" функцию 1 , ставящую в соответствие каждому объекту У единичный морфизм , и частичную функцию • , задащую композицию морфизмов. В тех случаях, когда требуется явно указать область определения и область значений, морфизмами будут называться также тройки вида , где RMfficKí^tWtF^-ccoUF) ср. [26] ).

§ I. Некоторые типы категорий о дополнительной структурой

I. Симметрической моновдальной замкнутей категорией (СМЗ-кате-горией) называется всякий упорядоченный набор вида А; Э, р} , У , Jí jJt'1) где 14 - категория,

ГвОкК) ,л:К*К-К

- бифгнкторн, OUK)xOUK)xOb(K)-* Могс Ю, ^: 0U K)->Mtn( К), ж'3цесь обозначает категорию множеств и отображений.

-l rrr естественные изоморфизмы ( сГ , jf - обратные к <1 , ß

Ju естественные изоморфизмы; из дальнейшего будет следовать, что у - обратный к самому себе) с компонентами вида: т:(ХлУ)л2 — Хл(Ул1)

Ь'.ХАГ -X и-ХлУ-УлХ -TüxV2. : когл (ХлУД ) ivowi (X, Y=> Ъ ) здесь X .У Л eOtik) ) 'и коммутативны оледущие диаграммы

XAVmZMH CXaV)A(IAU) ■Ь-ХлШЫЛ) да 4iu (.ХдСУл2))дЦ-*-*ХлШ)лЫ)

СХлУм! ^XA(VAI) ХлУХулу v д* да Ч л дл .п. луЗдесь и далее аргументы естественных преобразований, включенных в дополнительны!} структуру К » а также некоторых естественных -преобразований,явным образом определяемых через эти естественные преобразования, пшцутся в виде нижних индексов. В некоторых случаях (когда недостающие индексы легко восстанавливаются, исходя из требования осмысленности рассматриваемых выражений) все или часть индексов не будут указываться явно (например, ос ( "(ХАу ) следует -читать как ХХУ£ХаУ)( ; , поскольку с- (ХлУДлУ), см. также диаграммы Д1 - Д4).

УлХ)лг

Это - так называемые условия когерентности Келли-Маклейна ( [18] , ср. также [17] гл.З и 8).

2. Выпишем явно условия, которым подчиняются все данные, входящие в состав СМЗ-категории (они пригодятся вскоре при описании отношения эквивалентности для соответствующего исчисления) Выписываемые ниже условия не будут независимыми; мы стремимся выписать все варианты, которые могут в дальнейшем понадобиться.

А1. Для любого морфизма Р'Х^У, Р-^ • Р- Р

А2. Для любых морфизмов р : ~Ъ Ц , & : У^ Ъ, Н: Х-» У

Р-&)'Н = Г(Сг-И)

Эти два условия выражают свойство единицы и ассоциативность композиции в К • в связи с ассоциативностью мы часто будем записывать кратные композиции без скобок. Следующие четыре условия выражают функторность I? и л

АЗ. Для любых морфизмов Р^: Х^ХЬ £:Х^Х

А4. = -|хэу

А5. Для любых морфизмов Р,: Х^Х,, Д.'У^ Сг

А6. ^л/

Для любых ХуУуЯ 6- ОЬ(К)

А7. о^хуг ' ^ У'УН ~ ^лдсулг) ' ' = ^(хлу)лг > аз ^-р* = хац

Для любых морфизмов F: ХаУ ¿ Q : X

А9. зихуг(Л"х'уг (Q)) = Q , UXY3f С F;) = р.

Следующие тождества выражают коммутативность Д1 - Д4.

АЮ. ^XYtZüUí'^rXAVÍZtí = ^ ' ¿VIVA*} U.'( d*Y¿ Л ^ )

AH. (\ж л ) • ¿луг = px-v ;

AI2. • У// - ^хлу (это условие можно записать как /•у=/1 , т.е. ^ = у1 , здесь • обозначает композицию естественных преобразований, a i - тождественное естественное преобразование функтора л );

AI3. о£угх

Следующие условия выражают естественность oi) еС\ ^ Для любых морфизмов F: X ~*Х ; &: У У/ Н ' Л ~~> '

AI4. (Fa(GaH))'¿xy2 = e¿xV/?,-Л Рл&^дН J ; Ais. F- рх - ¡v • Г Fa iT); б Fa ^ ) *р"х = • F¡

AI6. (FaG)Yxv ^У*

GaF).

Следующие условия выражают естественность jü и Jü~' (в них НX Л Y Z , СЛ X^Y'^ - произвольные морфизмы, F, G, Н - те же, что и выше).

AI7. 3lXYÍ, ( Н • И • ( FA & )) = (& = Н )• (Jl„Vz Í Н')> Г. Используя функтор K^ovuu , это соотношение можно записать как AI7'. )«лих/у/г *

Ais. H-cx-^Í&VíFAG-).

Аналогично, с использованием Uovuu AI8 переписывается как

AI8'. • клил, ( F, & => Н ) ^Uuí FAG-,H)'XXV¿

Символ ^=7 здесь и ниже читается "введем в качестве обозначения".

Пусть ^ отброшенные нижние индексыцри 01 и Л4 легко восстановить). Отображения <í:X,Yi-*íiy hê^Y^êxy суть единица и коеди-ница сопряжения Jû (в терминологии [25] ). Следующие тождества следуют из А9 и AI7, AI8.

AI9. ( i 3 ¿хг )'<W)X = i

А20. ЁусУлЮ'^^^у ) И XAV •

Следующие два условия выражают естественность <Г по первому и £ по второму аргументу (в обычном смысле). Они следуют из AI7, AI8. Для любых морфизмов RX-X , G:Y-r :

A2I. Ну ^FaÍOKv = ¿>y-F ; A22. fixV'ff^GMxH G'fxy • Естественности <Г по второму и £ по первому аргументам (в обычном смысле слова) не будет, однако имеет место естественность в обобщенном смысле из [24] , а именно, выполняются ( F ,G- те же, что и в A2I,: А22) : А23. Ну -3 (ix aG))-¿xy "(fi^W)'^ i A24. Sx/y • ( 1X/3Y aF) = fCF

Понятие обобщенного естественного преобразования описывается подробнее в

§ 4.

Отметим, что Л и Л4 выражаются через £ и <Г , а именно, для любых

JûyzC F)-Hx^F).cTxv v = ev¡l-(GлЬ)

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

3. Компактной замкнутой категорией (КЗ-категорией) будет называться всякий упорядоченный набор вида где К - ШЗ-категория, £ : естественные изоморфизмы о компонентами вида

Потребуем, чтобы при этом также выполнялись следующие условия. Пусть ©xv Тогда справедливы:

А25. 6xy 'i>xy ~ ^хэу 9 £xv "бху = '

А26, = ? = ^х •

В том, чтобы выписывать условия, выражающие естественность £ и ^ нет необходимости. Из AI-A24 следует естественность отобра

• Теперь А25 и А26 влекут то, что $ и ^ - естественные изоморфизмы.

Компактные замкнутые категории рассматриваются в [29] . Там приводится несколько отличное по форме определение. Наши условия кажутся более слабыми (тривиально доказывается, что всякая КЗ-категория в смысле [29] является КЗ-категорией в нашем смысле), но в действительности эквивалентны условиям из [29]

4. Наконец, декартовой замкнутой категорией (ДЗ-категорией) называется всякий упорядоченный набор вида

К;0,< >) гдеК- ШЗ-категория, < >: 0U ЮЛЮ *(%(!<)-* Möt( Sek ) естественный изоморфизм и

- естественное преобразование с компонентами соответственно вида

Чтобы записать условия, которым должны подчиняться эти данные, введем обозначения!: ^ху ми О,) 'Ум •

А27. 0Х = р для любого р: X I (те^минальность I ; это условие влечет также естественность 0 ).

Для любых морфиамов Г: X ~*У, С.'Х-* 2 , Н:Уд Ъ т. е^Ш-Р ; А29. <е.н,а.н> = н в этих условиях отброшены очевидные нижние индексы). Как показывают А28 и А29, д (на объектах) и < > (на морфизмах) определяют произведение в категории К , причем отображения У1-» йху и а служат его естественными проекциями (естественность следует из определения I и ч, ). Этих условий уже достаточно, чтобы рассматриваемая структура была структурой ДЗ-катего-рии ( [30] , р.551): из них следует естественность ( > и то, что это изоморфизм, а также согласованность со структурой СМЗ-катего-рии. Под согласованностью здесь понимается выполнение тождеств:

АЗО. «с ^Ч^МУ^гУ^^А^^^хт У

А31. Длялюбых -1М) здесь и в следующих условиях отброшенные нижние индексы легко восстанавливаются) . 0гшетим еще следующие условия, являющиеся следствием условий на Л , от-' , г , <Г и А27-А29. Для любых морфиз

НОВ Р.-ХдУ-г :

А32. £У2 Р)-еху А*у> - Г ;

АЗЗ. =

5. Некоторые общие замечания» а) Каждая КЗ- или ДЗ-категория содержит в качестве поднабора некоторую СМЗ-категорию. Допуская некоторую вольность речи, мы будем говорить, что каэдая КЗ- или ДЗ-категория является одновременно СМЗ-категорией (можно считать, что применяется обычный "забывающий" функтор). б) Пусть символ 2 обозначает любое из выражений: СМЗ,КЗ,ДЗ. Существенную роль в дальнейшем играет понятие Гектора.

Пусть К и К' - некоторые £ -категории. Функтор Т^К-^К' назы-ваетоя ¿функтор™, ео® дай любы, XX, Ъ < ОКЮ ШЫ,

Т(ХлУ)=ТО0л'Т(У) ,Т(Х=У)-ТГХ)='Т(У) (и аналогично для морфизмов), п Коотмтт ж аналогично для р ^ а также для £ и ^ (если ¿Е есть КЗ) либо для 0 (если И есть ДЗ), далее, если для любого морфизма

СП (К;

Т(ЗГХУг( Г)) = ^тсхтуота/^^ • аналогично для (и для ^ > в том случае, когда £ есть ДЗ). Штрихами здеоь помечены данные к'. • в) Пусть

К жК-Екатегории. К называется ¿'-подкатегорией \С , если (без учета дополнительной структуры) К , и функтор включения является Z-функтором. г) Любая СМЗ-категория К содержит СМЗ-подкатегорию , структура которой допускает расширение до структуры КЗ-категории. (В качестве К0 можно взять подкатегорию, содержащую в точности те объекты К » для которых бХу и из п. 1.3 являются изо-иор&гашш [29] ). д) Важную роль будут играть 2, -категории, в которых выделенный объект является образупцим, т.е. для любых морфизмов

Т-'Х+У и &: X У имеем, если для всех морфизмов И : I имеет место РН = С'Н » то |--£г

§ 2. Естественные исчисления для некоторых типов категорий с дополнительной структурой

Естественность исчислений донимается здесь в том смысле, что их структура "буквально" копирует структуру соответствуадих категорий«

Естественные исчисления дня СМЗ-, КЗ- и ДЗ-категорий будут обозначаться через ЕИСМЗ> , , соответственно. СимволЕ будет обозначать любое из выражений СМЗ, КЗ, ДЗ.

I. Формулы еие строятся обычным образом при помощи двуместных связок А и з и скобок из переменных . и константы

I . (точнее, переменные и Г суть формулы, если А и В суть формулы, то (А А В) и (А^В) - формулы; внешние скобки на практике обычно не пишутся). Символы , Ь , с , Л , е (с ивдекса-ми или без) будут использоваться для обозначаения произвольных переменных; А ,В .С .й . Е (с индексами или без) для обозначения произвольных формул.

Выводимые объекты Ж Е будут называться £-каноническими морфизмами или, коротко, 2-морфизмами. Допуская некоторую избыточность (см. замечание 2.2 ниже), мы определим ¿чуюрфизш как тройки вида £: А -> В где А и В - некоторые фориуяы и где £ - некоторый терм, построенный цри помощи А , з , • (символа композиции) и скобок из символа 1 и символов естественный преобразований, входящих в структуру Е-категории, снабженных некоторыми формулами в качестве нижних, индексов. Типом морфизма А В будет называться секвенция А В . Символы £, ^ (с индексами или без) будут использоваться далее для обозначения термов, входящих в состав

2 -морфизмы определяются индуктивно при помощи следующих схем аксиом и правил вывода.

Рассмотрим следующие три группы схем аксиом.

1) 1.11Д:А-*А ; 1.

1.3 <Ф Ал(ВЛС) -^(ЛлВмС; 1.4 ■■ ЛлГ ->• А ; 1.5 р;':А-»Аа1 ; 1.6 №■ АлВ^ВлА ;

2) 2.

§ав:(А2.2 ^д:(А=>М-А;

3) 0Д:А—I

Схемами аксиом Ейсмз являются схемы группы (I), схемами Ей« схемы групп (I) и (2), а схемами ЕИДЗ - схемы групп (I) и (3). Следующие пять правил являются правилами всех трех исчислений: А -> В а:В . /:АлВ->С

15 -*а ' 2) ^ф.-А-в-С '

• ,, /•• А^В 9: С-В

5) д:С-»В

Правило I) называется также правилом композиции или сечения. В Ейдз имеется также следующее правило:

2. ЗАМЕЧАНИЕ 2.1. Непосредственно из определения видно, что исчисления ЕИ къ иЕИдз являются расширениями исчисления Шсиъ т.е. все СМЗ-морфизмы являются также КЗ- и ДЗ-морфизмами.

ЗАМЕЧАНИЕ 2.2. Включая тип в задание 2 -морфизма, мы следуем [ 17] (объекты, соответствующие 2 -морфизмам, называются там Ь^МиЬ ъиушлтЛь ). В таком задании имеется определенная избыточность (оправдываемая выигрышем в наглядности). Если морфизм, то по / однозначно восстанавливаются (при помощи рекурсии) вывод этого /] -морфизма (таким образом, £ является кодом вывода) и его тип - секвенция . Это очевидно для аксиом, а далее легко доказывается индукцией по процессу порождения морфизма

§• АВ . Поскольку тип восстанавливается по ^ также будет называться орфизмом , а развернутая запись -¿•А-В будет применяться только там, где есть необходимость, Кроне того, иногда будет говориться, что I есть ^-иорфгаи типа

Будем говорить, что секвенция А В выводима в , если существует /-, аморфизм т типа

ЗАМЕЧАНИЕ 2.3. Если истолковывать 2.«. э • • • как пропозициональные пероиенные, Г - как константу "истина", А и "э -как конъюнкцию и импликацию, то выводимость секвенции вида в ЕИдз равносильна ее выводимости в интуиционистском исчислении высказываний; исчислению ЕИСЮ отвечает в этом смысле некоторое более слабое исчисление (см.

§ 3). Что касается Ейкз , то оно вообще не является логическим в том смысле, что не'все выводимые в нем секвенции являются тавтологиями (например, не является тавтологиями А ^В 9 Л (А =1 ) и (А^Г)3! -»А • ). Это, однако, не мещает теоретико-категорным приложениям ЕИ , так как для теории категорий основной интерес представляют КЗ-морфизмы.

Во многих случаях нет необходимости указывать явно все нижние индексы в 2~морфизмах, поскольку недостающие индексы легко /восстанавливаются, исходя из требования, чтобы все рассматриваемые выражения были И-морфизмами.

Введем по аналогии с обозначениями в случае 2-категорий, обозначения (это может также рассматриваться как иллюстрация к вышесказанному): ^ Рл<'1*&04) аб ^ (V НалОв) в Здесь были отброшены очевидные нижние индексы при ЛГ и Л"1 «

3; Определим отношение эквивалентности = на 2 -морфизмах (если

§ = ^ для некоторых И-морфизмов | и } , то мы будем говорить также, что £ и ^ ¿^-эквивалентны).

Отношение = будет, грубо говоря, наименьшей конгруэнцией, цревращаадей в Х-категорию. Точнее, = определяется индуктивно при помощи описываемых ниже аксиом и правил.

Пусть А э 1-Аэ 33 получаются из А1-АЗЗ (см.

§ I) заменой = на =| , символов X , У , 2 , Ц на А , В , С , Й , символов $ & »Н -на £ , £ , ^ , при этом "морфизмы" следует всюду заменить на " Е -морфизмы". Аксиомы для . А э 0 . f 1 £

А э X - А э 24 . Этими аксиомами исчерпываются аксиомы для =н

Аксиомами Ц являются также А э 25 и Аэ 26.

Аксиомами = - также А э 27 - А э 33 (вместо А э 25 ж Аэ 26).

Правила для

0.1 * * 3 а 1 ^ 0.

З1 ^ к.

Эти правила (вместе с А э 0) обеспечивают, что = - отношение эквивалентности. Следуицие правила I) - 6) выражают "устойчивость" = относительно правил вывода с соответствующими номерами.

Предполагается, что X-морфизмы в рассматриваемых правилах таковы, что выражения, стоящие слева и справа от = в заключениях этих правил, являются 2 ^орфизмаш. Не указываемые явно нижние индексы X , Х-1 и > определяются типами соответствующих Гчлорф^ов.

П /.1 8< • 2Ч :

ТГГТ^ТТТГ з) jLZ.ii—— ; 4) £19»

5) ^ Л 1$«.

Этими правилами исчерпываются правила для ^ и

§ . Для =? добавляется правило

6) /тЕ^

Заметим, что если } ^ у , то типа / и совпадают. Это непосредственно проверяется для авсиом, и далее доказывается стандартной индукцией по обоснованию щ

Пусть [/обозначает класс эквивалентности / по | Предыдущее свойство позволяет писать такая запись будет применяться при необходимости явно указать тип).

4. После того как определено отношение = , на множестве формул и ^-морфизмов вводится структура X -категории. (В дальнейшем выражение ЕИе будет обозначать не только исчисление, но и эту -категорию). А именно* - это множество формул; если г\ и о - формулы, то Ьож

А, В)

- это множество классов эквивалентности Е/Зг: А"^ В ; единица для объекта А - это ^а^-'А^А ; функции с1ош. и сос1 определяются тривиальным образом; 1 - выделенный объект; композиция на £ -морфизмах задается правилом сечения (правилом (I) Ейс ); функторы => и Д на объектах ( Е -морфизмах) определяются условиями: А^В

А (А, В) ^ А л В , . Корректность^ переноса этих операций на классы' эквивалентности обуславливается непосредственно определением ("устойчивостью" относительно применения соответствующих правил).

Естественные преобразования (кроме ЛГ^ОГ"1/ ) задаются схемами аксиом, точнее, например, ¿:А,В,С сЗ^- и т.д. Естественные преобразования СГГ , ОТ"1 , ( > задаются на мах соответствующими правилами ЕИ г . Как и в случае функторов, определение = обуславливает корректность переноса этого определения с представителей ( Л. -морфизмов) на классы эквивалентности. Процесс построения исчисления со структурой 2-категории, описанный в пл. 1-4, может рассматриваться как частный случай общей схемы, которая впервые, по-видимому, была проведена И.Ламбеком ( [10] , {II] ), а в настоящее время стала стандартной (так, она систематически применяется в книге [17] , ср. также [3] , [13] , а для КЗ-категорий - [29] ). Категория Ей^ является свободной ¿ -категорией, порожденной дискретной категорией (а.1,. ,. ^ ( [И] .'[17] ¿'[29] ).

5. Интерпретацией будет называться всякий ¿-функтор -> К » гДе ^ ~ I-категория. Так как ЕИЕ имеет структуру свободной 2 -категории, то интерпретация 3 : ЕИг -> К полностью определяется своими значениями на переменных а,,. а.^,. , и обратно, всякое отображение (гц,.,^,. ] -»ОКЮ может быть единственным образом продолжено до интерпретации (это очевидно и непосредственно).

Отметим, что отображение ¿ьЬс1к определяет интерпретации ЕЙсмз в Шкз и ЕИДЗ,

6. Важную роль будет играть операция подстановки формул вместо переменных. Пусть А^ >., А^ - произвольные формулы, ап., а^ - произвольные попарно различные переменные. Выражение ^д^" будет называться подстановкой (формул А .,>., А^ вместо переменных ). Пусть Л - некоторое синтаксическое выражение. Тогда выражение СЛ!^ ' ^ ) будет обозначать результат одновременной подстановки А1 вместо всех вхождений в вместо всех вхождений в Л (внешние скобки часто будут опускаться) . Иногда удобно допускать случай /г = 0 (в этом случае никакая подстановка в действительности не делается).

Выражение вида будет обозначать список ^ всли , и пустой список, если и.- О (это обозначение будет использоваться и тогда, когда ^ 13. - ^ Л^ не являются синтаксическими объектами).

Перечислим некоторые свойства подстановок. I Л|-гЯ I

Если уд -подстановки, переменные

ЬГА, попарно различны, то 1 д^' - подстановка.

Пусть Л >Л>1 * . ? А*, - некоторые синтаксические выражения, и Я ^ Л1Лг . Л^ . Тогда для любой подстановки К • где А[ Вчаотности, если ец , не входят в Д) , то Л} (

Пусть а 1,., а и , Ц ,.Ьуч. - попарно различные переменные, А„.,АЛ~ произво.пьные формулы (очевидно, в этом случае ,и ^ь,'!^ - подстановки). Пусть Л - произвольное синтаксическое выражение, Ь^. , не входят в Л . Тогда

Пусть Л - некоторое синтаксическое выражение, и подстановки, причем переменные отличны от переменных и не входят в формулы А^- уДь* пусть В'ь н~п')

Легко видеть, что выводы в ЕИГ переходят при подстановке в выводы ЕИе . Любая подстановка ¿д,/^ определяет интерпретацию ЕИ^ -> ЕИг , если положить ПСя^-) =. Д^ (1 & £ $ и,) и И С а.) = сь для остальных переменных (формулы и 2] -морфизмы переходят при этой интерпретации в результат подстановки в них формул А*.,. » А и, вместо переменных л,,). В частности, имеет место

ЛЕММА 2.1. (а) Если £ - ^-морфизм типа А , то

-морфизм типа ; (б) дня любых ¿.-морфизмов

Будем называть переименованием переменных в синтаксическом выражении Л применение к нему всякой подстановки вида , где Ь 1 , •••, У г* ~ попарно различные переменные, отличные от всех переменных, входящих в Л (кроме, может быть, ).

СЛЕДСТВИЕ 2.1 % Если -морфизмы и д' получаются из 2 -морфизмов / и ^ в результате некоторого переименования переменных, то ^ ^ <'"==^>/

7. -морфизм ^ : Д —> В будет называться 2 -изоморфизмом, если существует 2 -морфизм ^ : В ~А в ЕИ^. такой, что ¿р-д. = 4в и • Если существует 2 -изоморфизмто формулы А и В будут называться ¿'-изоморфными. Выражение будет обозначать, что форму-А Е -изоморфна о . Распространим отношение на секвенции вида (т.е. на типы ¿-морфизмов), положив А —^ В ^ А В тогда и только тогда, когда А и В ^ В . Очевидно, что - отношение эквивалентности, содержится в ^ и

Если К - Е-категория, то ¿-каноническими морфизмами (или просто I -морфизмами) в К будут называться образы 2-морфизмов при всевозможных интерпретациях 3 : ЕИГ -> К -морфизмы называются равными (в экстенсиональном смысле), если равны вое их интерпретации в любой Л -категории • Оказывается, что отношение экстенсионального равенства I] -морфизмов совпадает с отношением ^ . Имеет место следующая лемма (ор. [3] , лемма 2.1): ЛЕММА 2.2. Пусть £ , - цроизвольные Е -морфизмы. Тогда / <=т> для любой Е «категории К и любой интерпретации Т-Шг К имеет место равенство ) в К

ДОКАЗАТЕЛЬСТВО. Достаточно заметить, что ^ т ^ влечет для любой интерпретации л , и в то же время само отношение ^ определяет равенство морфизмов в

Лемма 2.2 показывает, что коммутативность некоторой диаграммы X -морфизмов равносильна коммутативности всех диаграмм, получающихся из нее при всевозможных интерпретациях.

3. Назовем вхождение подформулы в формулу А положительным (отрицательным) , если для четного (нечетного) числа вхождений в А различных подформул вида В ^ С оно происходит от некоторого вхождения в В . (Положительные вховдения называют иногда ковариантны-ми, а отрицательные - контравариантными - ср. [18] ). Если число таких подформул равно нулю, то вхоздение называется существенно положительным. Заметим, что если формула А1 входит в формулу А г а формула А^ входит в формулу А3 • то знак вхождения А1 в А3 , происходящего от рассматриваемого вховдения Ат в А2 через рассматриваемое вхождение Аг в , может быть определен по знакам этих последних с помощью "правила произведения".

Здесь и далее символ О будет обозначать конец доказательства.

Вхождению формулы в секвенцию вида А припишем тот же знак, что и соответствующему вхоадению в формулу А ^В • Вхоаде-ния одной и той же формулы в формулу или секвенцию, имеющие противоположные знаки, будут иногда называться соцряженными.

ПРИМЕР 2,1. В следущей секвенции указаны знаки вхождений переменных, подчеркнуты существенно положительные вхождения формул в секвенцию : (С ее ^ 15 с) л с

Будем использовать символ УЬ (о индексами или без) для обозначения вхоаденжй произвольных синтаксических выражений, а символы ю , 1Г ,1хг (о индексами или без) - для обозначения вховдений переменных исчислений Ей £ . Если - вхождение, то VI будет обозначать выражение, вхождением которого оно является (и аналогично для вхождений переменных).

Пусть 1Л/ - некоторое вхоадение формулы или секвенции Л в синтаксическое выражение <3 (не обязательно линейное - например, в древовидный вывод). Для любого вхождения какой-либо формулы в 3 цроисходящего от вхоадения в Л через ^Ь , определяется его знак относительно VI , как знак соответствующего вхоадения в Л

Пусть Л - произвольное синтаксическое выражение. Тогда ]/СЛ) будет обозначать множество вхождений переменных исчисления ЕИ^ в Л . Если Л - формула или секвенция (т.е. оцределены знаки вхождений), то

ГШ У(Ю ж УТЛ) будут обозначать соответственно множества положительных, отрицательных и существенно положительных вхождений переменных в Л . Если при этом УЬ - вхоадение Л в некоторое объемлющее выражение, то V (ВД, У (VI) и V (VI) будут обозначать соответственно множества положительных, отрицательных и существенно положительных относительно /Щ<> вхождений в объемлющее выражение. В том случае, когда Л - линейное выражение, и упомянутые множества задаются посредством списков (например,

-^иг} или \/(Л)= [и^ъ } ) будет предполагаться, что порядок вхождений в списках совпадает с их порядком в А

Назовем секвенцию А В квазиуравновешенной, если каждая переменная входит в нее не более двух раз, уравновешенной, если каждая переменная, которая входит в нее, входит ровно двазды, и притом о противоположными знаками» I- уравновешенной , если она уравновешена и в любой ее подформуле С ° В , где 0 - постоянная (не содержащая вхождений переменных) формула, \у также постоянна.

Сформулируем (в терминологии, введенной выше) некоторые известные результаты о когерентности. а) Случай СМЗ-категорий.

ТЕОРЕМА 2.1. Если и А-*В - СМЗ-морфнзмы, и секвенция А В 1-уравновешенна, то ^^^

Эта теорема впервые доказана в [18] (теорема 2.4) и обычно называется теоремой когерентности Келли-Маклейна.

Центральными изоморфизмами называются СМЗ-изоморфизмы, которые строятся из \ , об , р , у , сГ' , при помощи композиции и

А . Пусть С, Т) - формулы, построенные из переменных а*, -, 4ц. и константы X при помощи А и скобок, в каждую из которых (кь) входит ровно один раз. С помощью теоремы 2.1 легко доказывается следующая теорема (впервые она была доказана раньше теоремы 2.1).

ТЕОРЕМА 2.2. Существует единственный с точностью до г центральный изоморфизм . (С&1. [I] , теорема 5.1, [18] теорема 3.4).

Если секвенция А В не является 1-уравновешенной, то

9 ' ' о могут существовать неэквивалентные СМЗ-морфизмы типа |5 , однако их конечное число (см. [17] , 8.6.7 и 8.6.14). б) Случай ДЗ-категорий.

З^цесь наличие схемы аксиом 0Л: А^Х и правила вывода заметно усложняет ситуацию. Для некоторых секвенций А -> I? существует бесконечно много попарно неэквивалентных ДЗ-морфизмов типа например, для секвенции Са^а-Ма—> - см. [17]

9.6.7).

Г.Е.Минцем в [13]| был доказан аналог теоремы 2.2 для ДЗ-морфизмов, построенных из \} л,.0 цри помощи только А > и композиции (без помощи , ОТ и Л"1 ).

Автором (й независимо, А.Вабаевым) доказана теорема когерентности, утвервдаицая, что любые два ДЗ-морфизма £ , ^ типа АВ , где А^В - квазиуравновешенная секвенция, ДЗ-эквива-лентны» (В [20] мы называли такие секвенции уравновешенными). Ее доказательство, принадлежащее автору, приводится ниже (см. теорему 14 Л). с) В случае КЗ-категорий наш интерес будет в основном сосредоточен на описании произвольных естественных преобразований. Относительно когерентности для КЗ-канонических морфизмов см. [ 29]

§ 3. Вспомогательные исчисления генценовского типа

Исчисления, рассмотренные в предыдущем параграфе, не лишены, с точки зрения теории исчислений, некоторых существенных недостатков (не устранимо сечение, выводы громоздки). йце Ламбек [ю] ввел вспомогательные исчисления генценовского типа и воспользовался устранимостью сечения в этих исчислениях для получения теорем о канонических морфизиах. В этом параграфе будут рассмотрены исчисления играющие роль, аналогичную исчислениям, рассмотренных Ламбеком, по отношению к!СН1 и ЕИЛз . Что касается Ей^ , то в построении вспомогательного генценовского исчисления в этой случае не будет необходимости, поскольку наличие аксиом £дв 'А^ВВлГА^ ) и , не являющихся тавтологиями, позволит ограничиться рассмотрением очень простых секвенций и обойтись без устранения сечения при получении интересующих нас теорем.

Генценовскив исчисления, связанные с ЕИсиз> (с Ейдъ ) будут обозначаться через ГИСМЗ (соответственно, через ). СимволЕ на протяжении этого параграфа будет обозначать СМЗ или ДЗ.

I. Формулы в ГИ^ те же, что и в ЕИ^ • Выводимыми объектами Тй^ будут секвенции вида Г-^ А , где А - формула, Г -список формул; для обозначения списков формул будут использоваться греческие буквы Г , Д , П . . • (с индексами или без). В секвенции Г-^А список Г называется антецедентом, А - сукцеден-том; вхождения формул в качестве членов списка Г - антецедентными членами. Говоря о ГИСМЗ и Гйдз , мы часто будем называть А конъюнкцией, аз- импликацией. Буквой р (с индексами или без) будут обозначаться выводы в ГЙ^- . Запись будет обозначать, вывод р I секвенции Г А

Перечислим аксиомы и правила вывода исчисления

Аксиомы.

I) А-*А ; (2) —X

Правила вывода:

Г-А ; . В,г-Сл

Г,Л-А*В А лВ,Г-СА£ Щ^Г1'' Г-А В,А-С " г.

Г-А-В А=В,Г,Д-С ' сокращение); сечение). или будут, как обычно, называться логическими, а остальные правила - структурными. Рядом о формулировками правил помещены их обозначения (для структурных правил - также их названия), которые будут играть вспомогательную роль.

Описанное только что исчисление несущественно отличается от (Л, ^) -фрашента интуиционистского исчисления высказываний с константой "истина".

Исчисление ГИСМЪ отличается от ГИдз, по трем пунктам: в нем нет цравила 1-* ; правила А е-* заменяются на правило

А ; правило Ь заменяется на правило ^ -> (так называемую ограниченную форму утончения [3] ). Здесь А -> и 9 - следующие адг—с . д-1 г->е~ правила: / ' -к-*- ; —--'-- ч ->

Фрагменты исчислений Гй ^ , в которых не применяется сечение, будут обозначаться через ГИ~

2. Напомним некоторые термины из теории логического вывода ( [27] [32] ). Под "вхождением" мы сейчас будем понимать явно указанное в формулировках правил вхождение. Пусть ^ - применение одного из правил, рассмотренных выше. Если ^ - применение сечения, то вхождения А в посылки называются формулами сечения. Если ^ -применение П , то вхождения А и В в посылку и в заключение называются формулами перестановки. Для остальных правил, вхождения те(гтэтнвние); хг^г^

ШЩп* (перестановка); Г-А А.А-С

Г,ВАМ Г,А-С

Правила, применениями которых вводятся вхождения А

Д , В в посылку (посылки) называются боковыми формулами, вхождение , где о обозначает А или (если оно имеется), либо вхождение А в заключение называется главной формулой. Вховдения формул в Г\ Д называются параметрическими.

3. Отметим, что правила л и У являются производными правилами ГЙДз . Они моделируются следующими последовательностями переходов:

А,В,ГЧЛ , г-с

1Щ Л.Г-1-(ое,внив)

АаВЛВГЧ АлВ,Г-*С

В ряде случаев удобно рассматривать всякий Гисмз -вывод одновременно как ГИдз -вывод; в этом случае мы будем предполагать, что каждое применение л ^ или У представлено соответствущей фигурой. В ГИ Дз удобно пользоваться также следующим; производным правилом:

Оно моделируется фигурой, состоящей из утончения и применения для которого главная формула У служит боковой формулой. Присоединим это правило к основным правилам ГЙД5 .В случае необходимости мы будем считать, что оно служит просто удобным сокращением для соответствующей фигуры вывода. В будет считаться единственной боковой формулой -»• . Определения из п.^ распространяются на автоматически.

4. По каядому ), -морфизму /: А В может быть построен вывод р секвенции Д-*В в ГИ^ . Для этого в выводе (единственном) Е-морфизма АВ каждая аксиома заменяется

ГИ„ -выводом, каждое применение правила вывода - некоторой фигу-£ рой вывода в Гй£ . Например, акоиома д в о А в-В А-^А |Д удв:пАР"^иАп заменяется на вывод ^ д £>дД „ ААВ-ВАА применение цравипа вида -11112— заменаетоя на фштру

А1-В д

-,----* Л

А,А-*ВАС С ^

А-ВдС

В дальнейшем используется в основном факт существования такого перевода, поэтому ограничимся этими примерами. (Подробности см. в [17] ).

Пусть Г - произвольный список формул. Если Г-А^и." » то а(Г) будет обозначать формулу (.(А.,л.)л А^ . Если же Г пуст, то Л (Г) будет обозначать X . (Аналогичные обозначения будут применяться для ¿-морфизмов .Если

Опишем перевод , при котором ГИ^. -выводы переходят в морфизмы, цричем Гй Е «выводы секвенции Г А переходят в X -морфизмы типа

Л(Г)-*]\ и для любого Е-мррфизма А( П А найдется вывод р секвенции Г —» Д , т.ч. -О^с^) iе £ ( Заметим, что любая формула может быть представлена в виде А С Г; для некоторого списка Р ). Наличие делает ГИ£ эффективным средством для изучения 2 -морфизмов. В описании мы в основном следуем [17] , используя некоторые уточнения из '¡13] , [15] . Для любой секвенции положим На выводах исчисления ГИЕ перевод ^с^- будет определен рекурсией по цроцессу построения ГИ^ -вывода.

При определении существенную роль сыграют центральные изоморфизмы (см. п*2.10). Пусть Г^ > Г^ - некоторые списки форяул, Г| Гь. - некоторые их перестановки. Если Г*, состоят из попарно различных переменных, то по теореме 2.2 существует единственный о точностью до центральный изоморфизм типа • Если П Пе. состоят из произвольных формул, то существует единственный о точностью до = центральный изоморфизм, получающийся из центрального изоморфизма описанного выше вида в результате очевидной подстановки формул вместо переменных. Зафиксируем для любых списков ;П, Г*. и их перестановок Г^ ,. , Г^ некоторый такой центральный изоморфизм типа

Л(Л(К),.,Л(ГГ* ) и обратный к нему. В приводимых ниже определивших равенствах для через обозначаются эти фиксированные центральные изоморфизмы (их типы легко определяются по типам остальных X -морфизмов).

В п.п. (1)-(7) й обозначает , где Е ^ СМЗ, ДЗ. Скобки в записи композиции не указываются (можно считать, что они группируются влево).

1) ^(А-А)ИД:А-А; м • £ • Фср, > А \т )■//.• Г, А ) С. ; es) Г^А В,А* С А=В,Г,А-»С

QWc-^-d П'-МА^Г.АМ; в) - Од Ч&р)* НмШ-- AÍ Гн С ;

7, Öf СМД^ ), Q f : ЛСГ, В, А# А) - С í

1Г,В,А,Д-С/

- рг)'(Рлсг/)Глп)1 )-íQo»íPiíaVj)•£:л(А,Гьс ; ю) ÖAS)^„ф^лО^с л(ИГ)-С ; Ш) ^Д' (щ^ bO^tf. л V,)* Xf АлВ, Г ЬС з

13, Яз =

Отметим, что если перевод отличается от только выбором изоморфизмов то для любого ГИ^ -вывода р (р) =

Ср) .В этом смысле перевод определен однозначно(с точностью до = ) . Отметим, что мевду ^сиь и ^аз есть согласованность, в том смысле что, можно показать, для любого ГИСМЪ -вывода р и ГИЛЗ -вывода р/ , получающегося, если заменить в р каждое применение У и на соответствующую фигуру вывода в ГИДЗ см. п.3.3) , ^дз ( Ш Яе (■ Р

ЗАМЕЧАНИЕ 3.1. Чтобы упростить описание конкретных выводов в исчислении ГИХ , расширим его всевозможными производными правилами^ каждое из которых можно получить при' помощи фигуры, состоящей из одного применения некоторого правила ГИ ^ (за исключением правила перестановки), которому предшествуют и за которым следуют некоторые применения правила перестановки. Зафиксируем для каждого из этих производных правил некоторую "представлявшую" его фигуру. Распространим перевод на выводы в расширенном исчислении. Если р - произвольный вывод в расширенном исчислении, то заменим все применения производных пра вил указанного вида на представляющие их фигуры и затем применим . Как показывают п. (7) определения перевода и теорема 2.2, при другом выборе фигур, представляющих рассматриваемые производные правила (они могут отличаться лишь применениями перестановок), результатом применения будет Е-морфизм, отличающийся от полученного первоначально только заменой некоторых центральных изоморфизмов на эквивалентные, и, следовательно, эквивалентный ему. В этом смысле распространение на выводы в расширенном исчислении определено однозначно с точностью до = независимо от вида фигур, "цредставляпцих" эти правила. В тех случаях, когда не будет поводов для недоразумений, эти производные правила будут обозначаться так же, как используемые в представляющих их фигурах правила, отличные от П-> . Такие правила часто будут использоваться при построении конкретных выводов (ср. примеры 3.2 и 3.3 ниже).

6. Используя перевод можно перенести на секвенции исчислений ГИ^ понятие знака вхождения. Будем считать, что знак вхождения в секвенцию вида Г —* А совпадает со знаком соответствующего вхождения в секвенцию вида л(Г) А » в (А ) . Автоматически переносятся и все связанные с этим понятия (см. п. 2.9).

Перевод иццуцирует на выводах исчисления ГИ^ отношение эквивалентности, которое мы, как и в случае исчисления Ей^ будем обозначать через = (и говорить, если р 1 р; , что выводы р ир' £ -эквивалентны).

Имеется следующая важная теорема:

ТЕОРЕМА 3.1. Для каждого ¿-морфизма Л( ГД найдется вывод р секвенции Г А в исчислении ГИ^ , такой, что

17] » теоремы 8.5.2 и 9.5.1).

Во многих случаях будет достаточно такой более слабой теоремы:

ТЕОРЕМА 3.2. Секвенция Л(Г)~* А выводима в исчислении ЕИ^ тогда и только тогда, когда секвенция Г А выводима в исчислении ГИ г . (По теореме 3.1 выводимость секвенции Г А в ГИ ^ следует из существования ¿-морфизма Л(Г) ^ А (т.е. ее выводимости в Ей^ ). Обратное следует из того, что по определению перевода ^^ , для любого вывода Р А в исчислении ГИ Я (р)- А(Г) А 2 - морфизм).

7. Прежде чем рассмотреть устранение сечения в ГИ^ , приведем некоторые цримеры.

ПРИМЕР 3.1. (ГиЕ —вывод и соответствущий ему Е-морфизм.)

Рассмотрим следующий ГИг -вывод р :

Имеем цри некотором выборе центральных изоморфизмов Гр) ^

Следующие примеры иллюстрируют использование Ги? -выводов для задания Ц -адзмов.

ПРИМЕР 3.2. Сомрьк. Ч йсмз Ср) , где р - следующий вывод

I) |> с а си к Ь^С ->£

CL , Сй.э Ь),(Ьэс ) ->с

-—--, о- =>Ь j bz>c. -> а. =>с

-д —>

Пусть а.,Ь,а -различные переменные. Тогда по теореме когерентности Келли-Маклейна (теорема 2.1) СМЗ-морфизм 7" (аос ) единствен (с точноотью до == ). в дальнейшем через будет обозначаться СМЗ-морфизм (Сож|)аЬс) •

Привлекая теорему когерентности, цри помощи ГИ ^ -выводов можно определять также обладающие различными свойствами обратимости (например, Хдодваш).

ПРИМЕР 3.3, Пусть р^ , pz - следующие выводы в ГИСн2(л$ Ь, с - различные сс-ъ-а. \> Ь а / Ь а. л Ь

--— "

--л —> ^(Ь^с) (алЬ)^с

Рассмотрим ШЗ-морсоизмы По теореме 2.

Поскольку подстановка определяет интерпретацию ЕИсмг в Ейсцз , имеем (для любых формул АД С ) ((Qí,2Ср^с

Шг ((^смэ «3 С^о ь и аналогично для другой композиции. Следовательно, -О^Р^а'в.с и Й:мз ^ являются взаимно-обратными СМЗ-изоморфизмами. В дальнейшем они будут обозначаться соответственно через /4д с/\аВ; = с

8. В Шсмз и ГИдт, в оледупцем смысле устранимо сечение: ТЕОРБМА. 3.3. Для любого вывода \> в ГИСЮ (в ГИДЗ ) найдется вывод р' в этом исчислении, с той же конечной секвенцией, не содержащий применений оечения и такой, что ¡> (что р'ц /> ). Для Гиснз это теорема 8.6.1, а для - теорема 9.6.

17] . Теорема 3.3 для ГИСМЗ вытекает также из теоремы об устранимости сечения более ранней работы [23] (ср. [3] ), а для Шдъ из теоремы 6.7 работы [13] и теоремы 6.5 [34] . (В [13] рассматривается исчисление натурального типа, а в [34] - перевод генценовс-ких выводов в натуральные). Теорема 3.3 показывает, что если выводы в ГИ ^ изучаются с точностью до = , то можно ограничиться рассмотрением исчисления ГИ~ . Выводы в ГИ^ обладают тем свойством, что всякая формула, появляющаяся в выводе, входит в конечную секвенцию (кроме, может быть, формулы I в ГИ~г ).

ЗАМЕЧАНИЕ 3.2. В силу теорем 3.1 и 3.3 всякое утверждение о когерентности (об эквивалентности между собой всех) ^орфизмов т.ч. а( Г ) —г* А равносильно утверждению об эквивалентности ' всех выводов секвенции А в ГИ~ ;

Введение диссертация по математике, на тему "Применения логических исчислений к изучению естественных преобразований в категориях"

I. Одаой из важных тем общей теории категорий является изучение естественных преобразований б категориях, снабженных дополнительной структурой, состоящей из выделенных объектов, выделенных функторов (чаще всего в этой роли фигурировали функторы типа тензорного произведения, внутреннего 1гопг -функтора, прямой суммы или прямого произведения) и выделенных естественных преобразований (типа естественного изоморфизма коммутативности тензорного произведения, естественного изоморфизма сопряженности тензорного произведения и внутреннего К^-функтора, или естественных проекций прямого произведения), при условии, что все эти данные подчиняются определенным соотношениям (скажем, ОС - \ где С обозначает естественный изоморфизм коммутативности тензорного произведения).

История воцроса восходит к началу 60-х годов (см. [I] ). Естественные преобразования в категориях с дополнительной структурой активно изучались с того времени С.Маклейном, С. Эйленбергом, И.Ламбе-ком и рядом других математиков (см., например, [2] [3] [5] [8] [18] [29] [30] ). 4Рассматривались в основном задачи, связанные с естественными преобразованиями, которые могут быть представлены некоторыми термами, построенными из символов выделенных естественных, преобразований при помощи символов выделенных функторов и символа композиции (тавив естественные преобразования мы будем называть, в духе работ С.Маклейна [2] [25] каноническими естественными преобразованиями; их точное определение для рассматриваемых в этой работе типов категорий дается ниже, в § 2), в частности задачи о корегентнооти канонических естественных цреобразований (верно ли, что все диаграммы в том иди ином классе диаграмм канонических естественных цреобразований комздутативны).

Полученные результаты находили применение в различных областях математики: ври построении бесконечнократннх пространств петель в алгебраической топологии (см. [2] [4] [5] ); при построении "длинных точных последовательностей" в гомологической алгебре [6]; при определении операций Стинрода в абелевых категориях [7] и т.д. Н.П.Титов нашел неожиданные применения результатов о когерентности к вопросам описания работы систем ЭВМ [8 ] •2. В ряде случаев для решения задач упомянутых типов с успехом применялась теория исчислений. Связующим звеном между теорией категорий и теорией исчислений служит тот факт, что с классом категорий, имеющих заданную дополнительную структуру, может быть связано (вообще говоря, многими способами) некоторое исчисление секвенциального типа, которое оказывается свободной категорией того же класса при следующем "распределении ролей": формулы играют роль объектов; роль морсоизмов из А в В отводится класоам эквивалентных друг другу выводов секвенции А-В (или их кодов) при некотором отношении эквивалентности =■ оцределяемом на основании соотношений, выполнение которых требуется в рассматриваемом классе категорий (в частности, класс эквивалентности аксиомы А^А играет роль единичного морфизма); роль композиции играет правило сечэния ——^—^ ; роль функторов играют пропозициональныеА Сусвязки (на объектах) и правила введения соответствующей связки(на морфизмах); роль естественных преобразований играют схемы аксиом или иногда (например, для изоморфизмов сопряженности) правила вывода.

Впервые, по-видимому, начал применять исчисления для изучения канонических естественных преобразований И.Ламбек (см. [9] - [И]), обнаруживший не только связь мевду исчислениями и категориями, имевшую описанный выше характер, но и то, что исчислениям, рассматриваемым в связи со шогими интересными классами категорий, можно придать формулировку, допускающую применение хорошо известных методов теории доказательств, например, устранение сечения. Ряд дальнейшие результатов можно найти в статьях [з] [12] - [16] и в книге [17] • В [17] описываются исчисления, отвечающие большинству представленных в литературе вариантов дополнительной структуры в категориях. (В основном эти исчисления оказались близки к различным фрагментам интуиционистского исчисления высказываний).

В СМЗ-категориях выделенными функторами являются коммутативное и ассоциативное с точностью до естественных изоморфизмов "тензорное произведение" и сопряженный к нему справа внутренний кот -функтор. Мы будем обозначать эти функторы через Лиз соответственно (существует значительное сходство мезвду свойствами этих функторов и свойствами конъюнкции и импликации в логике; ср. [II] [13] [Г?] ). Имеется выделенный объект, обозначаемый обычно через Т который является (с точностью до естественного изоморфизма) "тензорной единицей". Выделенными являются также некоторые естественныеизоморфизмы, обеспечивающие выполнение перечисленных условий на I, Л и о. Эти естественные изоморфизмы должны удовлетворять определенным соотношениям.

В КЗ-категориях треюуется, кроме того, чтобы для любых объектов X Y объекты а также и были естественно изоморфны (к выделенным в СМЗ-категориях естественным изоморфизмам добавляются соответствующие естественные изоморфизмы, на которые накладываются некоторые дополнительные соотношения).

4. Опишем коротко структуру диссертации и распределение содержания по главам.

Список источников диссертации и автореферата по математике, кандидата физико-математических наук, Соловьев, Сергей Владимирович, Ленинград

1. Mac Lane S. Natural associativity and commutativity. - Bice Univ.Studies, 1963, v.49, ТВ 4, p.28-46.

2. Mac bane S. Topology and logic as a source of algebra. Bull. Amer.Math.Soc., 1976, v.82, Ж 1, p.1-40.

3. Минц.Г.Е. Замкнутые категории и теория доказательств,- Зап. научн.семин.ЛОМИ, 1977, т.68, с.83-114.

4. Ддамс Д&. Бесконечнократные цространства петель. М.: "Мир", 1982, 198 с.

5. May J.P. Е^ -spaces, group completions, and permutative categories. "New developments in topology", bond.Math.Soc.Lect. Uotes, N 11, Cambr.Univ.Press, 1974, p.61-93.

6. Villamayor O.E., Zelinsky D. Brauer groups and cohomology for general commutative rings extensions. J.Pure and Appl.Algebra, 1977, v.11.

7. Epstein D.B.A. Punctors between tensored categories, Invent. Math., 1966, v.1, p.221-228.

8. Титов Н.П. Когерентность естественных изоморфизмов в категориях алгебр и модулей.- Авторефер.дисеерт. на соискание учен.ст. канд. физ.-матем.наук, М., 1981, 16 о.

9. Mann C. !Che connection between equivalence of proofs and cartesian closed categories. Proc.Lond.Math.Soc., 1975, v.31, N 3, p.289-310.

10. Минц Г.Е. Теория категорий и теория доказательств,- В кн.:Актуальные цроблемы логики и методологии науки. Киев, 1979, с.252-278.

11. Бабаев A.A. Равенство морфизмов и теорема когерентности для бизамкнутых категорий.- Зап.научн.семин.ЛОМИ, 1981, т.105, с.3-10.

12. Бабаев A.A. Равенство морфизмов в замкнутых категориях.- Изв. АН Азерб.ССР, сер. физ.-тех. и мат.наук, 1981, № I, с.3-10.

13. Бабаев A.A. Равенство морфизмов в замкнутых категориях.- Изв. АН Азерб.ССР, сер. физ.-тех. и мат.наук, 1981, № 2, с.3-9.

14. Szabo М.Е. Algebra of proofs. Studies in Log.and the Fondations of Math., North-Holland P.C., 1978, v.88, 297 p.

15. Kelly. G.M., Mac Lane S. Coherence in closed categories. « J.Pure and Appl.Algebra, 1971» v.1, p.97-140.

16. Соловьев C.B. Новые приложения теории доказательств к теории категорий.- 6 Всесогозн. конферен. по матем. логике. Тезисы, Тбилиси, 1982, с.173.

17. Бабаев A.A., Соловьев C.B. Теорема когерентности для канонических морфизмов в декартово замкнутых категориях.- Зап.научн. семин.ЛОМИ, 1979, т.88, с.3-29.

18. Соловьев C.B. Сохранение эквивалентности выводов цри редукции глубины формул.- Зап.научн.семин.ЛОМИ, 1979, т.88, с.197-208.

19. Соловьев C.B. 0 естественных преобразованиях в компактных замкнутых категориях.- 17 Всесоюзн. алгебр, конферен. Тезисы сообщений, 4.2. Минск, 1983, с.225.

20. Минц Г.Е. Теорема об устранимости сечения для релевантных логик.» Зап.научн.семин.ЛОМИ, 1972, т.32, с.90-98.

21. Eilenberg S., Kelly G.M. A generalisation of the Functorial Calculus, J.of Algebra, 1966, v.3, p.366-375.

22. Mac Lane S. Categories for the working mathematician*Berl.Springer, 1972, 262 p.

23. Фейс К. Алгебра: кольца, модули и категории. I. М.: "Мир", 1977, 688 с.

24. Клини С.К. Математическая логика. М.: "Мир", 1973, 480 с.

25. Карри Х.Б. Основания математической логики. М.: "Мир", 1969, 568 с.

26. Kelly G.M., Laplaza М. Coherence for compact closed categories. J.Pure and Appl.Alg., 1980, nv.19, p.193-213«

27. Eilenberg S., Kelly G.M. Closed cagegories. Proc.of the conf.on Categorical Algebra, La Jolla, 1965, p.421-562.

28. Szabo M.E. A counter-example to coheren e in cartesian closed categories, Canad.Mathem.Bull., 1975, v.18, p.111-114*

29. Kleene S.C. Permutability of inferences in Gentzen's calculi LKand LJ. Memoirs Amer.Math.Soc., 1952, N 10, p.1-26.

30. Соловьев С.В. Выводимость секвенции критерий существования естественного преобразования в категории модулей.- 16 Всесо-юзн. алгебр, конферен. Тезисы, ч.1, Л., 1981, с.150-151.

31. Pottinger G. Normalisation as a homomorphic image of cutelimination. Ann.of Math.bog., 1977, v.12, 323-357.

32. Шанин H.A., Давыдов Г.В., Маслов С.Ю., Минц Г.Е., Оревков В.П., Слисенко А.О. Алгорифм машинного поиска естественного логического вывода в исчислении высказываний.- М.-Л.: "Наука", 1965, 39 с.

33. Голота Я.Я. Сети меток и выводимость в интуиционистском исчислении высказываний.- Зап.научн.семин.ЛОМИ, 1969, т.16,с.28-43.

34. Голота Я.Я. Некоторые приемы, упрощающие построение сетей меток.- Зап.научн.семин.ЛОМИ, 1969, т.16, с.44-53.

35. Голота Я.Я. Матричный способ записи сетей меток.- Зап.научн. семин.ЛОМИ, 1974, т.40, с.4-9.

36. Харари Ф. Теория графов. М.: "Мир", 1973, 300 с.

37. Оревков В.П. Три способа выявления несущественных формул в секвенциях.- Зап.научн.семин.ЛОМИ, т.88, с. 163-176.