Residuated lattices. An algebraic glimpse at substructural logics (Q881452)

Substructural logics encompass, among many others, classical logic, intuitionistic logic, relevance logics, many-valued logics, fuzzy logics, linear logic and their non-commutative versions. This book is about residuated lattices and substructural logics. The main aim of the book is to consider both the algebraic and logical perspective within a common framework, to show that the interplay between algebra and logic is very natural and that it provides a deeper understanding of the subject. The first part of the book, consisting of the first three chapters, does not assume knowledge of logic or universal algebra and is intended to be accessible to graduate students. In particular, it can be used as a textbook for a graduate course in the subject complemented by some of the next four chapters. Therefore, the authors included many examples, exercises, explanatory remarks about the connections of algebra and logic, and suggested research directions. The later chapters contain many recent results of interest to the specialist in the area, and are to a large extend mutually independent as it is implied by the dependency chart. The book itself originated from a short monograph, written by the last two coauthors and published in 2001 under the title ``Residuated lattices. An algebraic glimpse at logics without contraction'', where the focus was on logics with exchange and weakening, whose algebraic models are integral commutative residuated lattices. Due to significant advances in the study of residuated lattices and to a deeper understanding of their connections with substructural logics, this book develops the general theory and includes recent results in the setting without structural rules. Furthermore, it refers to a broader perspective, proposes new directions of research, and has attained a stronger algebraic flavor, partly due to the background of the first two coauthors. Chapter 1 covers the basic definitions and results of first-order logic and universal algebra. This is followed by presentations of (propositional) classical and intuitionistic logic, both via a Hilbert system and a Gentzen system. A section on the connections between these logics and their algebraic counterparts, namely Boolean algebras and Heyting algebras, is followed by a discussion of the cut-elimination theorem for the Gentzen systems. The authors conclude with a section on consequence relations and logical matrices. Chapter 2 begins with defining the substructural logic FL via a Gentzen-style sequent calculus and several extensions that are obtained by adding certain basic structural rules. A discussion of the general concept of substructural logics over FL and their algebraic models leads to the central definition of FL-algebras and residuated lattices. Some of their basic algebraic properties are given. The parametrized local deduction theorem and an equivalent Hilbert system for FL are derived and the authors show that the variety of FL-algebras is an equivalent algebraic semantics of the Hilbert system for FL. Chapter 3 considers many aspects of residuation, starting with pairs of residuated maps and Galois connections, and going on to residuated pogroupoids and involutive residuated structures. The last section covers the recently developed structure theory of residuated lattices. Chapter 4 starts with detailed proofs of cut elimination for various sequent systems. Decidability of the systems is obtained as an easy consequence of cut elimination for systems that lack the contraction rule. After a survey of various decidability results in other logics and in varieties of residuated lattices, the authors prove the undecidability of the quasi-equational theory of various distributive varieties of FL-algebras and residuated lattices, as a consequence of the unsolvability of the word problem. In Chapter 5 the authors discuss some important logical properties of substructural logics from both a proof-theoretic and an algebraic perspective. These include the disjunction property, Halldén completeness, Maksimovs's variable separation property and Craig interpolation property. In Chapter 6 the authors discuss completions of residuated lattices and focus on canonical extensions and Dedekind-MacNeille completions. The authors describe an embedding of a partial residuated lattice into a full one. This embedding preserves finiteness in certain subvarieties, yielding there the finite embeddability property. An alternative, algebraic, proof of cut elimination is presented in Chapter 7, by means of a quasi-embedding of a Gentzen matrix. Chapter 8 deals with a generalization of the Glivenko translation of intuitionistic propositional logic into classical logic by means of a double negation interpretation. The authors show that this translation holds between many other pairs of substructural logics and characterize all such pairs for which one of the logics is involutive. In Chapter 9 the authors study various aspects of the subvariety lattices of residuated lattices and FL-algebras, or dually to the lattice of substructural logics. Also, this chapter is devoted to the investigation of minimal (atoms) and almost minimal non-trivial varieties, or equivalently of maximal and almost maximal consistent substructural logics. The authors study particular properties which specify properties of the lattice: commutativity, representability, idempotency, cancellativity, integrality, and their combinations. In Chapter 10 the authors discuss the structure of subvariety lattices a little further, focusing on splittings. A splitting is a way of dividing a lattice in half. If possible, this allows for studying these two parts separately. The authors prove that there is only one splitting, which is of a trivial nature since the lattice splits into its bottom element and everything else. The argument, however, develops an extension of Jankov's characteristic formulas, which may be applicable in other contexts. Finally, Chapter 11 deals with the universal algebraic properties of being semisimple and possessing a discriminator term. The setting is narrowed to the commutative and integral case, but the results are positive. Also, the authors prove that free algebras are semisimple and all semisimple varieties are discriminator varieties, which implies that semisimplicity is a Mal'tsev property in the commutative integral setting.