Title

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

Document Type

Article

Publication Date

3-2007

Abstract

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.

Journal

Annals of Pure and Applied Logic

Volume

145

Issue

3

First Page

223

Last Page

239