Несколько иначе выглядит ситуация для исчислений Айдукевича-Ламбека. В этом случае мы будем иметь дело не с 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). Ее р-я компонента удовлетворяет уравнениям.
