Many new results and new insights about classical and non-classical logics have been obtained using the sequent calculus, e.g. Gentzen’s consistency argument; interpolation, decidability, complexity for modal and substructural logics; (what else?).
I would like to identify new results and insights about logics that were obtained using proof systems—other than the sequent calculus—that utilised some notion of analyticity / a restriction of proof space such as the subformula property. I am interested across all sorts of logics and all sorts of formalisms like hypersequent, nested, labelled, display, proof nets, deep inference based. Here I am viewing a logic as a set of formulas.
For example, hypersequent calculi were recently used to obtain new decidability and complexity upper bounds for many substructural logics extending the commutative Full Lambek calculus with weakening (FLew) and contraction (FLec). See this post for more on these logics.[BalLanRam21] A. R. Balasubramanian, Timo Lang, RR. Decidability and Complexity in Weakening and Contraction Hypersequent Substructural Logics. LICS 2021.
I would be pleased to see your thoughts and references on this below !