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

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

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

Доказательство. Пусть А = (А, 0, 1,, ') будет некоторой алгеброй да Косты. Фильтр 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. С другой стороны, согласно [Camielli Alcantara 1984, р.82], множество всех фильтров на А будет представлять собой логику да Косты (А, С), в которой С представляет собой систему замыканий всех фильтров на А. Для логики да Косты имеет место тот результат [Camielli Alcantara 1984, р.87], что она является паранепротиворечивой абстрактной логикой. Для нас существенно, что тогда фактически все фильтры являются A-полными, т. е. либо aeF, либо a’Aa°eF, но не оба одновременно, поскольку в этом случае [a)vj[a'Aa°) = А. Тогда очевидным образом [а) п [а'ла⁰) = 0 = [ала'ла⁰) = [а') п [ала⁰). Следовательно, в роли [р') в А* будет выступать [у), и мы окончательно получаем [р)' = [р'). Определим теперь [р) з [q) = -р) J [9).

Лемма /. [р з [р) и [q).

Доказательство. В А мы имеем ал (а з Ь) < Ь, откуда получаем [6) с [а) п [а з Ь). Далее, в булевой алгебре А* мы получаем -. а) и [Ь) сi[a) и ([а) п[аз4))-/(п (—фа) п [а з b)) = -фа) о [а з Ь). Но в, А ала’ла⁰ = 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 обозначим через F_p значение F (p) функтора F на объекте р из А. Для любых q и р, таких, что р <* q, функтор F определяет функцию из F_p в F_q, которую обозначим F_pq. Функтор F будем рассматривать как семейство {F_p: реА} множеств, заиндексированных элементами множества А из алгебры А снабженных отображением перехода F_pq: F_p —> F_q при р < q (в частности, F_pp будет тождественной функцией на F_p).

При подобном подходе мы полагаем П_р = [р)⁺ и для р и q, таких, что р < q, функция Q_pq: Q_p —> Q_q сопоставляет каждому Se[p)⁺ множество S п [q)e[q)*, т. е. Q_;4(S) = S_q.

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

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

G. Каждая компонента х_р является инъективной и может рассматриваться как функция включения F_P^G_P. р-я компонента (х,)_р: G_p-> [р)⁺ характеристической стрелки y_t: G —> определяется ра венством для каждого хе G_p.

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

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

Начальный объект 0: А -> Set категории Set* — это постоянный функтор, такой, что 0_Р = 0 и 0_W = ide для р < 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-я компонента —>_р fl_p—> fl_p при отождествлении false_p с включением {0}с fl_p (и поскольку —Q —> Q является характеристической стрелкой подобъекта false) выглядит следующим образом:

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

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

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

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

Определим оценку У: Ф₀ —> {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(false_p(0)) = (по индуктивному предположению) = ->_р(0) = [р) = true_p(0). Отсюда F (a) = true и У (a)= 1. Точно так же проделываем в остальных случаях. ?

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

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