Derivability in certain subsystems of the Logic of Proofs is -complete

The Logic of Proofs realizes the modalities from traditional modal logics with proof polynomials, so an expression □ F becomes t : F where t is a proof polynomial representing a proof of or evidence for F . The pioneering work on explicating the modal logic S 4 is due to S. Artemov and was extended to several subsystems by V. Brezhnev. In 2000, R. Kuznets presented a Π 2 p algorithm for deducibility in these logics; in the present paper we will show that the deducibility problem is Π 2 p -complete. (The analogous problem for traditional modal logics is PSPACE-complete.) Both Kuznets’s work and the present results make assumptions on the values of proof constants.