Главная Логика
КАТЕГОРНАЯ ЛОГИКА
|
|
||||||
седьмая. Логические исчисления в топосахРелевантная логика в топосахИзвестно, что для любой малой категории С категория 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}. Выполняются следующие условия:
где L{S) есть двойственная к S решетка. Двойственная к ^алгебра Я(‘%) определяется на решетке L(S) путем добавления операций А°В, А-^В, -А = {z: z*eA} и определения константы 1 как /. Для релевантной алгебры L двойственное пространство L, R^L), определяется путем добавления к решетке всех простых фильтров ограниченной дистрибутивной решетки тернарного отношения х-у с z, определяя х* для xe
Более того:
Для наших целей удобно использовать следующие понятия [Urquhart 1996, р.273]. Если х,у являются элементами релевантного пространства Приступим теперь к непосредственному построению топоса 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: Qp -» Qq, отображающую каждый 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. Эта функция может быть продолжена на множестве всех формул Ф следующим способом: Мы говорим,
Напомним, что если Л является релевантной алгеброй, то мы можем определить оценку К'как отображение из Ф в Л, а формула А общезначима в Л, если 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 абсолютно произвольно и для У полнота уже доказана, то мы приходим к требуемому заключению. ?. |
<< | СОДЕРЖАНИЕ | ПОСМОТРЕТЬ ОРИГИНАЛ | >> |
---|