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.

You do not currently have access to this article.