A unified compilation style labelled deductive system for modal and substructural logic using natural deduction

This paper describes a proof theoretic and semantic approach in which logics belonging to different families can be given common notions of derivability relation and semantic entailment. This approach builds upon Gabbay's methodology of Labelled Deductive Systems (LDS) and it is called the compilation approach for labelled deductive systems (CLDS). Two different logics are here considered, (i) the modal logic of elsewhere (known also as the logic of inequality) and (ii) the multiplicative fragment of substructural linear logic. A general natural deduction style proof system is given, in which the notion of a theory is defined as a (possibly singleton) structure of points, called a configuration, and a "general" model-theoretic semantic approach is described using a translation technique based on first-order logic. Then it is shown how both this proof theory and semantics can be directly applied to the logic of elsewhere and to linear logic, illustrating also that the same technique for proving soundness and completeness can be adopted in both logics. Finally, the proof systems for the logic of elsewhere and for linear logic are proved to correspond, under certain conditions, to standard Hilbert axiomatisation and standard sequent calculus respectively. Such results prove that the natural deduction proof systems described in this paper are proper generalisations of any proof system already developed for these two logics