Substructural logics include classical, intuitionistic, linear, relevant, many-valued and fuzzy logic. Most of these logics are axiomatic extensions of FL, the logic associated with the full Lambek calculus. The algebraic semantics for FL is the variety of (pointed) residuated lattices. The latter include purely algebraic structures like lattice-ordered groups and ideal lattices of rings, on top of the ones that come from logic: Boolean, Heyting and MV-algebras.

The algebraic study of substructural logics over FL has been successful and this may be one of the reasons why relational semantics have not attracted a lot of attention. Another reason is that the various relational semantics that have been introduced by different authors have not had many applications.

In this talk we will introduce Kripke-style semantics, called residuated frames, for substructural logics and show how they are related to residuated lattices. Moreover, we will show how we can obtain a cut elimination (or rather cut admissibility) result at the level of frames that implies the cut elimination of FL and of two more algebraic variants. The language of frames brings to the surface a fundamental property of the underlying relation that is related to cut elimination. We use this to construct a Gentzen system for ‘classical FL’. This is a Gentzen system with classical sequents and two distinct (due to the non-commutative nature of FL) negation operations. The cut elimination of the system is stated and proved at the frame level. The decidability of the Gentzen system and of the equational theory of involutive residuated lattices follow from this result.