Логика доказуемости без интерполяционного свойства Крейга

Введенная Г. К. Джапаридзе в 1986 г. модельная логика доказуемости $D$ определяется как замыкание множества теорем логики $GL$ и аксиомы $\neg\ \Box\ \bot\ \wedge\ [\Box(\Box p\vee\Box q)\to\Box p\vee\Box q]$ с помощью правил $\operatorname{modus\,pnens}$ и подстановки. Найдены модели логики $D$, и доказано, что эта логика не обладает интерполяционным свойством Крейга. Вопрос о существовании логики доказуемости, не обладающей свойством Крейга, до сих пор был открыт.
Библиогр. 11 назв.