Hypersequents,logical consequence and intermediate logics for concurrency

The existence of simple semantics and appropriate cut-free Gentzen-type formulations are fundamental intrinsic criteria for the usefulness of logics. In this paper we show that by using hypersequents (which are multisets of ordinary sequents) we can provide such Gentzen-type systems to many logics. In particular, by using a hypersequential generalization of intuitionistic sequents we can construct cut-free systems for some intermediate logics (including Dummett's LC) which have simple algebraic semantics that suffice, e.g., for decidability. We discuss the possible interpretations of these logics in terms of parallel computation and the role that the usual connectives play in them (which is sometimes different than in the sequential case).