Abstract
-
MacNeille Completions of FL-algebras.
(A. Ciabattoni, N. Galatos and K. Terui)
We show that a large number of equations
are preserved under 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 a large class of
varieties of Heyting algebras and FL-algebras is closed under completions.
-
Algebraic proof theory for substructural logics:
cut-elimination and completions.
(A. Ciabattoni, N. Galatos and K. Terui)
We carry out a unified investigation of two prominent topics in
proof theory and algebra: cut-elimination 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
cut-elimination 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
cut-elimination 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.
