We begin with display and labelled calculi for a certain class of tense logics. These tense logics are extensions of Kt with any finite number of general path axioms, which are axioms of the form Xp -> Yp, where X and Y represent sequences of black and white diamonds.
For the minimal tense logic Kt, we provide a bi-directional embedding between display calculus proofs and labelled calculus proofs. It is then shown how to translate display proofs for Kt extended with general path axioms into labelled proofs.
Providing a reverse translation--translating labelled proofs into display proofs for Kt extended with general path axioms--has proven to be much more difficult because certain labelled structural rules do not correspond well to the display variants of such rules. Nevertheless, for a certain subclass of general path axioms a translation from labelled calculus proofs to display calculus proofs can be provided. Through the addition of special rules, referred to as "propagation rules," we can prove that the problematic structural rules are admissible in the resulting calculus. Every proof of a formula in this calculus contains sequents whose structure corresponds to a tree with two types of edges. This specific structure allows us to translate these proofs into display proofs, which gives an answer to an open question of translating labelled proofs to display proofs for extensions of the minimal tense logic Kt.
Effective Translations between Display and Labelled Proofs for Tense Logics