Derivability in certain subsystems of the logic of proofs is \(\Pi_2^p\)-complete (Q866565)

The Logic of Proofs LP, proposed by S. Artemov, is a realization of the modal logic S4 in which the modality is replaced with explicit terms representing proofs. V. Brezhnev extended the idea of explication to several subsystems, among which the K4 version is of particular interest as the Logic of Beliefs, and R. Kuznets presented a \(\Pi_2^p\) algorithm for deducibility in these logics. In this paper, the author shows that deciding derivability in several significant sybsystems of LP is \(\Pi_2^p\)-hard by encoding QBF-2 as a formula of LP which can be derived only if the quantified Boolean formula is true. From this, in conjuction with the observations by Kuznets, it follows that derivaibility in each of the subsystems is \(\Pi_2^p\)-complete, while the analogous problem for corresponding modal logics is known to be PSPACE-comple.