Abstract

In this paper we prove the equivalence between the Gentzen system G LJ*\c, obtained by deleting the contraction rule from the sequent calculus LJ* (which is a redundant version of LJ), the deductive system IPC*\c and the equational system associated with the variety RL of residuated lattices. This means that the variety RL is the equivalent algebraic semantics for both systems G LJ*\c in the sense of [18] and [4], respectively. The equivalence between G LJ*\c and IPC*\c is a strengthening of a result obtained by H. Ono and Y. Komori [14, Corollary 2.8.1] and the equivalence between G LJ*\c and the equational system associated with the variety RL of residuated lattices is a strengthening of a result obtained by P.M. Idziak [13, Theorem 1].An axiomatization of the restriction of IPC*\c to the formulas whose main connective is the implication connective is obtained by using an interpretation of G LJ*\c in IPC*\c.