Gentzen's sequent calculus can be given additional structure via focusing. We illustrate how that additional structure can be used to construct synthetic inference rules. In particular, bipolar formulas (a slight generalization of geometric formulas) can be converted to such synthetic rules once polarity is assigned to the atomic formulas and some logical connectives. Since there is some flexibility in the assignment of polarity, a given formula might yield several different synthetic rules. It is also the case that cut-elimination immediately holds for these new inference rules. Such conversion of bipolar axioms to inference rules can be done in classical and intuitionistic logics.
This talk is based in part on a paper in the Annals of Pure and Applied Logic co-authored with Sonia Marin, Elaine Pimentel, and Marco Volpe (2022).[-]

Gentzen's sequent calculi LK and LJ are landmark proof systems. They identify the structural rules of weakening and contraction as notable inference rules, and they allow for an elegant statement and proof of both cut-elimination and consistency for classical and intuitionistic logics. Among the undesirable features of sequent calculi is the fact that their inferences rules are very low-level. We present the focused proof system LKF in which synthetic inference rules can systematically be defined and for which cut-eliminate hold.[-]