On a Contraction-Less Intuitionistic Propositional Logic with Conjunction and Fusion

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 .