Cut-free sequent calculi for the provability logic D

Ryo Kashima, Taishi Kurahashi, Sohei Iwata +1

We say that a Kripke model is a GL-model if the accessibility relation $\prec$ is transitive and converse well-founded. We say that a Kripke model is a D-model if it is obtained by…