  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 attaching infinitely many worlds $t_1, t_2,
\ldots$, and $t_\omega$ to a world $t_0$ of a GL-model so that $t_0 \succ t_1
\succ t_2 \succ \cdots \succ t_\omega$. A non-normal modal logic D, which was
studied by Beklemishev (1999), is characterized as follows. A formula $\varphi$
is a theorem of D if and only if $\varphi$ is true at $t_\omega$ in any
D-model. D is an intermediate logic between the provability logics GL and S. A
Hilbert-style proof system for D is known, but there has been no sequent
calculus. In this paper, we establish two sequent calculi for D, and show the
cut-elimination theorem. We also introduce new Hilbert-style systems for D by
interpreting the sequent calculi. Moreover we show a general result as follows.
Let $X$ and $X^+$ be arbitrary modal logics. If the relationship between
semantics of $X$ and semantics of $X^+$ is equal to that of GL and D, then
$X^+$ can be axiomatized based on $X$ in the same way as the new axiomatization
of D based on GL.
