третья. Многоуровневые дедуктивные системы и дедуктивные л-категории

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

Наряду с рассмотренным ранее внутренним (типовым) языком мультикатегорий существует еще одна возможность описания отношений между стрелками, связанная с конструкцией так называемой двухуровневой дедуктивной мультикатегории. В этом случае, отправляясь от стрелок дедуктивной системы Р, строится новый секвенциальный язык, в котором формализуется дедуктивная металогика Р2 системы Р, а тем самым и описываются отношения между стрелками, т.е. отношения между выводами (см. [Dosen 1992]).

Объектами секвенциальной двухуровневой дедуктивной системы Р2 будут последовательности стрелок системы Р, т.е. последовательности типа X =f Поскольку т может быть равно нулю, то в этом случае X будет представлять собой пустую последовательность 0. Стрелки (секвенции) будут представлять собой выражения видаX^tf где Xесть объект Р2, а/есть стрелка Р. Доказуемость секвенции Х-> / в соответствующей двухуровневой дедуктивной системе будет означать утверждение о том, что исходя из стрелки X, мы можем сконструировать стрелку/ используя примитивные стрелки и примитивные операции. Иными словами, существует производная операция, отображающая X в / Таким образом, система подобных секвенций будет представлять собой формализацию металогики производных правил исходной дедуктивной системы. Теорема такой двухуровневой системы соответствует производной операции без посылок, т.е. секвенции X —> f где X целиком и полностью сконструирована из 0. Стрелка 0 -> / будет называться элементом /

Чтобы получить минимальное двухуровневое дедуктивное исчисление, вводим специальные стрелки

где f°g есть композиция fug, и бинарную операцию на стрелках

Пусть теперь S есть импликативная дедуктивная система и S2 се импликативная двухуровневая дедуктивная система.

Предложение 1. Секвенция 0 —> / доказуема в двухуровневом дедуктивном исчислении S2 тогда и только тогда, когда / есть стрелка S.

Доказательство. Слева направо показываем по длине доказательства, что если X -у / доказуема в S2, то все стрелки из X будут стрелками S лишь тогда, когда / содержится в S. В противоположную сторону индукция проходит также без затруднений. ?

Рассмотрим теперь, как отражается S в металогике S2, т.е. когда мы можем записывать в S производные операции S2. Мы увидим, что S способна на это, если S2 замкнута относительно следующего правила:

т.е. когда правило дедукции допустимо для S .

Рассмотрим следующий перевод, т.е. биекцию / из Р2 в Р:

Пусть S есть импликативная дедуктивная IB-система. Докажем следующее предложение:

Предложение 2. X -> / доказуема в S2 тогда и только тогда, когда 1(Х —> f) есть стрелка в S.

Доказательство. Слева направо доказываем индукцией по длине доказательства X —>/ в S2. Если X = 0, то получаем 0->/ Но тогда l(0 —» /) = 7(0)1- 1(f) = Tl- t(f). Поскольку t(A- В) = A z> В, то Тн А г> В приводит к Ah В, т.е. к стрелке в S. Если X =fg, то тогда получаем доказуемую стрелку^ -> g°f Но l(fgg°f) = t(fg)I- t(g°f)

= Kg°f)h Kg0/)* т.е. все сводится к единичной стрелке типа = я. Справа налево по предложению 1 получаем 0 —> (t(X)h t(/)) как доказуемую стрелку в S2, а затем применяем стрелку (°) в виде (Ть t(X))(t(X)h /(/)) -> (TV К/)) и сечение, получая (Th- t(X)) -> (Tl- /(/)). Действуя аналогично, мы доходим до стрелок в последовательности Xи для каждой такой стрелки Ah В получаем (Ah- В) —? (ТН А з В). Используя обратную секвенцию для f получаем X ->/ ?

Предложение 3. S2 замкнуто относительно правила дедукции. Доказательство. Мы имеем:

  • (1) (Tl— А) X (В- Q в S2 тогда и только тогда, когда t(X°(Tн A))h t(Bh- С) в S
  • (2) тогда и только тогда, когда /(.Y^Tl- A))h В о С.

Но из В з С с помощью стрелки р в S и сечения получаем t(X°(Ть- Д))1- (A z> В) z) (A z> С), что можно записать как /(,Y°(Tt- A))h- t(A z> В t- A z> Q. Отсюда по предложению 2 получаем (Tl- A) X —» (A z> В I- Az>C). Поскольку Tl- А есть стрелка S, то по предложению 1 0 —> (Tl- А) и, применяя сечение, получаем X —> (A Z3 В h A zd С), что и требовалось доказать. ?

Заметим, что аналогично, применяя стрелку у, можно получить правило

применяя стрелку w, получаем правило

применяя стрелку к, получаем правило

Если добавить к S2 дополнительную метасвязку импликации =>, то мы получаем импликативное секвенциальное двухуровневое дедуктивное исчисление GP2 при введении специальных стрелок:

где f. АУ- В, g: В- C;f=>g:Br>A kBdC,

и правил

где 0 означает пустую стрелку, т.е. стрелку ь- .

Точно так же можно ввести, помимо этого, следующие стрелки:

Соответственно можно заменить эти стрелки на следующие правила:

(достаточно положить срр= е(е(Р((ре»»

(достаточно положить <ру = е(е(у(фЕ6»))

(достаточно положить <р“= е(со(<рее»)

(где фк= е(к<ф»).

В этом случае мы получаем удвоение логики в двухуровневой дедуктивной системе S2, что приводит к двухуровневой системе SC,B№* (см. о подобном удвоении [Dosen 1988а]). Нетрудно также, рассматривая соответствующие тождества на метастрелках, получить двухуровневые мультикатегории, отвечающие полученным двухуровневым системам.

 
Посмотреть оригинал
< Пред   СОДЕРЖАНИЕ   ОРИГИНАЛ     След >