A focused approach to combining logics (Q639671)

The paper presents the proof system LKU which consists in a sequent calculus for classical logic with a rich notion of polarization. LKU was developed as a focused proof system intended to provide a unifying approach to logic. The system contains a rich set of logic connectives, introduction rules which are not sensitive to polarity, and structural rules that are sensitive to a change in polarity. By varying the polarity restrictions on the structural rules we obtain different fragments of LKU. This way it is possible to derive known focused proof systems for classical logic, intuitionistic logic and multiplicative-additive linear logic as well as explore the possibilities of a new logical system. Not all fragments of LKU satisfy cut elimination. However, the paper identifies a set of sufficient conditions in the generalized framework to ensure that cut elimination holds. The conditions are satisfied by the principal fragments of LKU above. A generalized proof of the completeness of focusing calculi with respect to their unfocused versions is also derived. Since the fragments of LKU are based on formulas containing the same set of connectives, a logic may include various fragments and the cut-rule can be used to communicate between these different fragments. The possibility of defining classical linear hybrid logics is explored as well as the circumstances when a classical lemma can be used in an intuitionistic proof while preserving intuitionistic provability. For related work in the area see [\textit{J.-Y. Girard}, Ann. Pure Appl. Logic 59, No.~3, 201--217 (1993; Zbl 0781.03044)]. A comparison between the LU system of Girard and the LKU system is also provided in the present paper.