Подструктурные дедуктивные категории

Описываемые ниже дедуктивные категории называются подструктурными, так как они соответствуют таким минимальным фрагментам ассоциативного исчисления Ламбека, линейной, релевантной, ВСК и интуиционистской логик, которые достаточны, чтобы описать лежащие в их основании структурные правила (подробнее см. [Restall 2000]). Заметим, что в отличие от рассмотренных ранее систем AL, М, R, ВСК, тоже соответствующих упомянутым логикам, в рассматриваемых ниже подструктурных дедуктивных (системах) категориях нет операции импликации.

Под дедуктивной категорией с умножением, следуя [Petrie 2002], будем подразумевать дедуктивную категорию с формулой Т (= истина) и бинарной операцией • для образования произведений А »В из двух данных формул А и В. Кроме этого, мы вводим следующее правило вывода:

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

Дедуктивная категория с умножением является моноидалыюй дедуктивной категорией, если в ней существуют следующие специальные стрелки для всех объектов А,В и С:

и выполняются следующие уравнения:

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

для каждой пары (А,В) ее объектов, и если выполняются следующие уравнения:

Симметричная моноидальная дедуктивная категория является релевантной, если она имеет специальную стрелку

для каждого объекта А и выполняются следующие уравнения:

Симметричная моноидальная дедуктивная категория является аффинной, если она имеет специальную стрелку

Для каждого объекта и выполняются следующие уравнения:

Предложение 1. Если симметричная моноидальная дедуктивная категория является одновременно и релевантной и аффинной, и ее стрелки удовлетворяют следующим уравнениям: (okw)a^(k/4»b)w/,= Л,

(8kw) = л,

то она представляет собой декартову дедуктивную категорию.

Доказательство. Приведенную аксиоматизацию декартовой дедуктивной категории будем называть структурно- эквациональной, чтобы отличить ее от стандартной аксиоматизации, приведенной ранее. Чтобы показать, что эти две аксиоматизации экстенсионально эквивалентны, определим:

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

Наоборот, если мы начнем со стандартной аксиоматизации, то можем определить

Нетрудно видеть, что при этом выполнимы

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

а в стандартной аксиоматизации -

Некоторые из этих выводов очевидны, другие (например, касающиеся b-стрелок) требуют некоторых усилий, которые остаются на долю читателя. ?

 
Посмотреть оригинал
< Пред   СОДЕРЖАНИЕ   ОРИГИНАЛ     След >