О пренексном фрагменте логики доказуемости с кванторами по доказательствам

Рассматривается фрагмент логики доказуемости с ванторами по доказательствам, в котором кванторы не встречаются в области действия предиката доказательств. Логика ql есть по определению множество формул этого языка, истинных в стандартной модели арифметики при любой интерпретации, основанной на стандартном гёделевском предикате доказательств для арифметики Пеано. Описана семантика Крипке для логики ql и доказана теорема о полноте. Установлена разрешимость для случая инъективных интерпретаций.