On the complexity of the reflected logic of proofs

Artemov's propositional logic of proofs LP captures all invariant properties of proof predicates “t is a proof of F ” which are represented in LP as formulas t:F. Kuznets in [On the complexity of explicit modal logics, in: Computer Science Logic 2000, Lecture Notes in Computer Science, Vol. 1862, Springer, Berlin, 2000, pp. 371–383] showed that the satisfiability problem for LP belongs to the class of the polynomial hierarchy. In this paper we consider the reflected logic of proofs, rLP, consisting of formulas t:F derivable in LP. The system rLP is as expressible as LP itself, since every F derivable in LP is represented in rLP by t:F for an appropriate proof term t. We prove a better upper bound (NP) for the decision procedure in rLP. In addition we prove the disjunctive property for the original logic of proofs LP, thus answering a well-known question in this area.