Аннотация:
Инфинитарная логика действий $\mathrm{ACT}^\omega$ описывает эквациональную теорию $*$-непрерывных решёток Клини с делениями и представляет собой инфинитарное расширение мультипликативно-аддитивного исчисления Ламбека ($\mathrm{FL}$) с помощью итерации Клини. Задача выводимости в $\mathrm{ACT}^\omega$ алгоритмически неразрешима и $\Pi^0_1$-полна [Buszkowski, Palka 2007]. Само исчисление $\mathrm{FL}$ — это субструктурная логика, в ней отсутствуют структурные правила сокращения, ослабления и перестановки. Рассматриваются расширения $\mathrm{FL}$ различными комбинациями структурных правил. Среди таких логик единственной алгоритмически неразрешимой является логика $\mathrm{FL}_{\mathsf{c}}$, расширяющая $\mathrm{FL}$ правилом сокращения [Chvalovský, Horcík 2016]. В докладе рассматривается логика $\mathrm{ACT}^\omega_{\mathsf{c}}$, расширяющая $\mathrm{FL}_{\mathsf{c}}$ итерацией Клини. Для этой логики построен вариант языковой семантики (с подходящей операцией замыкания), доказана теорема о полноте. Доказано, что задача выводимости в $\mathrm{ACT}^\omega_{\mathsf{c}}$ является $\Pi^1_1$-полной, что намного сложнее, чем для $\mathrm{ACT}^\omega$.
