Многоуровневые дедуктивные системы и дедуктивные п- категории

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

Напомним, что дедуктивная категория есть дедуктивная система, в которой между доказательствами имеют место тождества типа 1 ef~f (hg)/= h (gf). Казалось бы, что эти тождества имеют совершенно ясный смысл в теории доказательств. И это действительно так, за одним мелким, но досадным исключением. Что формально означает понятие «тождества», употребленное в такой формулировке?

В дедуктивных категориях обычно говорят не о тождестве двух объектов, но об их изоморфизме (одно-однозначном соответствии), определяемом с помощью стрелок (туда и обратно), т.е. формулы могут быть разными, но доказательно эквивалентными. В этом случае понятие тождества-изоморфизма не требует обращения к какой-либо содержательной теории тождества, внешней по отноше-

нию к категории как логической системе. Однако этот подход не работает для стрелок - в категории нет «стрелок» для стрелок, позволяющих использовать понятие изоморфизма вместо понятия тождества. Следовательно, понятие тождества для стрелок не то же, что понятие тождества для объектов. В двухуровневых категориях та же самая проблема возникает для стрелок второго уровня (метастрелок) - понятие тождества в общем случае может быть содержательно другим. Если же быть последовательным, то следует избегать обращения к такого рода содержательным понятиям (даже если явно указывать, какое понятие тождества подразумевается на каждом уровне). Поэтому для определения тождества в двухуровневых категориях приходится обращаться к трехуровневым категориям и т.д. Выполнение подобной программы приводит к понятию многоуровневых систем и так называемых /7-категорий (где п указывает на то, что на каком-то /7-ом уровне мы отказываемся от своего ригоризма и заменяем понятие изоморфизма некоторым неформальным понятием тождества).

Рассмотрим понятие так называемого /7-графа (см. [Marcinek Oziewicz 2001]).

Определение 1. оо-граф G представляет собой бесконечную последовательность семейств /-ячеек {G,}l€z, последовательность сюрьективных начал {sc = $/} и концов {to = /,}, и семейство сечений {/<; = /,},

Пусть type х = (sx,tx) (т.е. определяем понятие типа). По определению все 0-ячейки имеют один и тот же тип, должно быть не более двух и не менее одной (-1)-ячейки, G. = {s.Gq, /.iGo}. Биотображение G,: G,xG, -» 2 ,+1 определяется следующим образом. Если xj'EG/xG,, то

Должны выполняться следующие условия:

' 1. Если type х * type у, то Gj(x,y) = 0;

2. Sjoit = /,<>1*,.

Определение 2. Если для всякого /'EN имеет место G,+„ = G„, то про оо-граф G говорят, что он является п-графом. В этом случае 5,>„

t[+n И I/;* 1 °f ] ]'

Если для любых х,у, таких, что type х = type у, и для всякого /Е N имеет место |G,{x,y)| = 1, то про и-граф говорят, что он является скелетальным.

Таким образом, «-графы с формулами в качестве 0-ячеек (в частности, с формулой Т) и доказательствами в качестве 1-ячеек будут представлять собой многоуровневые дедуктивные системы (2- ячейки в этом случае можно рассматривать как стратегии доказательств в стиле предыдущего параграфа). И, наконец, на основании этих понятий, мы можем определить, что представляет собой и- категория.

Определение 3. п-категория есть и-граф G с операцией композиции

и-категория G является точной, если композиция са ассоциативна, в противном случае она является слабой и-категорией. Отсутствие ассоциативности означает, что у нас вместо равенств для стрелок соответствующих уровней присутствуют метастрелки, т.е. вместо уравнений (hg) f = h (gf) мы имеем «стрелку-ассоциатор» O-Uh ? (%)/=> h (gf).

Слабую 2-категорию обычно называют бикатегорией [Benabou 1967], слабую 3-категорию - трикатегорией [Gordon Power Street 1995], [Baez 1997]. 0-ячейки также называют объектами, 0- морфизмами, вершинами; 1-ячейки - морфизмами, 1-стрелками, функторами; 2-ячейки - 2-морфизмами, морфизмами морфизмов, естественными преобразованиями и т.д.

Таким образом, мы получаем дедуктивную п-категорию, полагая формулы в качестве 0-ячеек и доказательства в качестве 1- ячеек. Однако в этом случае мы также получаем две разновидности дедуктивных «-категорий - сильную и слабую, в зависимости от выбора равенств или стрелок для уравнений ассоциативности композиции соответствующих уровней.

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