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

Среди различных стилей представления логических систем, основывающихся на различии в форме вывода, можно выделить так называемые представления в стиле Шютте. В этом случае выводы имеют форму f V- А ... Ат, что означает, что/есть доказательство альтернатив А ... Ат без каких-либо гипотез. Дж. Ламбек [Lambek 1994, р. 153] предпочитает дуальное представление, основывающееся на использовании выводов /: Гн- , поскольку в этом случае мы можем рассматривать / как мультилинейный оператор Гь О (можно рассматривать О как тип истинностных значений и выводы А ... Ат- О как w-сортные отношения).

Формулировки в стиле Шютте наводят на мысль о логических системах, дуальных к интуиционистским системам в смысле дуального ограничения: если в первом случае требуется, чтобы сукце- дент секвенции состоял не более чем из одной формулы, то дуальное ограничение сводится к тому, что антецедент секвенции может состоять не более чем из одной формулы (см. [Czermak 1971]). Подобную систему с правилами введения и удаления, дуальную интуиционистской логике, строит, например, Н. Гудмен [Goodman 1981]. Ее переформулировка в виде исчисления секвенций, осуществленная В. А. Смирновым [Смирнов 1987, с. 223], выглядит следующим образом:

основные секвенции: А —> А и А -> Т; структурные правила: сечение, перестановка справа, добавление справа С —> А ;

С->АА

где А<=В означает коимпликацию (импликацию Брауэра), которой в алгебре соответствует псевдоразность.

Если вместо выводов в стиле Шютте/ I- А ... Ат,, означающих, что/есть доказательство альтернатив А ... Ат без каких-либо гипотез, рассматривать однопосылочные выводы f: В- А ... Ат (что можно тогда понимать как доказательство альтернатив А ... Ат исходя из гипотезы В), то можно сформулировать соответствующие косеквенциальные дедуктивные системы, в которых принимается дуальная концепция секвенции. Более того, можно сформулировать и дуальные импликативные дедуктивные системы и соответствующие им категории, рассматривая язык с дуальной связкой импликации.

Мы получаем коимпликативное исчисление, если мы допускаем, что существует формула _1_ (= ложь) и бинарная операция для образования коимпликации А <= В из двух данных формул А и В. Кроме этого, мы вводим следующие два правила вывода:

Нетрудно видеть, что наше коимпликативное исчисление будет соответствует некоторой простейшей коимпликативной системе 1°, ибо:

а) мы имеем аксиому 1° в виде:

б) правило модус поненс в виде:

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

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

Таким образом, для данного графа X мы можем сконструировать коимпликативные исчисления D°(X) и свободную коэкспонен- циальную категорию F(X)°, порожденную X.

Пусть GRPH будет категорией графов, чьими объектами являются графы и каждый морфизм F: X -> Y есть пара отображений F: Objects(X) —> —> Objects{Y) и F: Arrows(X) —> Arrows(Y), такая, что f.X->X’ влечет /=(/): F(X) -> F(Х').

Пусть ЕХР° будет категория коэкспоненциальных дедуктивных категорий, чьими объектами являются коэкспоненциальные дедуктивные категории, а стрелками функторы F: А -> В, сохраняющие коэкспоненциальную структуру, т.е.

Пусть U будет обычным стирающим функтором ЕХР° —> GRPH. С каждым графом X мы можем ассоциировать морфизм графов Нх: X —> UF(X) следующим образом: Нх(Х)= X и, если /: X —> У есть стрелка в X, то Нх(/) = f (классы эквивалентности / рассматриваются как доказательства в D°(X)). Мы имеем следующее универсальное свойство:

Предложение 1. Для любой коэкспоненциальной дедуктивной категории А и любого морфизма F: Х—> U(A) графов существует единственная стрелка F': F(X)°—>А в ЕХР°, такая, что U(F')Hx=F.

Доказательство. Конструкция F’ требует от нас выполнения следующих условий:

Требуется проверить, что F' определен правильно, т.е. что для всех fg.AV- В в F’ (X),f= g влечет F* (f) = : Р (g ). Последнее очевидно, поскольку никаких других, кроме требуемых нам, тождеств в F' (X) не выполняется. ?

