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

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

седьмая. Логические исчисления в топосах

Релевантная логика в топосах

Известно, что для любой малой категории С категория Set^свсегда будет топосом (см., например, [Гольдблатт 1983]). Именно это положение и служит отправным моментом при получении категорией семантики для интуиционистской логики путем трансформации алгебры Гейтинга в малую категорию. Главной особенностью при этом является то, что в качестве малой категории С служит алгебра Гейтинга, которая категорно представляет собой декартово замкнутую конечную кополную категорию предпорядка Н. Как мы уже знаем, нетрудно превратить подобную категорию в N- категорию, наделяя ее контравариантным функтором N: Н —» Н. Это обстоятельство наводит на мысль использовать рассмотренные нами N-категории с целью получения «топосной» семантики для других, отличных от интуиционистской, логических систем.

В качестве первого шага на этом пути, построим категорную семантику релевантной логики, основывающейся на конструкции категории Set*-функторов из ft/V-категории А в категорию множеств Set. С этой целью мы начнем со следующих определений и фактов.

Известно, что для ограниченной дистрибутивной решетки L дуальное (двойственное) пространство L, S(L) будет упорядоченным топологическим пространством, в котором множество точек S является семейством всех простых фильтров на L, упорядоченных по включению. Релевантное пространство является структурой = (S,R,*,t), где S есть наше семейство всех простых фильтров. R есть тернарное отношение на S,*- унарная функция на S, / с S. Для А,В

