Abstract

A residuated algebra is a generalization of a residuated groupoid; instead of one basic binary operation with residual operations \,/, it admits finitely many basic operations, and each n-ary basic operation is associated with n residual operations. A logical system for RAs was studied in e.g. [6, 8, 15, 16] under the name: Generalized Lambek Calculus GL. In this paper we study GL and its extensions in the form of sequent systems. We prove an interpolation property which allows to replace a substructure of the antecedent structure by a single formula in a provable sequent. Together with model constructions, based on nuclei [13], interpolation leads to proofs of Finite Embeddability Property for different classes of RAs, as e.g. all RAs, distributive lattice-ordered RAs, boolean RAs, Heyting RAs and double RAs