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

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

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


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

Устранение сечения в подструктурных дедуктивных мультикатегориях

Для подструктурной дедуктивной мультикатегории G мы можем сконструировать свободную подструктурную дедуктивную мультикатегорию Fr(G), порожденную G. Объекты этой мультикатегории получаются индуктивно из объектов G с помощью операций ®, л, v, /, ±. Ее секвенции получаются из секвенций G путем присоединения базисных секвенций lA, и т.д., и формирования новых операций из старых с помощью правила сечения и правил (®), (-)р и т.д. Тождества между сравнимыми секвенциями в Fr(G) будут те и только те, которые следуют из тождеств в G, и мульти- категорные тождества

Помимо этого, добавляются еще и тождества и т. п., рассмотренные ранее.

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

Определение 1. Подструктурный мультифунктор F из подструктурной дедуктивной мультикатегории М в подструктурную дедуктитвную мультикатегорию М' представляет собой мультифунктор, сохраняющий структуру мультикатегорий, т.е. выполняются следующие условия:

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

Пусть U будет стирающим мультифунктором, тогда подструктурный мультифунктор G—>C/F(G) будет, как известно, полным и точным [Lambek 1993] (полнота свидетельствует о том, что мультифунктор не порождает никаких новых секвенций по сравнению со старыми, а точность свидетельствует об отсутствии новых тождеств между секвенциями).

Теорема устранения сечения принимает теперь следующий

вид:

Теорема 1 (устранение сечения). Если стрелки р, р, q, k, 1 заменить на правила (®), (-)р, (-),, (-)*, (-)/, то любая секвенция в UF(G), сконструированная с помощью правил сечения, будет эквивалентна секвенции, сконструированной без применения правила сечения.

Доказательство. Без потери общности допускаем, что стрелки /: ЛК Л и g: ГАЛЬ В уже были получены без применения правила сечения. Позднее покажем, что g(J) эквивалентна секвенции, в конструировании которой были вовлечены сечения меньшей "степени", причем степень сечения g{f) определяется как

где d(A) есть число вхождений всех связок в А и d(F) = d{A) + ... + + d(Am). Возможны следующие случаи:

  • 0. И/и g содержатся в G.
  • 1. На последнем шаге конструирования /вводится одна связка по левую сторону стрелки.
  • 2. На последнем шаге конструирования g вводится одна связка по левую сторону стрелки, но не в А.
  • 3. На последнем шаге конструирования g вводится одна связка по правую сторону стрелки.
  • 4. На последнем шаге конструирования и/и g вводится одна связка в А.

В случае 0 стрелка g(j) уже содержится в мультикатегории G, замкнутой относительно сечения. Рассмотрим теперь по очереди остальные случаи.

(1). Связка ®.

Случай 1. Пусть Л = Г'А'® В'А' и/=/'*. В этом случае мы имеем:

Заменим это выражение на:

где новое сечение имеет меньшую степень. Более того, имеет место g(f '*> = (ge, что можно показать во внутреннем языке. На место переменной типа А'®В' мы можем поставить ух'у', где х' и у' являются переменными типа А' и В’ соответственно. Нетрудно убедиться, что

проверяя, что обе стороны сводятся к gufu'x’y'v'v, используя определения () и ®.

Случай 2. Пусть Г = Г‘А'®В'А' и / = /'*. (Случай, когда Д= Г'А'®В'А' такой же, поэтому он будет опущен) Мы имеем:

Заменим это выражение на:

где новое сечение имеет меньшую степень. Более того,

поскольку обе стороны сводятся кf'u 'x'y'v'fwv.

Случай 3. В = А'®В' и g - fo®f: Г'Д'(- А'®В'. Допустим, что А содержится в Г'. (Случай, когда оно появляется в Д' аналогичен и будет опущен) Мы имеем:

Заменим это выражение на:

где новое сечение имеет меньшую степень. Более того,

поскольку обе стороны сводятся к ifauJwu2fv'ввиду определений

(®)и<).

Случай 4. В = А'®В' и g =fo®f nf=g'®. Мы имеем Заменим все это на:

где оба новых сечения имеют более низкую степень. Более того,

что можно рассматривать следующим образом. Левая часть выражения сводится к /'®Mp/o«/ivV ввиду определений (®) и (). Теперь мы используем тот факт, что / =/а это затем сводится к /

'ufau'fv'v, которое также представляет собой то, к чему сводится правая часть ввиду определения ( ).

(2). Связка л.

Случай 1. Пусть Л = Л|Л'лВ'Л2 и/=Мы имеем:

Заменим это выражение на:

где новое сечение имеет меньшую степень. Более того, если /'есть переменная типа А'л.В', то

так как обе стороны сводятся к guf'w>t V2v, используя определения

Ои/V

Случай 2. Пусть Г = Г^А'лВ'Гг и g = g'p. Мы имеем:

Заменим это выражение на:

)

где новое сечение имеет меньшую степень. Более того,

поскольку обе стороны сводятся к gt/ip/'Mj/wv так же как в случае 1. Случай 3. В = Л'лВ' и g = go*g- Мы имеем

Заменим это выражение на

где оба новых сечения имеют меньшую степень. Более того,

(и аналогично для q), так как левая сторона сводится к так же как и правая.

Случай 4. Пусть А = А'лВ',/ = /ол/i и g = gр. Мы имеем:

Заменим это выражение на

где новое сечение имеет меньшую степень. Более того,

(3). Связка V.

Случай 1. Л = PiAvB'A' и f=foyf- Мы имеем:

Заменим это выражение на:

где оба новых сечения имеют меньшую степень. Более того,

(то же самое имеет место, если мы заменим кх'на 1у), поскольку обе стороны сводятся к guf0u'xVV.

Случай 2. Пусть Г = f'A'vB'A' и пусть g = go^gi? Мы имеем:

где оба новых сечения имеют меньшую степень. Более того,

govg,« кг 'v W = go{f)vg{fi wkcVW

(то же самое имеет место, если мы заменим ' на кх ?), поскольку обе стороны сводятся к gou 'х V 'fwv.

Случай 3. В = A'vB' и g = g1*. Мы имеем

Заменим это выражение на

где новое сечение имеет меньшую степень. Более того,

поскольку обе стороны сводятся к kg 'иfwv.

Случай 4. А = A’vB',f=f и пусть g = g0vg|. Мы имеем

Заменим это выражение на:

где оба новых сечения имеют меньшую степень. Более того, govgi(/*)wwv = govgiHk/'wv = gouf'wv = g0(f')uwv.

(4). Нульместная связка I. Заметим, что Случай 3 невозможен. Случай 1. А = Г7Д' и/=/". Мы имеем:

Заменим это выражение на: где новое сечение имеет меньшую степень. Более того, и

сводятся к тому же самому выражению.

Случай 2. Г = Г7Д' и пусть g = g". Мы имеем:

Заменим это выражение на:

где новое сечение имеет меньшую степень. Более того,

Случай 3. А = J,f = i и пусть g = g". Мы имеем:

Очевидно, что g"(i) = g 'может быть построено без сечения.

(4). Нульместная связка _L. Возможны только два случая.

Случай 1. Мы имеем:

Заменяем все это построение на стрелку ?: ГГ’_1_Д'Д(- В, сконструированную без сечения, и отметим, что g(D) = ?.

Случай 2. Пусть Г = Г'±Д'. Мы имеем:

Заменяем все это на стрелку ?: Г'З-Д'ЛДь- С, сконструированную без сечения, и отметим, что ? = ?. ?

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