Titulo: Algebraic aspects of cut elimination

We will present a purely algebraic method of proving the cut
elimination theorem for various sequent systems. Our motivation of
giving an algebraic proof of the cut elimination theorem is not only
to clarify the meaning of cut elimination from an algebraic point of
view, but also to give a proof of cut elimination accessible to
algebraists, avoiding heavy syntactic arguments which are usually seen
in the standard proof of cut elimination. Such a proof will be useful
also for algebraists, as cut elimination offers us a useful tool for
proving ecidability. For more information on our approach, see [1] and
[2] below.

Let S be a sequent system with cut, and let S~ be the system obtained
from S by deleting the cut rule. Our basic idea is to introduce
mathematical structures, called Gentzen matrices for S~, and to show
that S~ is with respect to the class of algebras for S. This is
carried out by using the "quasi-completion" of these Gentzen
matrices. It is shown that the quasi-completion is exactly a
generalization of the MacNeille completion. Our method can be applied
also to get the cut elimination theorem for predicate logics and modal
logics.

Starting from this unexpected connection between cut elimination and
MacNeille completions, the study has been developed further mainly by
Ciabattoni, Galatos and Terui as "algebraic proof theory" (see [3]).

References:
[1] F. Belardinelli, P. Jipsen and HO, Algebraic aspects of cut 
elimination theorem, Studia Logics, 2004.
[2] N. Galatos, P. Jipsen, T. Kowalski and HO, Residuated Lattices: 
an algebraic glimpse at substructural logics, Studies in Logic and the 
Foundations of Mathematics, vol.151, 2007.
[3] A. Ciabattoni, N. Galatos and K. Terui, Algebraic proof theory for 
substructural logics: cut-elimination and completions, APAL, 2012.