Axioms vs Hypersequent Rules with Context Restrictions: Theory and Applications

ABSTRACT. We investigate the connections between hypersequent rules with context restrictions and Hilbert axioms extending classical (and intuitionistic) propositional logic. We introduce sufficient syntactic conditions for cut elimination in such hypersequent calculi, translations between rules with context restrictions and axioms (and vice versa), and general decidability and complexity results. Our work subsumes many logic-tailored results, entails finite axiomatisability for a number of normal modal logics given by simple frame properties, and provides a method to construct cut-free hypersequent calculi from a set of axioms. As a case study we obtain a new cut-free hypersequent calculus and complexity bound for the logic of uniform deontic frames.