Полная версия

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

  • Увеличить шрифт
  • Уменьшить шрифт


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

Паранепротиворечивая логика в топосах

Построим теперь категорную семантику для паранепротиворе- чивой логики, используя CN-категории. Поскольку у нас имеется категорнос представление алгебры да Косты в виде CN-категорий, то мы можем попытаться получить Set* в качестве модели паране- противоречивой логики, заменяя RN-категорию А на CN- категорию.

Теорема 1. Множество главных фильтров алгебры да Косты =-изоморфно алгебре да Косты.

Доказательство. Пусть А = (А, 0, 1, <, л, v, г>, ') будет некоторой алгеброй да Косты. Фильтр F на А представляет собой непустое подмножество А, такое, что:

  • (1) если a.beF, то алЬеК,
  • (2) если аеF и а<Ь, то beF.

Фильтр F является собственным фильтром, если OgF. Говорят, что фильтр F будет Л-полным (или полным относительно А), если a'Aa°eF или aeF, но не оба одновременно.

Рассмотрим множество А' всех главных фильтров, т.е. множество вида

Относительно теоретико-множественного включения с, пересечения, объединения и дополнения А* будет представлять собой алгебру Макнейла [MacNeille 1937], т.е. полную булеву алгебру. Если определить на А* упорядочение < как р) < [<7) тогда и только тогда, когда q < р, то очевидным образом мы получаем предпоря- док на Л+. Определим теперь операцию ' как

[рУ = -р) kj —.[/?“) где -1 - булево дополнение на А*, т.е. -i[jc)={y: [у)п[х)=0]. Поскольку, очевидным образом p)rq) = [рл<7) и [р)и[<7) = |pvq) (А является дистрибутивной решеткой, поэтому А вложима в решетку своих главных фильтров [Расёва Сикорский 1972, с.82]), то, учитывая закон да Моргана, получаем -l[p)u-.[p°) = -i([p) п [р0)) = -п[рлр°). В булевой алгебре А* [рлр°) представляет собой элемент [у), такой, что [рлр°) п [у) = 0. С другой стороны, согласно [Camielli Alcantara 1984, р.82], множество всех фильтров на А будет представлять собой логику да Косты (А,С), в которой С представляет собой систему замыканий всех фильтров на А. Для логики да Косты имеет место тот результат [Camielli Alcantara 1984, р.87], что она является паранепротиворечивой абстрактной логикой. Для нас существенно, что тогда фактически все фильтры являются A-полными, т.е. либо aeF, либо a'Aa°eF, но не оба одновременно, поскольку в этом случае [a)vj[a'Aa°) = А. Тогда очевидным образом [а) п [а'ла0) = 0 = [ала'ла0) = [а') п [ала0). Следовательно, в роли [р') в А* будет выступать [у), и мы окончательно получаем [р)' = [р'). Определим теперь [р) з [q) = -р) J [9).

Лемма /. [р з <7) = ->[р) и [q).

Доказательство. В А мы имеем ал(а з Ь) < Ь, откуда получаем [6) с [а) п [а з Ь). Далее, в булевой алгебре А* мы получаем -.[а) и [Ь) с -i[a) и ([а) п[аз4))-/(п (—фа) п [а з b)) = -фа) о [а з Ь). Но в А ала'ла0 = 0, следовательно, ала'ла0 < Ь, откуда а'ла°< аэй[аз/>)с [а'ла0). Но а'ла0, согласно [Camielli Alcantara 1984, р.81], играет роль классического отрицания, откуда [а з Ь) с -фа) и -{а) п [а з Ь) = [а з Ь). Отсюда получаем —>[a) и [6) с [а з Ь).

Далее, в А алЬ < b влечет b <(а з Ь), откуда в А+ мы получаем [аз6)с [6). Но поскольку [аз Ь) с -фа), то в булевой алгебре А+ получаем [а з b) с -фа) и [6). Следовательно, [р ZDq) = —i[/?)w[^). ?

