Полная версия

Главная arrow Логика arrow КАТЕГОРНАЯ ЛОГИКА

  • Увеличить шрифт
  • Уменьшить шрифт


<<   СОДЕРЖАНИЕ ПОСМОТРЕТЬ ОРИГИНАЛ   >>

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

Сформулируем вначале понятие полисеквенциальной дедуктивной системы, основываясь на [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, /г: Ф|/)Ф2.#Фз1- Ф4, и при условии, что, по крайней мере, одна из Г2, Дг и одна из Гз, Дз пусты; g#(f#h )=/# (g # А),

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

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

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

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

 
<<   СОДЕРЖАНИЕ ПОСМОТРЕТЬ ОРИГИНАЛ   >>