Полная версия

Главная arrow Логика arrow КАТЕГОРНАЯ ЛОГИКА

  • Увеличить шрифт
  • Уменьшить шрифт


<<   СОДЕРЖАНИЕ ПОСМОТРЕТЬ ОРИГИНАЛ   >>

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

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

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

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

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

типаЛет+i.

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

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

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

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

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

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

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

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

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

g{f)=g (?

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

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

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

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

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

 
<<   СОДЕРЖАНИЕ ПОСМОТРЕТЬ ОРИГИНАЛ   >>