Predicate provability logic with non-modalized quantifiers (Q1176101)

A modal predicate formula is called a \(Q'\)-formula if it has no quantifiers within the scope of \(\square\). Let \(T\) be an arithmetical theory extending Peano arithmetic \((PA)\); it is also supposed that all theorems of \(T\) are true, and Gödel numbers of axioms of \(T\) are given by a formula \(\alpha(x)\) which is ''provably binumerable'' in \(T\), that is \[ T\vdash\forall x(\alpha(x)\to Pr[\alpha(x)])\land\forall x(\neg\alpha(x)\to P_ 2[\neg\alpha(x)]) \] (\(Pr\) is based on \(\alpha\) and encodes provability in \(T\)). As usual, \(Q'\)-formulas can be interpreted as arithmetical ones if \(\square\) is transcribed as \(Pr\). \(Q'L(T)\) (resp. \(Q'L\)) denotes the set of all \(Q'\)-formulas whose interpretations are always provable in \(T\) (resp. true). It is known that if \(T\) is \(RE\) then \(Q'L(T)\) is \(\Pi^ 0_ 2\)-complete (Vardanyan) and \(Q'L\) is non-arithmetical (Artemov). The paper proves that nevertheless \(Q'L(T)\) and \(Q'L\) can be axiomatized in some other cases. Namely, let \(Q'GL\), \(Q'S\) be \(Q'\)-fragments of quantified versions of Gödel-Łöb's logic \(GL\) and Solovay's logic \(S\). The main theorem claims that \(Q'L(T)=Q'GL\) and \(Q'L=Q'S\) whenever \(Pr_{Q'GL}(x)\) is provably binumerable in \(T\).