Abstract

We present an intuitionistic sequent calculus for arbitrary finitely many-valued logics which has a positive semantics given by a natural extension of Kripke models. Our calculus has two types of rules: introduction rules and pseudo-cut rules. The introduction rules introduce formulas at all places on the left or on the right hand side of a sequent. They generalize the introduction rules of 2-places sequent calculus. The pseudo-cut rules allow to introduce formulas in the middle of a sequent. They may not exist in a 2-places sequent calculus. We show the soundness and completeness of our system and we study in detail the cut elimination procedure for these calculi.