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

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

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


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

Декартово бизамкнутые дедуктивные категории

Декартово бизамкнутая дедуктивная категория представляет собой полное интуиционистское дедуктивное исчисление, выполняющее следующие дополнительные тождества:

для всех /? Ah С, g: В- Си h: A v В- С.

Операция (-)v (-) была определена ранее как / v g = Ав ( /

л g ))s. Порою пишут 0 вместо ± и А + В вместо A v В. В этом случае (в математической терминологии) тождества утверждают, что 0 есть инициальный объект, а А + В представляет собой копроизведение с инъекциями рАв и р'^в- Отсюда Агг(1Д) имеет в точности один элемент и Агг(А,С) х Агг(В,С) будет изоморфно Arr(/fv

B, С).

Если понимать изоморфизм A Ht- В как факт одновременного существования стрелок А В п В А, то нетрудно доказать, что в декартово бизамкнутых категориях имеют место следующие стрелки:

Для декартово бизамкнутых дедуктивных категорий имеет место функциональная полнота. Точнее, мы имеем:

Предложение 1. Если А есть декартово бизамкнутая дедуктивная категория и А[х] есть декартово замкнутая дедуктивная категория полиномов по индетерминанту х: Тн А над А, то А[х] также является декартово бизамкнутой дедуктивной категорией.

Доказательство. Сошлемся на одно-однозначное соответствие между стрелками В- С в А[х] и стрелками A v В- С в А. Таким образом 1 будет инициальным объектом в А[х], поскольку (записывая изоморфизм как =)

а последнее множество имеет как раз один элемент, потому что 1 есть инициальный объект в А. Опять, В v С (т.е. В + С) является дизъюнкцией (копроизведением) в Л[х], потому что

Здесь используется тот факт, что л В) х л С) есть копроизведение в А[х], а также дистрибутивный закон

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