Hypersequents are a natural generalization of ordinary sequents which turn out to be a very suitable tool for presenting cut-free Gentzent-type formulations for diverse logics. In this paper, an alternative way of formulating hypersequent calculi (by introducing meta-variables for formulas, sequents and hypersequents in the object language) is presented. A suitable category of hypersequent calculi with their morphisms is defined and both types of fibring (constrained and unconstrained) are introduced. The introduced morphisms induce a novel notion of translation between logics (...) which preserves metaproperties in a strong sense. Finally, some preservation features are explored. (shrink)

Direct download   Export citation   Bookmark