Инфинитарная логика действий с экспоненциальными модальностями

Логика действий аксиоматизирует эквациональную теорию решёток действий, или решёток Клини с делениями. Решётки Клини с делениями сочетают структуру решётки, структуру моноида с делениями (связанными с частичным порядком) и итерацию Клини. В инфинитарной версии логики действий итерация аксиоматизируется посредством омега-правила, что делает эту логику алгоритмически неперечислимой, а именно, $\Pi_1^0$-полной. Логика действий относится к субструктурным логическим системам, т.е. в ней отсутствуют правила сокращения, ослабления и перестановки формул. Эти правила можно частично восстановить с помощью экспоненциальной модальности, под знаком которой они разрешены. В работе [1] доказано, что добавление такой модальности к инфинитарной логике делает её $\Pi_1^1$-полной. Также доказано, что замыкающий ординал оператора непосредственной выводимости для этой системы равен $\omega_1^{CK}$. В работе [2] рассмотрен вариант экспоненциальной модальности, допускающий правило мультиплексирования вместо правила сокращения. Для такого исчисления замыкающий ординал не превосходит $\omega^\omega$, а сложность лежит между полной арифметикой первого порядка и $\Sigma^0_{\omega^\omega}$-уровнем гиперарифметической иерархии.