Niveau: Supérieur
A Focused Approach to Combining Logics Chuck Lianga, Dale Millerb aDepartment of Computer Science, Hofstra University, Hempstead, NY 11550, USA bINRIA Saclay – Ile-de-France and LIX/Ecole Polytechnique, 91128 Palaiseau, France Abstract We present a compact sequent calculus LKU for classical logic organized around the concept of polarization. Focused sequent calculi for classical, intuitionistic, and multiplicative-additive linear logics are derived as fragments of the host system by varying the sensitivity of specialized structural rules to polarity in- formation. We identify a general set of criteria under which cut elimination holds in such fragments. From cut elimination we derive a unified proof of the completeness of focusing. Furthermore, each sublogic can interact with other fragments through cut. We examine certain circumstances, for example, in which a classical lemma can be used in an intuitionistic proof while preserving intuitionistic provability. We also examine the possibility of defining classical- linear hybrid logics. Key words: focused proof systems, unity of logic, linear logic 1. Introduction Gentzen presented natural deduction proof systems for both intuitionistic and classical logics in [1]. The natural deduction system NJ for intuitionistic logic contained introduction and elimination rules for each logical connective. The natural deduction system NK for classical logic contained the same intro- duction and elimination rules but added the external axiom for the excluded middle.
- logic
- focused proof
- contraction rules except
- llf
- cut elimination
- proof systems
- structural rules
- divided into
- between classical
- sequent calculus