Об арифметической сложности предикатных логик полных конструктивных арифметических теорий

В статье доказывается, что предикатная логика всякой полной конструктивной арифметической теории $T$, обладающей свойством экзистенциальности, является $\Pi_1^T$-полной. Для этого используется техника равномерного частичного определения истинности для интуиционистских арифметических теорий. Основная теорема применяется для характеризации предикатной логики, соответствующей одному из вариантов понятия реализуемой предикатной формулы. А именно, показано, что множество всех неопровержимых предикатных формул рекурсивно изоморфно дополнению множества $\emptyset^{(\omega +1)}$.