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

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

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


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

Исчисления Айдукевича-Ламбека в голосах

Несколько иначе выглядит ситуация для исчислений Айдукевича-Ламбека. В этом случае мы будем иметь дело не с N- категориями, как в случаях релевантной и паранепротиворечивой логики, но с S-категориями - категориями предпорядка, снабженными ковариантным бифунктором ®: ми

Обозначим для любого р из G = (| GI, Ер множество Ер= {q: q которое очевидным образом будет представлять собой полугруппу с операцией а-рЬ = min(a-b,p)

а затем определяем на операции следующим образом:

для Er, Eq с Ер

  • 1. Ег-рЕя = {с: с для некоторого aeEr, beEq},
  • 2. Ег1рЕд = {сеЕр. c-pb для всякого beEq},
  • 3. ErpEq = {сеЕр: а-рС для всякого аеЕг).

Нетрудно видеть, что Е = (Ер, -р, 1р, р>, где Ер. Расширяя G естественным образом до резидуальной полугруппы и обозначая S соответствующую S-категорию, мы получаем функтор Q на объекте р S-категории S как 0.р = Е*р и для любого функтора F: S -» Set обозначим как Fp значение F(p) функтора F для объекта р из S. Для произвольных q и р, таких, что p'&q, функтор F определяет функцию из Fp в Fq , которую мы обозначим как Fpq. Функтор F будет рассматриваться как совокупность {Fp: ре | GI} множеств, индексированных элементами | GI, снабженная отображением перехода Fpq: Fp —» Fq по р (в частности, Fpp будет представлять собой функцию тождества на Fp).

Определим для р н q, таких, что р функцию Qp —> Qq, отображающую каждый ЕгеЕ*р в EseE*q, т.е. Q.pq(Er) = EseE*q. Постоянный функтор 1: S -» Set может быть определен с помощью условий 1 р= {0} для peS и ря = при р q. Классификатор подобъектов true: 1 -» О представляет собой естественное преобразование, чья р-я компонента truep: {0} —> О.,, будет определяться равенством truep (0) = Ер. Таким образом, функция true выбирает наибольший элемент из каждой резидуальной полугруппы над Ер.

Можно убедиться, что Q-аксиома выполняется в категории (топосе) Sets поскольку доказательство этого факта требует использование свойств наследственных множеств (как в [Гольдблатт 1983] для случая интуиционистской логики). Поскольку наши Fp- множества являются конаследственными, то получаем, что Sets также будет топосом, и мы можем начать определять соответствующие истинные стрелки.

Начнем со стрелки ®. Мы получаем ®: fixQ —> О как характеристическую стрелку для

{true, true). Ее р-я компонента удовлетворяет уравнениям

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