A formal framework for hypersequent calculi and their fibring

Marcelo Coniglio

Martin Figallo

pp. 73-93

in: Arnold Koslow, Arthur Buchsbaum (eds), The road to universal logic I, Basel, Birkhäuser, 2015

Abstract

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.