Неразрешимое итеративное пропозициональное исчисление

Рассматриваются итеративные пропозициональные исчисления, представляющие собой конечные множества пропозициональных формул вместе с операцией modus ponens и операцией суперпозиции, заданной множеством операций Мальцева. Для таких исчислений изучается вопрос разрешимости проблемы выводимости формул. Строится неразрешимое итеративное пропозициональное исчисление, аксиомы которого зависят от трёх переменных. Вывод формул в данном исчислении моделирует процесс решение проблемы соответствий Поста. В частности, доказывается, что общая проблема выразимости для итеративных пропозициональных исчислений алгоритмически неразрешима.