Abstract

MacNeille Completions of FLalgebras.
(A. Ciabattoni, N. Galatos and K. Terui)
We show that a large number of equations
are preserved under DedekindMacNeille completions when applied to
subdirectly irreducible FLalgebras/residuated lattices.
These equations are identified in a systematic way,
based on prooftheoretic ideas and techniques in substructural logics.
It follows that a large class of
varieties of Heyting algebras and FLalgebras is closed under completions.

Algebraic proof theory for substructural logics:
cutelimination and completions.
(A. Ciabattoni, N. Galatos and K. Terui)
We carry out a unified investigation of two prominent topics in
proof theory and algebra: cutelimination and completion,
in the setting of substructural logics
and residuated lattices.
We introduce the substructural hierarchy 
a new classification of logical axioms
(algebraic equations)
over full Lambek calculus FL, and show that
cutelimination for extensions of FL and
the MacNeille completion for subvarieties of pointed
residuated lattices
coincide up to the level N2 in the hierarchy.
Negative results, which indicate limitations of
cutelimination and the MacNeille completion, as well as
of the expressive power of structural sequent rules, are also provided.
Our arguments interweave
proof theory and algebra, leading to
an integrated discipline which we call algebraic proof theory.