CUT-FREE SEQUENT CALCULI FOR THE PROVABILITY LOGIC D

Abstract We say that a Kripke model is a GL-model (Gödel and Löb 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 $\mathbf {D}$ , which was studied by Beklemishev [3], is characterized as follows. A formula $\varphi $ is a theorem of $\mathbf {D}$ if and only if $\varphi $ is true at $t_\omega $ in any D-model. $\mathbf {D}$ is an intermediate logic between the provability logics $\mathbf {GL}$ and $\mathbf {S}$ . A Hilbert-style proof system for $\mathbf {D}$ is known, but there has been no sequent calculus. In this paper, we establish two sequent calculi for $\mathbf {D}$ , and show the cut-elimination theorem. We also introduce new Hilbert-style systems for $\mathbf {D}$ by interpreting the sequent calculi. Moreover, we show that D-models can be defined using an arbitrary limit ordinal as well as $\omega $ . Finally, 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 $\mathbf {GL}$ and $\mathbf {D}$ , then $X^+$ can be axiomatized based on X in the same way as the new axiomatization of $\mathbf {D}$ based on $\mathbf {GL}$ .