Из доказанной леммы 1 следует [р) з [[р з q). Отсюда мы получаем сохранение всех операций алгебры да Косты на А* и тогда мы можем говорить об отображении <р: А -» А+, которое очевидным образом будет ^-изоморфизмом. ?

Рассмотрим теперь вопрос релятивизации А*. Поскольку А* является полной булевой алгеброй, то для любого [р)еА’ мы стандартным образом можем получить булеву алгебру [р)+ всех главных фильтров в [р) [Расёва Сикорский 1972, с.96]. При этом 0 по- прежнему является нулевым элементом, а единицей теперь будет [р). Так как предупорядочение < теперь можно просто получить сужением отношения предпорядка в А* на [р), а операции ' и з могут быть релятивизированы через булевы операции в [р)+, то нетрудно превратить [р)+ в алгебру да Косты.

Таким образом, обозначая [р)л[^г) через [q)p, мы получаем для S,TeA+ (сужая операции из А* на [р)+):

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

При подобном подходе мы полагаем Пр = [р)+ и для р и q, таких, что р < q, функция Qpq: Qp —> Qq сопоставляет каждому Se[p)+ множество S п [q)e[q)*, т.е.. Q;4(S) = Sq.

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

Пусть теперь т: F G - произвольный подобъект Set*- объекта

G. Каждая компонента хр является инъективной и может рассматриваться как функция включения FP^GP. р-я компонента (х,)р: Gp-> [р)+ характеристической стрелки yt: G —> определяется ра

венством

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

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

Переходя теперь непосредственно к конструированию интерпретации паранепротиворечивой логики в топосе Set*, построим вначале истинностные стрелки. Начнем со стрелки false.

Начальный объект 0: А -> Set категории Set* - это постоянный функтор, такой, что 0Р = 0 и 0W = ide для р < <у. Компонентами естественного преобразования 0 —> 1 являются 0 ^ {0} (она и та же компонента для любого р). По определению стрелка false характеристической стрелкой подобъекта !: 0 1. Для ее компоненты

false/. {0} -> Ар имеем falseр(0) = {q:p и 1и(0) = О,} = {q: р < q и Ое0} = 0, и, следовательно, естественное преобразование выбирает нулевой элемент из каждой алгебры да Косты,

Что касается конъюнкции и дизъюнкции, то их определения остаются те же, что и в случае Setр [Гольдблатт 1983], т.е. фактически нам нужно для п: fixQ ?/> Q and u: QxQ Q определения их p-x компонент в виде

Для определения стрелок отрицания и импликации используем то обстоятельство, что в алгебре [pf они конструируются из булевых операций. Но в этом случае булево отрицание выглядит у нас

как -с Q Q , чья p-я компонента —>р flp—> flp при отождествлении falsep с включением {0}с flp (и поскольку —Q —> Q является характеристической стрелкой подобъекта false) выглядит следующим образом:

Отсюда отрицание = : Q -r> Q получаем, выводя, что р-я компонента = р: flp—> flp отрицания удовлетворяет равенству

Импликацию =>: QxQ —> Q получаем, определяя р-ю компоненту с помощью (4) как

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

вая как Se/t=a) если F(a) = true: 1 —» Q для всех Set*-оценок V.

Определим оценку У: Ф0 —> {0,1}, продолжая ее на Ф следующим образом:

  • 1. 2. 3.
  • 4.
  • 5.
  • 6.
  • 7.

Связь между V и V получаем, положив

Лемма 2. V( a) = true тогда и только тогда, когда У (а) = 1. Доказательство. Для a = л; лемма истинна по определению. Далее мы прибегаем к индукции по длине формул, т.е. учитывая наши пункты 1 - 7. Пусть a = —>р и Уф) = false, тогда

Следовательно, F(a)p(0) = ->ДК(р)Д0)) = -*p(falsep(0)) = (по индуктивному предположению) = ->р(0) = [р) = truep(0). Отсюда F(a) = true и У(a)= 1. Точно так же проделываем в остальных случаях. ?

Теорема. Для любого топоса Set* Set* t= а тогда и только тогда, когда Ь с, a (т.е. а доказуема в С|).

Доказательство. Поскольку по лемме 2 выбор оценки V произволен, а для У в [da Costa Alves 1976] доказана полнота, то это приводит к требуемому результату. ?

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