Abstract of the author:

I will outline an algebraic and systematic approach to proof theory for substructural logics, which is being developed together with A. Ciabattoni, N. Galatos and L. Strassburger. In proof theory, one transforms Hilbert axioms into Gentzen rules to obtain cut-elimination theorems. In algebra, one embeds a given algebra into a complete one for various purposes. It is not surprising that these two are deeply related, since both are concerned with conservative extension. The connection is, however, even tighter than expected. For one thing, the passage from Hilbert axioms to Gentzen rules plays a crucial role for algebraic completion too. For another, Maehara-Okada cut-elimination can be construed as generalization of Dedekind-MacNeille completion. To illustrate the situation, we introduce a hierarchy on nonclassical axioms. One of our goals is then to identify a boundary in the hierarchy, below which proof theory (cut-elimination) works well and above which one finds negative algebraic results (failure of completions).

In the first talk, I will give a gentle introduction to the theory of Dedekind-MacNeille completions and algebraic cut-elimination, presumably for both sequent and hypersequent calculi. In the second talk, I will introduce the substructural hierarchy and show how it naturally classifies axioms in nonclassical logics, and apply the algebraic method to obtain uniform cut-elimination theorems for logics whose axioms are located at a low level of the substructural hierarchy.