The Canonical FEP Construction for Residuated Lattice Ordered Algebras

A class of algebras has the finite embeddability property (FEP, for short) if every finite partial subalgebra of a member of the class can be embedded into a finite member of the class. If a class of algebras has the FEP then it is generated as a quasivariety by its finite members hence, if it is finitely axiomatized it has a decidable quasi-equational theory (and also a decidable universal theory) [1]. If a class of algebras with the FEP algebraizes a logic, then the logic has the finite model property; in fact, it has the ‘strong finite model property ’ meaning that if a rule is refutable in the logic, then it is refutable in a finite model of the logic. Consequently, decidability results for a logic may also be obtained by proving the FEP for its algebraic model class. In this talk we consider ‘residuated lattice ordered algebras’, which are al-gebras with an underlying lattice order and with unary and binary operations that are ‘residuated’. A unary function f: A → A is called residuated if there exists a function g: A → A such that f(a) ≤ b if, and only if, a ≤ g(b) for all a, b ∈ A. A binary function ◦ : A × A → A is called residuated if there exis