Неразрешимость логики Гёделя–Лёба с кванторами по пропозициональным переменным

Рассмотрена известная модальная логика доказуемости $GL$ в языке с кванторами по пропозициональным переменным, пополненная естественными кванторными аксиомами. Доказана ее неразрешимость. Результат сохраняется при расширении логики формализованным принципом неподвижной точки.
Библиогр. 4.