Подобное универсальное свойство означает, что F есть функтор GRPH—>EXP°, лсвосопряженный к U с сопряжением Нх: Id —> UF (см. четвертую главу). Для коэкспоненциальных дедуктивных категорий можно определить также понятие подстановки доказательств, что определяется следующим предложением:

Предложение 2. Для данной коэкспоненциалъной дедуктивной категории А, индетерминанта х: А0f- А над А и стрелки а: А0- А, существует единственный функтор Sxa: А[х] —> А, такой, что Sx°(x) = auSxaHx= U

Доказательство Вначале докажем, что:

Для данной дедуктивной категории А, и индетерминанта х Ао- А над А, функтора F: А->В и любой стрелки b: F(A0)I- F(A) в В имеется единственный функтор F А[х] —> Б, такой, что F(x)= b и

fhx=f.

Каждое доказательство (р(лг) при допущении х может иметь следующую форму: к, х, х(х)Ф),

где к есть стрелка в А, т.е. постоянный полином. Решающим шагом является определение F '(ф(*))- Определим индуктивно:

Остается лишь показать, что Р определен на полиномах, а не на доказательствах, то есть, что <р(*) =х ф'(х) влечет F '(<р(х)) = F

'(Ф'М). Если в последнем случае писать ф(х) = ф'(х), то достаточно проверить, что = имеет все свойства подстановки и отвечает всем тождествам экспоненциальной категории. Например, чтобы проверить, что 1_ф(*)д * = Ф(*), мы вычисляем F'( hp(x)j s) = (F'(jp(x)j %

= (lf'(sht. д.

Теперь, чтобы получить доказательство нашего предложения, достаточно положить Р= 1д. ?

Наделяя коэкспоненциальные дедуктивные категории дополнительной структурой, мы одновременно получаем различные категорные коимпликативные исчисления, соответствующие логическим исчислениям. Так, если мы добавим к нашей системе аксиом новую аксиому, выглядящую следующим образом:

P°V (В <= А) <= (С <= А)- В <= С то мы получаем импликативное исчисление, соответствующее системе минимальной импликативной логики 1В°. Действительно, с помощью ранее введенных правил нетрудно вывести следующее правило:

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

Аксиому В° соответствующей логической системы мы теперь получаем в следующем виде:

Теорема дедукции в коимпликативной системе устанавливает, что

Теорема дедукции. С каждым доказательством ф(х): В~С из допущения х: AhL может быть ассоциирована стрелка типа (В <=С) <= Ah 1, не зависящая от х.

Слабая теорема дедукции. С каждым доказательством ф(х|BhC из допущений Xi: Ath±,..., хт: Amhl. может быть ассоциирована стрелка (... ((В <= С) <= А„)<= ...)<= AiH_L, зависящая от В и С, но не зависящая от Хь ...,хт.

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

Теорема I (обобщенная слабая теорема дедукции). В 1В°- импликативном исчислении с каждым доказательством (р(х/,...,хт): Bh С из допущений Xi'.A[h±y ... , хт: AmhA. может быть ассоциирована стрелка типа/(...((В<= С) с= С„)<= ...)<= С]Ы, не зависящая от Х|, ... т, где Ci есть либо одно из А, ... , Ат, либо 1В°- теорема.

Доказательство. Как и раньше, будем писать / = kxX€AVx2eA2.....*mf3mуХт), где индекс хеА указывает, чтох имеет

тип А. Заметим, что каждое доказательство ср(хь ... уХт): В- С из допущений jci... , хт: Ат-1. должно иметь одну из следующих форм:

Во всех случаях х(*ь ••• r*m) и V(*i> ••• r*m) являются более краткими доказательствами, чем ф(дг|,... rxm), и мы определяем индуктивно:

Нетрудно заметить, что случаи (iv) и (v) отличаются только выбором С„. Далее, поскольку речь идет об индукции по длине доказательства <р(х|,... ,хт), то формально можно было бы определить эту длину как 0 в случаях (i) и (И), как сумму длин х(*ь — Л») и v)/(jci, ... jm) плюс один в случае (iii) и как длину v|/(*i, ... jcm) плюс один в случаях (iv) - (vi). ?

Действуя дуальным образом, мы можем добавить к 1В°- импликативному исчислению аксиомы, являющиеся категорными аналогами дуальных аксиом С°, W°, К° :

Нетрудно видеть, что это ведет к добавлению следующих правил (стрелок):

(достаточно положитьf,= ( [_/j ABc)s)

(достаточно положить fw= (|_/j w0^),)

/ВСИ/>-коэкспоненциальную дедуктивную категорию мы получаем теперь путем добавления следующих тождеств:

Последнее уравнение утверждает, что X является инициальным объектом

Аналогично функциональной полноте для IBCWK- экспоненциальных категорий, мы получаем следующую теорему для IBCWK?-коэкспоненциальных дедуктивных категорий:

Теорема 2 (функциональная полнота). Для любого полинома <р(х): В ~ С по индетерминантам х: А К 1 над IBCWK0- коэкспоненциальной дедуктивной категорией мы можем получить единственную стрелку f. (В<= С)<= Лн_1_, такую, что ((/)., х), = <р(х).

Дуальная секвенциальная дедуктивная система представляет собой мультиграф, состоящий из класса стрелок (называемых также "секвенциями") и класса объектов (иногда называемых "типами") и двух отображений

Начало: {стрелки} —> {объекты}

Конец: {стрелки} —> {объекты}*

где {объекты}* представляет собой свободный моноид, порожденный классом объектов, его элементами являются последовательности Г = А ... А„ объектов. Заметим, что п может быть равно нулю и в этом случае Г представляет собой пустую последовательность. Стрелка f В- также называется элементом В.

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

и бинарную операцию на стрелках:

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

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

и правил

Как и в случае импликативного дедуктивного исчисления, легко видеть, что наше коимпликативное косеквенциальное дедуктивное исчисление GF соответствует некоторой системе 1°. Действительно, мы получаем:

а) аксиому 1° в виде:

б) правило модус поненс в виде:

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

В частности, (в*ва)ш = Ьсь (f°±)i = Ц.

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

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

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

то мы получаем косеквенциальное коимпликативное исчисление G1B°, соответствующее системе минимальной коимпликативной логики 1В°. Действительно, с помощью ранее введенных правил нетрудно вывести следующее правило:

Для

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

Аксиому В° получаем теперь в виде следующей стрелки:

Действуя подобным же образом, мы можем добавить к косек- венциальному коимпликативному исчислению G/B° аксиомы, являющиеся категорными аналогами дуальных аксиом С°, W°, К° :

Нетрудно видеть, что это ведет к добавлению следующих правил (стрелок):

(достаточно положить ft = s°[e0[y0[/ct]]])

(достаточно положить fw= s0[w°[/f:E]])

(где/< = е°[к°[/]]).

GIBCWK°-коэкспоненциальную дедуктивную комульти-

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

I

Для данного мультиграфа G мы можем сконструировать коим- пликативные исчисления D°(G) и свободную коэкспоненциальную дедуктивную комультикатегорию P(G), порожденную G. Объекты этой комультикатегории получаются индуктивно из объектов G с помощью операции <=. Ее косеквенции получаются из косеквенций G путем присоединения базисных косеквенций I,*, г°АВ, i°A т. д., и формирования новых операций из старых с помощью правил (-)?, (-

), и т.д. Наконец, тождества между сравнимыми косеквенциями в

F(G) будут те и только те, которые следуют из тождеств в G, и ко- мультикатегорные тождества

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

Введем теперь понятие комультифунктора, используя следующие определения:

Определение 1. Комультифунктор F из дедуктивной комульти- категории М в дедуктивную комультикатегорию М' представляет собой отображение класса объектов М в класс объектов М' вместе с отображением из класса стрелок М в класс стрелок М такие, что если f В— А ... А„ есть стрелка в М, то F(J): F(B)h- F(A,) ... F(A„) есть стрелка в /И'и F(A) = 1^,, F(g[/])= F(g) [F{f)).

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

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

Пусть G будет С/ВСИ^-мультикатегорией. Для коэкспонен- циального С/ВСИ/В°-мультифунктора F (т.е. сохраняющего ВСWK°-структуру G) имеет место следующая теорема:

Теорема 6. (устранение сечения). Если стрелки е, /, р, у, w, к заменить па правила (-),, (-)р, (-)», (-)и., (-)к, то любая косеквен-

ция в UF(G), сконструированная с помощью правил сечения, будет эквивалентна косеквенции, сконструированной без применения правила сечения.

Доказательство проводится дуально соответствующему доказательству для случая мультикатегорий.

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