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

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

Известно, что для любой малой категории С категория 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 определим как Fp значение F(p) функтора F для объекта р из А. Для произвольных q и р, таких, что р < q, функтор F определяет функцию из Fp в Fq, которую мы обозначим как Fpq. Функтор F будет рассматриваться как совокупность { Fp: ре А} множеств, индексированных элементами множества объектов А и снабженной отображением перехода FP4. Fp —» Fq по р < q (в частности, Fpp будет представлять собой функцию тождества на Fp).

Продолжим подобным образом, полагая Qp = [р)+ (т.е. равной релевантной алгебре всех главных фильтров в [р)), и определяя для р и q, таких, что р < q, функцию Qpq: QpQq, отображающую каждый 5е[р)+ в Sn[(7)e [qf, т.е. f2ОТ(5) = Sq.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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