A Gentzen system for involutive residuated lattices
type: Item
instance of: scholarly article
title: A Gentzen system for involutive residuated lattices
zbMATH Open document ID: 1088.06012
author: Annika M. Wille
published in: Algebra Universalis
publication date: 2006-03-21T00:00:00Z
review text: 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.
Mathematics Subject Classification ID: 06F05
Mathematics Subject Classification ID: 03B25
Mathematics Subject Classification ID: 03F03
Mathematics Subject Classification ID: 03F52
Mathematics Subject Classification ID: 03G25
zbMATH DE Number: 5013979
zbMATH Keywords: Gentzen system
zbMATH Keywords: involutive residuated lattice
zbMATH Keywords: linear logic
zbMATH Keywords: equational theory
reviewed by: Marius Tărnăuceanu
MaRDI profile type: Publication
full work available at URL: s00012-005-1957-6
OpenAlex ID: W1965379419
DOI: 10.1007/S00012-005-1957-6
description: scientific article; zbMATH DE number 5013979