ISSN 1519-9681



Vol. 10(7), 2010
Vol. 10(6), 2010
Vol. 10(5), 2010
Vol. 10(4), 2010
..Vol. 10(2), 2010
Vol. 10(1), 2010

Vol. 10(7), 2010
Fibring of hypersequent calculi and preservation
of rule-elimination
Marcelo E. Coniglio(1); Martín Figallo(2)
(1) CLE and Department of Philosophy
State University of Campinas - Campinas, Brazil
(2) Department of Mathematics
Universidad Nacional del Sur - Bahía Blanca, Argentina


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. We say that a commutative hypersequent calculus A has the full r-elimination property if for every derivation in A (from a set of premises) there is another derivation in A, from the same premises, without using the rule r; full cut-elimination is an important particular case of this notion. In this paper, we present a category of formal hypersequent calculi with their morphisms, and define their combinations by means of unconstrained and constrained (categorical) fibring. Using an example given by A. Avron we prove that the usual cut-elimination property is not preserved by unconstrained fibring of hypersequent calculi, provided that at least one of the calculi satisfy that metaproperty, and so r-elimination (w.r.t. derivations without premises) is not preserved by fibring hypersequents. On the other hand, we prove that fibring of (hyper)sequent calculi preserves full r-elimination provided that at least one of the calculi satisfy that metaproperty. In particular, fibring of (hyper)sequent calculi preserves full cut-elimination.
vol. 10, n. 7, 2010

|   Home   |   2011   |   2010   |   2009   |   2008   |   2007   |    2005   |   2004   |   2003   |   2002   |   2001   |

© 2001-2008 - Centre for Logic, Epistemology and the History of Science – CLE