Секвенции в коситусах (логика Брауэра)

Понятие копокрытий дуально по отношению к понятию покрытий в алгебре Гейтинга. Теперь мы будем работать с дуальными конструкциями в алгебре Брауэра. Последняя дуальна к алгебре Гейтинга и имеет структуру В = (5,a,v,—,1), где а — b есть псевдодополнение а относительно Ь. Соответствующие категорные аналоги выглядят следующим образом.

Определение 1. В-категория С является конечной кополной декартово козамкнутой категорией предпорядка, т.е. для любых а,Ь из С существует С-объект <= (коэкспоненциал) и С-стрелка ev°: b —» [а <= Ь,а (стрелка кооценки), такая, что для любого объекта с в С следующая диаграмма

будет коммутативна, T.e.(g+la)°ev° = g.

Определение 2. BN-категория С является В-категорией, снабженной контравариантным функтором N: С —> С, таким, что:

  • (i) Na = а <= 1;
  • (ii) N(a —> b) = Nb -> Na

где <= есть коэкспоненциал, и мы полагаем, что:

(iii) a->b есть стрелка в С тогда и только тогда, когда а<=Ь=0 для любых двух объектов а,Ъ из С.

Напомним, что Н. Гудменом [Goodman 1981] была предложена система логики Брауэра, которая в [Смирнов 1987, с.223] сформулирована в виде секвенциального исчисления LB (см. параграф 8, глава первая). С соответствующими изменениями LB может быть переписана как секвенциальное исчисление с начальной секвенцией единственного вида а—>а и следующими добавочными правилами:

где г есть брауэровское отрицание.

Интерпретация в терминах BN-категорий будет основываться на следующей модификации определенного нами ранее словаря перевода высказываний интуиционистской логики в Н-категорию:

Определение 3. Копредтопология на С есть функция, сопоставляющая каждому С-объекту р совокупность CoCovip) множеств С- стрелок с началом в р (копокрытий), таких, что:

  • (i) 1 peCoCov(p);
  • (ii) если —> р,: iel} и для любого iel мы имеем {р, —> р'у. jeJi}eCoCov(pi), то ->р): iel & jeJi) eCoCov(p)
  • (iii) если p^*rp^>qeCoCov(p), то [r,q]—>peCoCov{p), и наоборот ([-,-]-замкнутость).

Из нашего определения следует, что пара (C,Cov) есть коситус. Как и в случае Н-категорий, мы налагаем еще одно ограничение на копредтопологию:

(iv) каждое CoCov(p) максимально по отношению к N- функтору, т.е. либо aeCoCovip), либо NaeCoCov(p), но не оба одновременно.

Теорема 1. Все аксиомы и правша LB могут быть интерпретированы в коситусе (C,CoCov), где С есть BN-категория.

Доказательство. Все доказывается дуально к соответствующим случаям интерпретации в Н-ситусе. ?

Формульным эквивалентом каждой секвенции р —> аь ... , а„ будет Р — а.]л ... лат. Для каждого копокрытия мы определяем одно-однозначное отображение /Вг: CoCov —> Form, с помощью

CoCov(p) •— а <= (]^|аг- ) ввиду (iii). Остальное дуально интуицио-

/«/

нистскому случаю.

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