Главная Логика
КАТЕГОРНАЯ ЛОГИКА
|
|
||||||
Экспоненциальные дедуктивные мультикатегорииДедуктивная мультикатегория представляет собой дедуктивную систему, в которой следующие уравнения между доказательствами имеют место:
Существует естественный способ описания категорных тождеств, связанный с формулированием так называемого внутреннего (типового) языка мультикатегорий (см., например, [Lambek 1989, р. 224]). С этой целью вводится счетное множество переменных каждого типа и секвенции интерпретируются как (мультилинейные) операции. Определим индуктивно термы всех типов:
типаЛет+i. Заметим, что вводятся переменные всех типов, но не переменные для типов. Тождество (или скорее доказуемое тождество) термов одного и того же типа есть отношение конгруэнтности, удовлетворяющее обычной подстановке термов вместо свободных переменных. Таким образом, из <р(х) = <р'(х) можно вывести ф(а) = ф'(а), где а есть любой терм того же самого типа, что и переменная х. В принципе, однако, можно декларировать переменные и записывать это как ф(х) =х (р'(х). Помимо обычных правил для равенства также допускаются следующие правила для тождественной секвенции и сечения:
Здесь х есть переменная типа А, и = х ... хт является последовательностью переменных типа Г - А ... Ат> v есть последовательность переменных тип Д и w есть последовательность переменных типа Л. Описание внутреннего языка на этом практически заканчивается, Тождества между секвенциями теперь вполне определимы: про две секвенции fg: А ... Ат- - Ат+] говорят, что они тождественны, если fx 1 ... хт = gx ... хт доказуемо во внутреннем языке. Существенно, что xmi все различны, даже если две А{ могут совпадать. Отсюда можно легко вывести описанные ранее тождества в мультикатегориях. Например, для /: Дн A, g : ГЛДЬ В и /?: Г'#Д'Н С вычисляем:
Мы определяем экспоненциальную дедуктивную мультикатегорию, наделяя дедуктивную мультикатегорию А введенными правилами вывода и дополнительными тождествами: I-
В частности, (еАВУ =А=,в, 0Y)' = 1г- С помощью введенных правил нетрудно получить следующее правило:
Для этого достаточно положить: g{f)=g (? (/ЛбС^йГ-экспоненциальную дедуктивную мультикатегорию получаем теперь путем добавления следующих тождеств:
![]() Во внутреннем языке единственность секвенций может быть выражена также в виде правил вывода, отсюда тождества имплика- тивной дедуктивной мультикатегории могут быть переписаны следующим образом: ![]() где So есть переменная типа Т; ![]() где л'о есть переменная типа Т; ![]() ![]() где So есть переменная типа Т. |
<< | СОДЕРЖАНИЕ | ПОСМОТРЕТЬ ОРИГИНАЛ | >> |
---|