О позитивных логиках доказуемости

Рассматривается фрагмент языка модальной логики, состоящий из импликаций $A\to B$, где формулы $A$ и $B$ строятся из пропозициональных переменных и константы "истина" лишь с помощью конъюнкции и модальностей типа ромб. Такой фрагмент называем строго позитивным.
Более бедный язык позволяет обобщить стандартную интерпретацию связки $\Diamond$ как гёделевской формулы, выражающей непротиворечивость формальной арифметики, на более широкие классы арифметических схем, в частности на так называемые схемы рефлексии. В позитивной логике переменные интерпретируются как множества арифметических предложений (схемы), а связки — как операции над такими множествами.
Для строго позитивных фрагментов стандартных модальных логик ранее была установлена разрешимость за полиномиальное время. В то же время, строго позитивный язык оказывается достаточно выразительным для конкретных применений логики доказуемости к исследованию формальных теорий, в частности, к построению систем ординальных обозначений.
Мы формулируем арифметически полное исчисление с модальностями, занумерованными натуральными числами и символом $\omega$, где $\omega$ соответствует полной равномерной схеме рефлексии в арифметике, а $n<\omega$ соответствует ограничению этой схемы арифметическими $\Pi_{n+1}$-предложениями. Для этого исчисления устанавливается теорема о полноте относительно подходящего класса конечных шкал Крипке, доказывается полиномиальная разрешимость проблемы выводимости, а также теорема об арифметической полноте, аналогичная известной теореме Р. Соловея для стандартной логики доказуемости.