Неразрешимые свойства расширений логики доказуемости. I

Доказывается, что не существует алгоритмов, которые по аксиоматике исчисления в нормальных расширениях логики доказуемости $GL$ определяли бы, обладает ли это исчисление следующими свойствами: разрешимостью, финитной аппроксимируемостью, дизъюнктивным свойством, интерполяционным свойством.