Неразрешимость логики решёток Клини с делениями

Решёткой Клини называется решётка с дополнительными операциями умножения (задаёт структуру моноида) и итерации Клини, $a^{\star}$, определяемой как наименьшая неподвижная точка операции $x \to 1 \lor ax$. Если в такой решётке определены операции левого и правого деления, естественным образом согласованные с операцией умножения и частичным порядком, задаваемым решёточной структурой, получается решётка Клини с делением [Пратт 1991, Козен 1994]. Относительно интерпретации на решётках с делением (без итерации Клини) корректно и полно исчисление Ламбека с аддитивными конъюнкцией и дизъюнкцией. Добавление итерации Клини с соответствующими аксиомами даёт логику решёток Клини с делениями (в иностранной литературе также используется термин "action logic"). Для болеесильной системы, полной относительно более узкого класса $\star$-непрерывных алгебр Клини (где $a^\star$ определяется как $\sup \{ a^n | n = 0,1,2,3... \}$), известно [Бушковский 2007], что эта логика неразрешима, точнее - $П_1^0$-полна. Вопрос о сложности для логики всех решёток Клини с делением в работах Пратта, Козена и Бушковского оставлен как открытая проблема. Будет рассказано её решение: доказательство неразрешимости, а именно $\Sigma_1^0$-полноты.