Interpolation method for multicomponent sequent calculi

Abstract

The proof-theoretic method of proving the Craig interpolation property was recently extended from sequents to nested sequents and hypersequents. There the notations were formalism-specific, obscuring the underlying common idea, which is presented here in a general form applicable also to other similar formalisms, e.g., prefixed tableaus. It describes requirements sufficient for using the method on a proof system for a logic, as well as additional requirements for certain types of rules. The applicability of the method, however, does not imply its success. We also provide examples from common proof systems to highlight various types of interpolant manipulations that can be employed by the method. The new results are the application of the method to a recent formalism of grafted hypersequents (in their tableau version), the general treatment of external structural rules, including the analytic cut, and the method’s extension to the Lyndon interpolation property.