Подструктурные дедуктивные категории
Доказательство. Приведенную аксиоматизацию декартовой дедуктивной категории будем называть структурноэквациональной, чтобы отличить ее от стандартной аксиоматизации, приведенной ранее. Чтобы показать, что эти две аксиоматизации экстенсионально эквивалентны, определим: Под дедуктивной категорией с умножением, следуя, будем подразумевать дедуктивную категорию с формулой Т (= истина) и бинарной… Читать ещё >
Подструктурные дедуктивные категории (реферат, курсовая, диплом, контрольная)
Описываемые ниже дедуктивные категории называются подструктурными, так как они соответствуют таким минимальным фрагментам ассоциативного исчисления Ламбека, линейной, релевантной, ВСК и интуиционистской логик, которые достаточны, чтобы описать лежащие в их основании структурные правила (подробнее см. [Restall 2000]). Заметим, что в отличие от рассмотренных ранее систем AL, М, R, ВСК, тоже соответствующих упомянутым логикам, в рассматриваемых ниже подструктурных дедуктивных (системах) категориях нет операции импликации.
Под дедуктивной категорией с умножением, следуя [Petrie 2002], будем подразумевать дедуктивную категорию с формулой Т (= истина) и бинарной операцией • для образования произведений А «В из двух данных формул А и В. Кроме этого, мы вводим следующее правило вывода: 
и добавляем к обычным категорным тождествам следующие дополнительные уравнения между доказательствами:
Дедуктивная категория с умножением является моноидалыюй дедуктивной категорией, если в ней существуют следующие специальные стрелки для всех объектов А, В и С:
и выполняются следующие уравнения:
моноидальная дедуктивная категория является симметричной моноидалыюй дедуктивной категорией, если она имеет специальную стрелку.
для каждой пары (А, В) ее объектов, и если выполняются следующие уравнения:
Симметричная моноидальная дедуктивная категория является релевантной, если она имеет специальную стрелку 
для каждого объекта А и выполняются следующие уравнения:
Симметричная моноидальная дедуктивная категория является аффинной, если она имеет специальную стрелку.
Для каждого объекта и выполняются следующие уравнения:
Предложение 1. Если симметричная моноидальная дедуктивная категория является одновременно и релевантной и аффинной, и ее стрелки удовлетворяют следующим уравнениям: (okw)a^(k/4«b)w/,= Л,.
(8kw) = л,
то она представляет собой декартову дедуктивную категорию.
Доказательство. Приведенную аксиоматизацию декартовой дедуктивной категории будем называть структурноэквациональной, чтобы отличить ее от стандартной аксиоматизации, приведенной ранее. Чтобы показать, что эти две аксиоматизации экстенсионально эквивалентны, определим:
для случая структурной аксиоматизации. Нетрудно показать, что это ведет к выполнению стандартных условий декартовой категории: 
Наоборот, если мы начнем со стандартной аксиоматизации, то можем определить.
Нетрудно видеть, что при этом выполнимы.
Теперь мы должны доказать, что «двойной перевод» (туда и обратно) приведет нас к тем же самым понятиям, т. е. показать, что в структурной аксиоматизации выполняются следующие уравнения:
а в стандартной аксиоматизации ;
Некоторые из этих выводов очевидны, другие (например, касающиеся b-стрелок) требуют некоторых усилий, которые остаются на долю читателя. ?