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

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

Существует естественный способ описания категорных тождеств, связанный с формулированием так называемого внутреннего (типового) языка мультикатегорий (см., например, [Lambek 1989, р. 224]). С этой целью вводится счетное множество переменных каждого типа и секвенции интерпретируются как (мультилинейные) операции.

Определим индуктивно термы всех типов:

• 1) каждая переменная есть терм своего типа,
• 2) если f. А| ... А„I- А„+ представляет собой секвенцию и а,- есть терм типа А,, для / = 1, ..., т, то /а, ... а_т есть терм

типаЛет+i.

Заметим, что вводятся переменные всех типов, но не переменные для типов.

Тождество (или скорее доказуемое тождество) термов одного и того же типа есть отношение конгруэнтности, удовлетворяющее обычной подстановке термов вместо свободных переменных. Таким образом, из <р(х) = <р'(х) можно вывести ф(а) = ф'(а), где а есть любой терм того же самого типа, что и переменная х. В принципе, однако, можно декларировать переменные и записывать это как ф(х) =_х (р'(х). Помимо обычных правил для равенства также

допускаются следующие правила для тождественной секвенции и сечения:

Здесь х есть переменная типа А, и = х ... х_т является последовательностью переменных типа Г - А ... А_т> v есть последовательность переменных тип Д и w есть последовательность переменных типа Л.

Описание внутреннего языка на этом практически заканчивается, Тождества между секвенциями теперь вполне определимы: про две секвенции fg: А ... А_т- - А_т+] говорят, что они тождественны, если fx 1 ... х_т = gx ... х_т доказуемо во внутреннем языке. Существенно, что x_mi все различны, даже если две А_{ могут совпадать. Отсюда можно легко вывести описанные ранее тождества в мультикатегориях. Например, для /: Дн A, g : ГЛДЬ В и /?: Г'#Д'Н С вычисляем:

Мы определяем экспоненциальную дедуктивную мультикатегорию, наделяя дедуктивную мультикатегорию А введенными правилами вывода и дополнительными тождествами: I-

В частности, (е_АВУ =_А=,в, 0Y)' = 1г-

С помощью введенных правил нетрудно получить следующее правило:

Для этого достаточно положить:

g{f)=g (?

(/ЛбС^йГ-экспоненциальную дедуктивную мультикатегорию получаем теперь путем добавления следующих тождеств:

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

где So есть переменная типа Т;

где л'о есть переменная типа Т;

где So есть переменная типа Т.