Weak arithmetical interpretations for the Logic of Proofs

TitleWeak arithmetical interpretations for the Logic of Proofs
Publication TypeJournal Article
Year of Publication2016
AuthorsKuznets, R, Studer, T
JournalLogic Journal of IGPL
AbstractArtemov established an arithmetical interpretation for the Logics of Proofs LPCS, which yields a classical provability semantics for the modal logic S4. The Logics of Proofs are parameterized by so-called constant specifications CS, stating which axioms can be used in the reasoning process, and the arithmetical interpretation relies on constant specifications being finite. In this article, we remove this restriction by introducing weak arithmetical interpretations that are sound and complete for a wide class of constant specifications, including infinite ones. In particular, they interpret the full Logic of Proofs LP.