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

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

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


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

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

Расширим теперь, следуя [Lambek 1993], понятие дедуктивной мультикатегории за счет введения новых операций ®, л, v, /, ±. Первая из этих операций представляет собой категорный аналог «произведения» (конкатенации) в системах Айдукевича-Ламбека, л и v - это конъюнкция и дизъюнкция из декартовых дедуктивных категорий, / представляет собой константу, играющую ту же роль относительно ®, которую играет Т относительно а и v. И, наконец, J. также знакома нам по декартовым категориям. Отсутствие в логике аналогов ® и / обычно объясняется тем, что, в присутствии генценовских структурных правил, эти связки совпадают с л и Т. Введем следующие специальные стрелки:

и следующие правила:

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

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

(достаточно положить / 0g = ц.4в( _/)(g); очевидным образом iAB - a®U)

(достаточно положить fp =J{p) и gp = g(q); очевидным образом pAB = (Ь)/» Чан = (1 в)д

(достаточно положить fy = k{f) и gi = 1(g); очевидным образом кАВ = (Ь)*, he = (1 «)/)•

В частности, р®АВ = Ьад, Рлв л qлв = ArJ>, к^в v АВ = AwB, i' = 1/,

?1 = Ц.

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

где si есть переменная типа Л<8>В;

где $2 есть переменная типа А/В где ,s3 есть переменная типа Т; где есть переменная типа 1.

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