Embeddings of Propositional Logics into the Provability Logics S and D

2026/08/05 by Mashu Noguchi
Mathematics · #math.LO #msc:03B45 #msc:03F45

paper · pdf

25 pages

arxiv created 2026/08/06 · arxiv updated 2026/08/07

Abstract

Just as Visser showed that the formal propositional logic FPL can be embedded into Gödel-Löb provability logic GL, Petrukhin proposed a propositional logic SPL that can be embedded into Solovay's non-normal provability logic S. In this paper, we fix Petrukhin's proof and extend the result to Japaridze's provability logic D, and propose a propositional logic DPL that can be embedded into D.

Citations

• Cut-free sequent calculi for the provability logic D
• Semantical cut-elimination for the provability logic of true arithmetic
• A propositional logic with explicit fixed points
• Provability interpretations of modal logic
• The Logic of Provability