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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

• (1) (Tl— А) X (ВQ в S² тогда и только тогда, когда 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))ht (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, получаем правило.

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

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

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

и правил

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

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

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

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

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

(достаточно положить <�р"= е (со (<�р^ее").

(где ф^к= е (к<�ф").

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