Deciding universal sentences in integral residuated lattices with a conucleus (INVITED)

Abstrakt

A conucleus on a residuated lattice is a generalization of an S4 modal operator on a Boolean algebra. Its interest stems from extending the relation between S4 modal algebras and Heyting algebras given by the Gödel translation to other varieties of residuated lattices. We consider the problem of deciding the validity of universal sentences (or equivalently, quasi-equations) in varieties of integral conuclear residuated lattices and show that among other varieties, MV-algebras with a conucleus and Abelian l-group cones with a conucleus have decidable universal theories. As a corollary, this settles positively the long-standing open problem of whether integral cancellative commutative residuated lattices have a decidable universal theory.