Algebraic proof theory: Hypersequents and hypercompletions

We continue our program of establishing connections between proof-theoretic and order-algebraic properties in the setting of substructural logics and residuated lattices. Extending our previous work that connects a strong form of cut-admissibility in sequent calculi with closure under MacNeille completions of corresponding varieties, we now consider hypersequent calculi and more general completions; these capture logics/varieties that were not covered by the previous approach and that are characterized by Hilbert axioms (algebraic equations) residing in the level P3 of the substructural hierarchy. We provide algebraic foundations for substructural hypersequent calculi and an algorithm to transform P3 axioms/equations into equivalent structural hypersequent rules. Using residuated hyperframes we link strong analyticity in the resulting calculi with a new algebraic completion, which we call hyper-MacNeille.