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

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

Добавление этих правил к секвенциальным дедуктивным исчислениям порождает генценовские дедуктивные системы.

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

Генценовское импликативное дедуктивное исчисление GI получается при введении дополнительно специальных стрелок г._Лв'- A (A z> В)I- В. i_A: h А и правил.

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

и два правила для конъюнкции.

Под генценовской дедуктивной мультикатегорией [Lambek 1989] мы будем понимать дедуктивную мультикатегорию с дополнительными операциями /" «, f'^M» (введенными правилами перестановки, сокращения и ослабления), удовлетворяющим следующим уравнениям:

В частности, в мультикатегории из / ху, gxx' и hx, где х и х' имеют один и тот же тип, мы можем получить.

допуская, таким образом, перестановку аргументов, диагональное отображение и проекции.

Предложение 1. Внутренний язык генценовской дедуктивной мультикатегории выполняет условие неограниченной функциональной полноты:

для любого данного терма

_m), который не содержит никаких других переменных, отличных от х, типа A,(i = 1,2, …, т), существует единственная операция f: A … A_mh В, такая, что

Здесь вхождение х, не обязательно упорядочено, х, может входить несколько раз и вообще может явным образом не появляться (см. [Lambek 1989, р.232]).