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

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

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


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

Устранение сечения в свободных сопряжениях

Пусть теперь (A*,B*,F,G,q>,у) будет свободным сопряжением, порожденным парой множеств объектов. Назовем вхождение символа композиции 0 в стрелочный терм из Л* или В* сечением. Каждое сечение в стрелочном терме А из Л* и В* определяется подтермом h вида h2 ° Ль который мы будем называть подтермом сечения.

Степень стрелочного терма есть число вхождений символов 1,°,F (примененного к стрелочным термам), G (примененного к стрелочным термам), <р или у в этих стрелочных термах. Если подтермом сечения является й2 ° hu то степень сечения будет степенью Л2° Л,.

Докажем теперь следующую теорему.

Теорема устранения сечения. Для любого стрелочного терма h из А* существует свободный от сечения стрелочный терм И'из А*, такой, что h = И'в А*, и то же самое справедливо для В*.

Набросок доказательства. В стрелочном терме И из Л* или из В* возьмем сечение наивысшего уровня, т.е. сечение, чей подтерм h2 ° h таков, что в h и h2 нет сечений. Покажем путем рассмотрения всех возможных случаев, что существует такой стрелочный терм h что h2 0 Ai = h'и И'либо свободен от сечения, либо содержит сечение наивысшего уровня, чья степень все еще в точности меньше степени h2° h. Отсюда индукцией по длине терма получим, что существует стрелочный терм h такой, что h2° h = ИИ'свободен от сечения. Теорему получаем индукцией по числу сечений в И. В полном доказательстве этой теоремы используется все равенства (i)-(iv) из определения сопряжения кроме случая ассоциативности композиции стрелок категории. ?

Свободный от сечения стрелочный терм из Л* или из В* вида Q, ... Q„lc где и > 1, каждый Q, есть либо F, либо G, либо <р, либо у, а С представляет собой порождающий объектный терм, будет называться нормальной формой. С помощью теоремы устранения сечения и условия F(A) = 1 f(A) легко получить теорему о нормальной форме:

Теорема о нормальной форме. Для каждого стрелочного терма h из А* или В* существует стрелочный терм И'из А* или В* в нормальной форме, такой, что h = h 'имеет место в А* или В*.

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