Поликатегории, *-автономные категории, симметричные моноиадльно-замкнутые категории
Упоминавшаяся вчера статья Майка Шульмана, кстати, огонь! (https://arxiv.org/pdf/2004.08487.pdf)
Интересно и логикам и категорщикам. В очень явном виде строится конструкция, (а) вполне-унивалентным образом вкладывающая любую поликатегорию в *-автономную категорию, (б) вкладывающая любую замкнутую симметричную моноидальную категорию в полную и кополную *-автономную при помощи полного сильного симметрично-моноидальным функтора, который может быть выбран так, чтобы сохранять любой наперёд заданный набор выбранных пределов, копределов и тензорных произведений, (в) то же верно для линейно-дистрибутивных категорий.
С стороны логики месседж такой: мультипликативно-аддитивная (т.е. без экспоненциальных модальностей) линейная логика без 0 и ⊤ консервативна над аналогичной интуиционистской линейной логикой без 0.
Есть такой очень естественный с категорной и вычислительной (теоретико-типовой) точки зрения фрагмент линейной логики - интуиционистская линейная логика: _⊗_, 1, _⊸_, _&_, _⊕_. Вот обычная интуиционистская логика моделируется в декартово-замкнутой категории (где требуется наличие конечных сопроизведений, чтоб была дизъюнкция), а что будет если взять симметричную моноидально-замкнутую категорию? Вот в ней как раз интуиционистская линейная логика живёт. Естественный вопрос - насколько она слабее “классической” линейной логики, где всё симметричненько? Ну и вот ответ, что если без 0, то нинасколько. А если с 0, то слабее, потому как наличие нуля это в точности то, что позволяет закодировать оператор «не», который ведёт себя в классической и в интуиционистской логике по-разному, это известный результат Шеллинкса 1991 года.
Интересно и логикам и категорщикам. В очень явном виде строится конструкция, (а) вполне-унивалентным образом вкладывающая любую поликатегорию в *-автономную категорию, (б) вкладывающая любую замкнутую симметричную моноидальную категорию в полную и кополную *-автономную при помощи полного сильного симметрично-моноидальным функтора, который может быть выбран так, чтобы сохранять любой наперёд заданный набор выбранных пределов, копределов и тензорных произведений, (в) то же верно для линейно-дистрибутивных категорий.
С стороны логики месседж такой: мультипликативно-аддитивная (т.е. без экспоненциальных модальностей) линейная логика без 0 и ⊤ консервативна над аналогичной интуиционистской линейной логикой без 0.
Есть такой очень естественный с категорной и вычислительной (теоретико-типовой) точки зрения фрагмент линейной логики - интуиционистская линейная логика: _⊗_, 1, _⊸_, _&_, _⊕_. Вот обычная интуиционистская логика моделируется в декартово-замкнутой категории (где требуется наличие конечных сопроизведений, чтоб была дизъюнкция), а что будет если взять симметричную моноидально-замкнутую категорию? Вот в ней как раз интуиционистская линейная логика живёт. Естественный вопрос - насколько она слабее “классической” линейной логики, где всё симметричненько? Ну и вот ответ, что если без 0, то нинасколько. А если с 0, то слабее, потому как наличие нуля это в точности то, что позволяет закодировать оператор «не», который ведёт себя в классической и в интуиционистской логике по-разному, это известный результат Шеллинкса 1991 года.