с S пусть А°В будет {z: 3xy(Rxyz & хеА & уеВ), и пусть А—>В будет {х: X/yz((Rxyz & уеА) влечет zeB}. Выполняются следующие условия:

1. Если A,BeL(S), то Л°В и А -* В являются клопенами;
2. (Rxyz & х'< х & у'< у & z'< z) влечет Rx'y'z'
3. Vxyz(-,Rxyz влечет 3A,BeL(S)(xeA &уеВ & zeA°B);
4. Функция х •— х* является непрерывным убывающим отображением на 5;
5. t принадлежит L{S) и удовлетворяет условию: Яуг(у< z эквивалентно Эх(хег & Rxyz)),

где L{S) есть двойственная к S решетка.

Двойственная к ^алгебра Я(‘%) определяется на решетке L(S)

путем добавления операций А°В, А-^В, -А = {z: z*eA} и определения константы 1 как /. Для релевантной алгебры L двойственное пространство L, R^L), определяется путем добавления к решетке всех простых фильтров ограниченной дистрибутивной решетки тернарного отношения х-у с z, определяя х* для xe как {а: —iagx}, и полагая / = {xeS(L): lex}. Справедливо следующее утверждение [Urquhart 1996, р.268]:

(1) Алгебра, двойственная к релевантному пространству, является релевантной алгеброй;

(2) Пространство, двойственное к релевантной алгебре, представляет собой релевантное пространство.

Более того:

(3) Если Я является релевантной алгеброй, то Я изоморфна ее второму дуалу, Л(Д?)), что дается отображением Да) = {хе^(?): аех};

(4) Если <К, г~ гомеоморфно (т.е. упорядоченно гомеоморфно и изоморфно по отношению к тернарному отношению, *-операции и единице) второму дуалу Я^Дф), при отображении 0(х) = {ЯеДЗ^хеф.

Для наших целей удобно использовать следующие понятия [Urquhart 1996, р.273]. Если х,у являются элементами релевантного

пространства то определим х®у как множество {zeRxyz}, х-~у будет множеством {ze} и х = {z: zgx*}; для X.Y - подмножеств пространства 3?.- определяем X®Y как множество U {х®у: xeX, yeY}, X~Y будет множеством n{x~у: хеХ, уе У} и = X - {=1 х: хеХ). Элементы релевантного пространства можно фактически отождествить с главными фильтрами, т.е. xe можно отождествить с [х) = {у х < у}. В этом случае множество х@у совпадает с множеством [х)®[у), х~у совпадает с множеством [х) —[у) и =1 х = =1 [х).

Приступим теперь к непосредственному построению топоса Set*. Рассмотрим вначале функтор Q: А —» Set (гдее А есть RN- категория), который будет представлять собой классифицирующий объект в топосс Set*. Как и в интуиционистской логике для любого функтора F: А —э Set определим как F_p значение F(p) функтора F для объекта р из А. Для произвольных q и р, таких, что р < q, функтор F определяет функцию из F_p в F_q, которую мы обозначим как F_pq. Функтор F будет рассматриваться как совокупность { F_p: ре А} множеств, индексированных элементами множества объектов А и снабженной отображением перехода F_P4. F_p —» F_q по р < q (в частности, F_pp будет представлять собой функцию тождества на F_p).

Продолжим подобным образом, полагая Q_p = [р)⁺ (т.е. равной релевантной алгебре всех главных фильтров в [р)), и определяя для р и q, таких, что р < q, функцию Q_pq: Q_p -» Q_q, отображающую каждый 5е[р)⁺ в Sn[(7)e [qf, т.е. f2_ОТ(5) = S_q.

Постоянный функтор 1: А —» Set может быть определен с помощью условий 1 _р= {[1)} для р&А и 1 _pq = при р < q. Классификатор подобъектов true-. 1 —» Q представляет собой естественное преобразование, чья p-я компонента true_p: {[1)} -» Q_p будет определяться равенством true_p ([1)) = р). Таким образом, функция true выбирает наибольший элемент из каждой релевантной алгебры [р)⁺-типа.

Пусть т: F >г* G будет произвольным подобъектом Set*- объекта G. Каждая компонента х_р является инъективной и может рассматриваться как функция включения F_P^G_P. р-я компонента (Хх)_р- G,,—» [р)* характеристической стрелки y_t: G —> Q будет идентифицироваться с помощью равенства

для каждого хе G_p.

Легко убедиться, что Q-аксиома выполняется в категории (то- посе) Set* поскольку доказательство этого факта требует использование свойств главных фильтров в точности как в [Гольдблатт 1983] для случая интуиционистской логики.

Вначале мы сконструируем истинностные стрелки в топосе Set*. Конъюнкция и дизъюнкция будут определяться так же, как и в случае Set^p, где Р есть алгебра Гейтинга, т.е. нам, в сущности, нужны для гсйхй^йииОхй-эП определения их р-х компонент в виде

Стрелка false'A —> П может быть определена как естественное преобразование, чья р-я компонента false_p. {=) [1)} —> Q_p будет определяться равенством false_p([ 1)) = =j [р). Таким образом, функция false выбирает наибольший элемент из каждой релевантной алгебры (=i [р))⁺-типа.

Для отрицания О -ч О мы определяем р-ю компоненту —>_р: С1_Р —> Г2р как

Импликация э: fi х Q ч Й получается при определении ее р- ой компоненты как

Отметим, что истинностными стрелками в Set* являются естественные преобразования, компоненты которых совпадают с соответствующими связками (операциями) на релевантных алгебрах в А. Однако истинностные стрелки получались и в случае Set^p из категорного описания интуиционистских истинностных функций в Set в [Гольдблатт 1983]. Нетрудно прийти к выводу, что общая структура, отражаемая в топосах Set* и Set* вызвана тем обстоятельством, что и релевантные алгебры и алгебры Гейтинга содержат в себе дистрибутивные ограниченные решетки. По сути дела, то обстоятельство, что Set* есть топос, означает обязательное существование в нем еще и экспоненциала, обусловленного резиду- альностью интуиционистской импликации относительно решеточного пересечения, т.е. релевантная структура здесь наложена на интуиционистскую, представляющую собой некоторый базисный фон.

Будем называть Set*-оценкой функцию V: Ф₀ —> iSe<*(l,Q), назначающую каждой пропозициональной букве к, некоторое истинностное значение У(л,) = 1 —> Q. Эта функция может быть продолжена на множестве всех формул Ф следующим способом:

Мы говорим, что формула а &^-общезначима (что записываем как Set*=а), если К(а) = true: 1->0 для всех .^/-оценок V.

Напомним, что если Л является релевантной алгеброй, то мы можем определить оценку К'как отображение из Ф в Л, а формула А общезначима в Л, если 1 < У'(А ) для любой оценки V формул из Ф в Л логика, определяемая Л, будет представлять собой множество всех формул, общезначимых в Л.

По V мы определяем оценку У, положив

Лемма 1. У( а) = true тогда и только тогда, когда 1 < У (а). Доказательство. Для а = л, лемма справедлива в силу определения. Далее мы применяем индукцию по построению формулы. Пусть а = —и Уф) = false, тогда

Следовательно, Г(а)Д[1)) = -у,(Г(р)Д[1)) = ^_p(false_p({))) = (по

индуктивному определению) = —._p(=j [р)) = р) = true_p([ 1)). Таким образом, У( а) = true and 1 < У (а). Остальное доказывается обычным образом. ?.

Теорема 1. Для любого топоса Set*, Set*t= а тогда и только

тогда, когда -_к а (т.е. а доказуема в R).

Доказательство. Поскольку по лемме 1 мы выбираем оценку V абсолютно произвольно и для У полнота уже доказана, то мы приходим к требуемому заключению. ?.

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