Embeddings of Propositional Logics into the Provability Logics $\mathbf{S}$ and $\mathbf{D}$

Abstract

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