Неразрешимое промежуточное исчисление

Приводится исчисление с конечным числом аксиом, расположенное строго между классическим и интуиционистским пропозициональными исчислениями, для которого проблема выводимости алгоритмически неразрешима. Доказательство этого факта производится сведением проблемы выводимости в исчислениях Поста к проблеме выводимости в указанном исчислении.