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

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

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


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

Секвенции в Ра-ситусах

Главным недостатком интерпретации в категориях предпорядка является невозможность рассмотрения проблемы отождествления выводов. Как следствие, например, мы оказываемся не в состоянии стандартным образом развить в таких категориях подход, предложенный Дж. Ламбеком и описывающий подобного рода аспекты взаимоотношения между категориями и теорией доказательств.

Возможный путь преодоления этих трудностей может быть найден при использовании так называемых категорий путей.

Определение 1. Для любой категории предпорядка С категорией путей РаС является такая категория, что:

  • (i) объекты РаС те же, что и С;
  • (ii) /: а -> b есть стрелка РаС тогда и только тогда, когда f = fn° /„_1 ° -0 /j (и > 1), где /j есть стрелки С, а

является областью определения // и b является областью значения/,.

Очевидным образом С будет подкатегорией РаС, и непосредственной проверкой мы приходим к заключению, что следующее предложение может быть доказано:

Предложение I. Для любой N-категорш (HN-.BN-, HBN- категории) С категория путей РаС будет декартово замкнутой (соответственно козамкнутой, бизамкнутой) конечно полной (соответственно кополной, биполной) снабженной контравариант- ным функтором NPaC-^PaC (соответственно NhNi), таким, что выполняются соответствующие условия из определения В- категории (соответственно N-категории, BN-категории, HBN- категории).

Более того, естественным образом можно перейти от рассмотрения предтопологии в наших категориях предпорядка к топологии Гротендика в категориях путей.

Предложение 2. Предтопология в HN-категории (N-, BN-, HBN- категории) С определяет предтопологию Гротендика (поли-, ко-, бипредтопологию соответственно) в HN-категории (N-, BN-, HBN-категории соответственно) путей РаС.

Доказательство. Стандартное определение предтопологии Гро- тендика в [Гольдблатт 1983] выглядит следующим образом:

Предтопологией на категории С называется функция, сопоставляющая каждому С-объекту а совокупность Cov(a) множеств С- стрелок, оканчивающихся в а, такая, что

(1) одноэлементное множество {1 „д-эа) принадлежит Cov(a);

fr

(2) если х———>а:х е X] е Cov(a) и для каждого хеХ то

fr

(3) если х ———>а: х е X] е Cov(a) и g: bа - произвольная С-стрелка, то для каждого хеХ существует обратный образ стрелки f относительно g

и {Ьхах—? >b : х е X) е Cov(b).

а

Если С есть HN-категория, то мы должны проверить лишь выполнимость (3) в РаС. Но ввиду предложения 1 очевидно, что РаС имеет обратные образы и все (Ь,ах) принадлежат Cov(a) в силу определения предтопологии. В случае ко-, би- и полипредтопологии доказательство аналогично. ?

Теперь мы получаем Ра-стус (-коситус, -биситус, -полиситус соответственно) как пару (PaC,Cov) для любого ситуса (С,Соу) (коситуса, биситуса, полиситуса соответственно). В согласии с предшествующим рассмотрением секвенция Г-ч а в Яа-ситусс должна интерпретироваться как некоторый элемент Cov(a), где а есть перевод а, т.е. как конус {а(- -» а: i е 1}, где а, являются соответствующими переводами формул из Г.

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