MacNeille completions of FL-algebras.

We show that a large number of equations are preserved by Dedekind-MacNeille completions when applied to subdirectly irreducible FL-algebras/residuated lattices. These equations are identified in a systematic way, based on proof-theoretic ideas and techniques in substructural logics. It follows that many varieties of Heyting algebras and FL-algebras admit completions. [ABSTRACT FROM AUTHOR]