© 2001 by Oxford University Press
Intuitionistic sequent calculi for finitely many-valued logics
A1 Institut Supérieur d'Electronique de Paris, 21 rue d'Assas, 75006 Paris, France E-mail: eugenia.reznik@isep.fr A2 Trusted Logic, 5 rue du Bailliage, 78000 Versailles, France E-mail: curmin@logique.jussieu.fr
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.
Key Words: finitely many-valued logics, sequent calculus, Kripke models, cut elimination