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 S4 is due to S. Artemov and was extended to several subsystems by V. Brezhnev. In 2000, R. Kuznets presented a algorithm for deducibility in these logics; in the present paper we will show that the deducibility problem is -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.