Варианты субэкспоненциала локального сокращения в исчислении Ламбека

Исчисление Ламбека было введено как инструмент для исследования лингвистических конструкций. В дальнейшем это исчисление пополнялось как новыми связками, так и структурными правилами, вроде правил сокращения, ослабления и перестановки. Эти структурные правила разрешаются только для формул под знаком особой модальности, называемой экспоненциалом. Само исчисление Ламбека является некоммутативной субструктурной логикой, и для произвольных формул эти структурные правила не допускаются. Следующий шаг — введение системы субэкспоненциалов: под знаком такой модальности могут допускаться лишь некоторые структурные правила.
Возникает следующий вопрос: можно ли сформулировать систему с тем или иным вариантом правила локального сокращения (для формул под субэкспоненциалом), чтобы восстановить свойство устранимости сечения? Рассматриваются два подхода к решению этой задачи: можно как ослабить правило введения ${!}$ в правой части секвенции (LSCLC), так и расширить правило локального сокращения с отдельных формул до их подпоследовательностей (LMCLC). Стоит также отметить, что в коммутативных исчислениях такой проблемы нет в силу возможности перестановки формул в секвенции (т. е. локальное и нелокальное правила сокращения совпадают).
Доказываются следующие результаты:
устранимость сечения в исчислениях LMCLC и LSCLC;
алгоритмическая разрешимость фрагментов этих исчислений, в которых ${!}$ разрешается применять только к переменным;
алгоритмическая неразрешимость LMCLC (для LSCLC разрешимость остаётся открытым вопросом);
корректность и отсутствие сильной полноты LSCLC относительно класса реляционных моделей;
различные результаты об эквивалентности для этих исчислений и исчислений с другими вариантами субэкспоненциала сокращения.