Экспоненциальные дедуктивные поликатегории

Сформулируем вначале понятие полисеквенциальной дедуктивной системы, основываясь на [Szabo 1975] с учетом некоторых позднейших модификаций этого понятия Дж.Ламбеком. Полисеквенциальная дедуктивная система представляет собой полиграф, состоящий из класса стрелок и класса объектов, и двух отображений:

где {объекты}* представляет собой свободный моноид, порожденный классом объектов, его элементами являются последовательности Г = А … А_п объектов. Заметим, что п может быть равно нулю и в этом случае Г представляет собой пустую последовательность.

Чтобы получить минимальное полисеквенциальное дедуктивное исчисление, введем специальную стрелку.

и бинарную операцию на стрелках:

при условии, что Ф или Г — пустые последовательности и У или, А — пустые последовательности. Отсюда возникают четыре возможностьи:

Случай 1. Г и, А пусты, заключением является g#f: 0Ь ФЕЖ Случай 2. Г и 4^х пусты, заключением является g#f: 0ДН ФЕ. Случай 3. Ф и Ч? пусты, заключением является gUf: Г0ДНЕ. Случай 4. А и Ф пусты, заключением является g#f: Г0Ь ЕЧ*.

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

Чтобы получить полисеквенциальное дедуктивное исчисление в генценовском стиле, или просто генценовское полисеквенциальное дедуктивное исчисление, водятся следующие стандартные операции на стрелках:

Перестановка:

Импликативное полисеквенциалъное дедуктивное исчисление мы получаем при введении специальных стрелок.

и правил.

Импликативное полисеквенциальное дедуктивное исчисление, полученное подобным образом, представляет собой, по сути дела, некоторую версию импликативного фрагмента так называемой классической билинейной логики из [Abrusci 1991].

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

для всех / I’llГ2ЛГ3, g: Д|Н Д2ЯД3, /г: Ф|/)Ф₂.#Фз1- Ф4, и при условии, что, по крайней мере, одна из Г₂, Дг и одна из Гз, Дз пусты; g#(f#h)=/# (g # А),.

для всех /г: Г! I— Г₂^1 Г₃ВГ₄₎/ ААД₂1-Дз, g- Ф^ФгЬ Фз, и при условии, что, по крайней мере, одна из Ф|, Д] и одна из Ф₂, Д2 пусты.

Идея поликатегории была выдвинута Дж. Ламбеком еще в 1969 г., однако он не выписал все уравнения между доказательствами. Это было сделано М. Сабо в 1975 г., хотя последний допустил слишком много случаев сечения. Позднее поликатегории были исследованы И. Велиновым [Velinov 1988], а полное множество уравнений можно найти в [Cockett Seely 1992].

Экспоненциальная дедуктивная поликатегория представляет собой дедуктивную поликатегорию со стрелками е⁺, s', i и соответствующими операциями (правилами) импликативного экспоненциального дедуктивного исчисления, для которой справедливы следующие уравнения:

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