Nonaxiomatizability of predicate logics of proofs (Q1406443)

The present paper deals with the problem of the possibility of the effective description of the predicate logics of proofs. The author shows that the predicate logics of proofs possess also a lower bound for complexity, namely the true predicate logic of proofs is \(\Pi_1^0(\text{TA})\)-complete, where TA is the set of true arithmetic propositions. Also, the logic of proofs restricted by the tools of formal arithmetics PA is \(\Pi_2^0\)-hard.