When studying proof systems for various logics—particularly substructural or nonclassical ones, we are naturally led to the following natural question: Which axioms, when added to a base logic, preserve the cut-freeness of the proof system? Remarkably, this question has a precise algebraic counterpart: Which varieties of pointed residuated lattices are closed under MacNeille completions? 

In this talk, we will explore this connection through the lens of algebraic proof theory. We will introduce the substructural hierarchy and demonstrate that the class N_2 precisely marks the expressive boundary for (intuitionistic) sequent-style calculi, while the class P_3 represents the limit for hypersequent-style. As we classify familiar axioms within the hierarchy, an open question naturally arises: what proof system corresponds to the class N_3, which includes many important axioms, such as distributivity and the Łukasiewicz axiom.