A Gentzen system for involutive residuated lattices (Q818712)

A cut-free Gentzen system was developed by J. Y. Girard for Girard quantales. The goal of the present paper is to establish such a system in the more general situation of involutive residuated lattices. Moreover, soundness and completeness are proved by using some algebraic arguments. The proof of completeness is connected to a version of \textit{M. Okada} and \textit{K. Terui} [J. Symb. Log. 64, No.~2, 790--802 (1999; Zbl 0930.03021)], presented in an algebraic form by \textit{P. Jipsen} and \textit{C. Tsinakis} [in: J. Martínez (ed.), Ordered algebraic structures. Proceedings of the conference on lattice-ordered groups and \(f\)-rings held at the University of Florida, Gainesville, FL, USA, February 28--March 3, 2001. Dordrecht: Kluwer Academic Publishers. Developments in Mathematics 7, 19--56 (2002; Zbl 1070.06005)], too. A remarkable conclusion of these proofs is that the equational theory of involutive residuated lattices is decidable.